verifythis_fm2012_lcp.mlw 14.1 KB
Newer Older
1
(**
2

3 4 5 6 7 8 9 10 11 12 13
{1 VerifyThis@fm2012 competition, Challenge 1: Longest Repeated Substring}

{h
The following is the original description of the verification task,
reproduced verbatim. A <a
href="http://fm2012.verifythis.org/challenges">reference
implementation in Java</a> (based on code by Robert Sedgewick and
Kevin Wayne) was also given. The Why3 implementation below follows the
Java implementation as faithfully as possible.

<pre>
14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
Longest Common Prefix (LCP) - 45 minutes

VERIFICATION TASK
-----------------

Longest Common Prefix (LCP) is an algorithm used for text querying. In
the following, we model text as an integer array. You may use other
representations (e.g., Java Strings), if your system supports them.

LCP can be implemented with the pseudocode given below. Formalize and
verify the following informal specification for LCP.

Input:  an integer array a, and two indices x and y into this array
Output: length of the longest common prefix of the subarrays of a
        starting at x and y respectively.

Pseudocode:

    int lcp(int[] a, int x, int y) {
        int l = 0;
34
        while (x+l&lt;a.length && y+l&lt;a.length && a[x+l]==a[y+l]) {
35 36 37 38 39 40
            l++;
        }
        return l;
    }


MARCHE Claude's avatar
MARCHE Claude committed
41
ADVANCED
42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
========

BACKGROUND
----------

Together with a suffix array, LCP can be used to solve interesting text
problems, such as finding the longest repeated substring (LRS) in a text.

A suffix array (for a given text) is an array of all suffixes of the
text. For the text [7,8,8,6], the suffix array is
[[7,8,8,6],
   [8,8,6],
     [8,6],
       [6]]

Typically, the suffixes are not stored explicitly as above but
represented as pointers into the original text. The suffixes in a suffix
array  are sorted in lexicographical order. This way, occurrences of
repeated substrings in the original text are neighbors in the suffix
MARCHE Claude's avatar
MARCHE Claude committed
61
array.
62 63 64 65 66 67 68 69 70 71 72 73 74 75 76

For the above, example (assuming pointers are 0-based integers), the
sorted suffix array is:

[3,0,2,1]

VERIFICATION TASK
-----------------

The attached Java code contains an implementation of a suffix array
(SuffixArray.java), consisting essentially of a lexicographical
comparison on arrays, a sorting routine, and LCP.

The client code (LRS.java) uses these to solve the LRS problem. Verify
that it does so correctly.
77
</pre>}
MARCHE Claude's avatar
MARCHE Claude committed
78

79 80
*)

MARCHE Claude's avatar
MARCHE Claude committed
81 82


83
(** {2 First module: longest common prefix} 
84

85
    it corresponds to the basic part of the challenge
86

87
*)
88

89
module LCP 
90

MARCHE Claude's avatar
MARCHE Claude committed
91
use export int.Int
92
use import array.Array
MARCHE Claude's avatar
MARCHE Claude committed
93

94 95 96
(** [is_common_prefix a x y l] is true when the prefixes of length [l]
    at respective positions [x] and [y] in array [a] are identical. In
    other words, the array parts a[x..x+l-1] and a[y..y+l-1] are equal
97 98
    *)
predicate is_common_prefix (a:array int) (x y l:int) = 
99
  0 <= l /\ x+l <= a.length /\ y+l <= a.length /\ 
MARCHE Claude's avatar
MARCHE Claude committed
100 101
  (forall i:int. 0 <= i < l -> a[x+i] = a[y+i])

102 103 104
(** This lemma helps for the proof of [lcp] (but is not mandatory) and
    is needed later (for [le_trans]) *)
lemma not_common_prefix_if_last_char_are_different:
MARCHE Claude's avatar
MARCHE Claude committed
105 106 107 108
  forall a:array int, x y:int, l:int.
    0 <= l /\ x+l < a.length /\ y+l < a.length /\ a[x+l] <> a[y+l] ->
      not is_common_prefix a x y (l+1)

109 110 111
(** [is_longest_common_prefix a x y l] is true when [l] is the maximal
    length such that prefixes at positions [x] and [y] in array [a]
    are identical. *) 
112
predicate is_longest_common_prefix (a:array int) (x y l:int) = 
113 114 115
  is_common_prefix a x y l /\ 
  forall m:int. l < m -> not (is_common_prefix a x y m)

116 117 118
(** This lemma helps for proving [lcp] (but again is not mandatory),
    and is needed for proving [lcp_sym] and [le_trans] lemmas, and the
    post-condition of [compare] function in the "absurd" case *)
MARCHE Claude's avatar
MARCHE Claude committed
119 120 121 122 123
lemma longest_common_prefix_succ:
 forall a:array int, x y l:int.
  is_common_prefix a x y l /\ not (is_common_prefix a x y (l+1)) ->
  is_longest_common_prefix a x y l

MARCHE Claude's avatar
MARCHE Claude committed
124
use export ref.Refint
MARCHE Claude's avatar
MARCHE Claude committed
125

126
(** the first function, that compute the longest common prefix *)
MARCHE Claude's avatar
MARCHE Claude committed
127 128 129
let lcp (a:array int) (x y:int) : int
  requires { 0 <= x <= a.length }
  requires { 0 <= y <= a.length }
130
  ensures { is_longest_common_prefix a x y result }
MARCHE Claude's avatar
MARCHE Claude committed
131 132 133 134 135 136
  = let n = a.length in
    let l = ref 0 in
    while x + !l < n && y + !l < n && a[x + !l] = a[y + !l] do
      invariant { is_common_prefix a x y !l }
      incr l
    done;
MARCHE Claude's avatar
MARCHE Claude committed
137
    assert { not is_common_prefix a x y (!l+1) };
MARCHE Claude's avatar
MARCHE Claude committed
138 139
    !l

140 141 142 143 144

end

module LCP_test

145
(** test harness for lcp *)
146 147 148 149

use import array.Array
use import LCP

MARCHE Claude's avatar
MARCHE Claude committed
150
let test () =
MARCHE Claude's avatar
MARCHE Claude committed
151 152 153
  let arr = Array.make 4 0 in
  arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
  let x = lcp arr 1 2 in
MARCHE Claude's avatar
MARCHE Claude committed
154
  assert { is_common_prefix arr 1 2 1};
155
  assert { not is_common_prefix arr 1 2 2};
156
  check { x = 1 };
MARCHE Claude's avatar
MARCHE Claude committed
157 158 159 160
  (* int[] brr = {1,2,3,5}; *)
  let brr = Array.make 4 0 in
  brr[0]<-1; brr[1]<-2; brr[2]<-3; brr[3]<-5;
  let x = lcp brr 1 2 in
MARCHE Claude's avatar
MARCHE Claude committed
161
  assert { is_common_prefix brr 1 2 0};
162
  assert { not is_common_prefix brr 1 2 1};
163
  check { x = 0 };
MARCHE Claude's avatar
MARCHE Claude committed
164 165 166 167
  (* int[] crr = {1,2,3,5}; *)
  let crr = Array.make 4 0 in
  crr[0]<-1; crr[1]<-2; crr[2]<-3; crr[3]<-5;
  let x = lcp crr 2 3 in
MARCHE Claude's avatar
MARCHE Claude committed
168
  assert { is_common_prefix crr 2 3 0};
169
  assert { not is_common_prefix crr 2 3 1};
170
  check { x = 0 };
MARCHE Claude's avatar
MARCHE Claude committed
171 172 173 174
  (* int[] drr = {1,2,3,3}; *)
  let drr = Array.make 4 0 in
  drr[0]<-1; drr[1]<-2; drr[2]<-3; drr[3]<-3;
  let x = lcp drr 2 3 in
MARCHE Claude's avatar
MARCHE Claude committed
175
  assert { is_common_prefix drr 2 3 1};
176
  assert { not is_common_prefix drr 2 3 2};
177
  check {x = 1}
178

MARCHE Claude's avatar
MARCHE Claude committed
179

MARCHE Claude's avatar
MARCHE Claude committed
180 181 182 183 184 185 186 187 188
end

(** {2 Second module: sorting with respect to prefixes } *)
module PrefixSort

  use import array.Array
  use import LCP

  (** order by prefix *)
189
  predicate lt (a : array int) (x y:int) =
MARCHE Claude's avatar
MARCHE Claude committed
190
     let n = a.length in
191
     0 <= x <= n /\ 0 <= y <= n /\
192
     exists l:int. is_common_prefix a x y l /\
193
     (y+l < n /\ (x+l = n \/ a[x+l] < a[y+l]))
MARCHE Claude's avatar
MARCHE Claude committed
194

195 196


MARCHE Claude's avatar
MARCHE Claude committed
197
(** comparison function, that decides the order of prefixes *)
MARCHE Claude's avatar
MARCHE Claude committed
198
let compare (a:array int) (x y:int) : int
199 200
  requires { 0 <= x <= a.length }
  requires { 0 <= y <= a.length }
MARCHE Claude's avatar
MARCHE Claude committed
201
  ensures { result = 0 -> x = y }
202 203
  ensures { result < 0 -> lt a x y }
  ensures { result > 0 -> lt a y x }
MARCHE Claude's avatar
MARCHE Claude committed
204
  =
205
  if x = y then 0 else
MARCHE Claude's avatar
MARCHE Claude committed
206 207
  let n = a.length in
  let l = lcp a x y in
MARCHE Claude's avatar
MARCHE Claude committed
208
  assert { is_common_prefix a x y l };
MARCHE Claude's avatar
MARCHE Claude committed
209 210 211 212
  if x + l = n then -1 else
  if y + l = n then 1 else
  if a[x + l] < a[y + l] then -1 else
  if a[x + l] > a[y + l] then 1 else
213 214
  absurd

MARCHE Claude's avatar
MARCHE Claude committed
215

MARCHE Claude's avatar
MARCHE Claude committed
216 217
  predicate le (a : array int) (x y:int) = x = y \/ lt a x y
 
MARCHE Claude's avatar
MARCHE Claude committed
218 219 220 221
  (* needed for le_trans (for cases x = y /\ le y z and le x y /\ y = z) *)
  lemma lcp_same_index :
    forall a:array int, x:int.
      0 <= x <= a.length -> is_longest_common_prefix a x x (a.length - x)
MARCHE Claude's avatar
MARCHE Claude committed
222 223 224 225 226 227 228

  lemma le_trans :
    forall a:array int, x y z:int.
    0 <= x <= a.length /\ 0 <= y <= a.length /\
    0 <= z <= a.length /\ le a x y /\ le a y z -> le a x z


MARCHE Claude's avatar
MARCHE Claude committed
229 230
  (** spec of sorted in increasing prefix order *)
  use map.Map
MARCHE Claude's avatar
MARCHE Claude committed
231

232 233 234
  predicate sorted_sub (a:array int) (data:Map.map int int) (l u:int) =
    forall i1 i2 : int. l <= i1 <= i2 < u ->
      le a (Map.get data i1) (Map.get data i2)
MARCHE Claude's avatar
MARCHE Claude committed
235

MARCHE Claude's avatar
MARCHE Claude committed
236
  predicate sorted (a : array int) (data:array int) =
237
    sorted_sub a data.elts 0 data.length
MARCHE Claude's avatar
MARCHE Claude committed
238

MARCHE Claude's avatar
MARCHE Claude committed
239
  (** spec of permutation of elements *)
240
  use import array.ArrayPermut
MARCHE Claude's avatar
MARCHE Claude committed
241 242
  use map.MapInjection (* for the range function used below *)

MARCHE Claude's avatar
MARCHE Claude committed
243
  let sort (a:array int) (data : array int)
244
  requires { data.length = a.length }
MARCHE Claude's avatar
MARCHE Claude committed
245
  requires { MapInjection.range data.elts data.length }
MARCHE Claude's avatar
MARCHE Claude committed
246
  ensures { sorted a data }
247
  ensures { permut (old data) data }
MARCHE Claude's avatar
MARCHE Claude committed
248 249
  =
   'Init:
MARCHE Claude's avatar
MARCHE Claude committed
250
   for i = 0 to data.length - 1 do
MARCHE Claude's avatar
MARCHE Claude committed
251
     invariant { permut (at data 'Init) data   }
252
     invariant { sorted_sub a data.elts 0 i  }
MARCHE Claude's avatar
MARCHE Claude committed
253
     invariant { MapInjection.range data.elts data.length }
MARCHE Claude's avatar
MARCHE Claude committed
254 255 256
     let j = ref i in
     while !j > 0 && compare a data[!j-1] data[!j] > 0 do
       invariant { 0 <= !j <= i }
MARCHE Claude's avatar
MARCHE Claude committed
257
       invariant { MapInjection.range data.elts data.length }
MARCHE Claude's avatar
MARCHE Claude committed
258
       invariant { permut (at data 'Init) data   }
259 260
       invariant { sorted_sub a data.elts 0 !j }
       invariant { sorted_sub a data.elts !j (i+1) }
MARCHE Claude's avatar
MARCHE Claude committed
261 262
       invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
                     le a data[k1] data[k2] }
MARCHE Claude's avatar
MARCHE Claude committed
263 264 265 266 267
       'L:
       let b = !j - 1 in
       let t = data[!j] in
       data[!j] <- data[b];
       data[b] <- t;
MARCHE Claude's avatar
MARCHE Claude committed
268
       assert { exchange (at data 'L) data (!j-1) !j };
MARCHE Claude's avatar
MARCHE Claude committed
269
       decr j
MARCHE Claude's avatar
MARCHE Claude committed
270
     done
271
   done
MARCHE Claude's avatar
MARCHE Claude committed
272

MARCHE Claude's avatar
MARCHE Claude committed
273 274
end

MARCHE Claude's avatar
MARCHE Claude committed
275 276 277 278 279





MARCHE Claude's avatar
MARCHE Claude committed
280 281
(** {2 Third module: Suffix Array Data Structure } *) 

MARCHE Claude's avatar
MARCHE Claude committed
282

MARCHE Claude's avatar
MARCHE Claude committed
283 284 285 286
module SuffixArray

use import array.Array
use import LCP
MARCHE Claude's avatar
MARCHE Claude committed
287
use import PrefixSort
MARCHE Claude's avatar
MARCHE Claude committed
288
use map.MapInjection
MARCHE Claude's avatar
MARCHE Claude committed
289

MARCHE Claude's avatar
MARCHE Claude committed
290

MARCHE Claude's avatar
MARCHE Claude committed
291 292
predicate permutation (m:Map.map int int) (u : int) =
  MapInjection.range m u /\ MapInjection.injective m u
MARCHE Claude's avatar
MARCHE Claude committed
293

MARCHE Claude's avatar
MARCHE Claude committed
294 295 296 297
type suffixArray = {
    values : array int;
    suffixes : array int;
}
MARCHE Claude's avatar
MARCHE Claude committed
298 299 300
invariant { self.values.length = self.suffixes.length /\
  permutation self.suffixes.elts self.suffixes.length /\
  sorted self.values self.suffixes }
301

MARCHE Claude's avatar
MARCHE Claude committed
302
let select (s:suffixArray) (i:int) : int
MARCHE Claude's avatar
MARCHE Claude committed
303
  requires { 0 <= i < s.values.length }
MARCHE Claude's avatar
MARCHE Claude committed
304 305 306
  ensures { result = s.suffixes[i] }
  = s.suffixes[i]

MARCHE Claude's avatar
MARCHE Claude committed
307
use import array.ArrayPermut
MARCHE Claude's avatar
MARCHE Claude committed
308

MARCHE Claude's avatar
MARCHE Claude committed
309
(** needed to establish invariant in function [create] *)
MARCHE Claude's avatar
MARCHE Claude committed
310 311 312 313
lemma permut_permutation :
  forall a1 a2:array int.
  permut a1 a2 -> permutation a1.elts a1.length -> permutation a2.elts a2.length

MARCHE Claude's avatar
MARCHE Claude committed
314
(** constructor of suffixArray structure *)
MARCHE Claude's avatar
MARCHE Claude committed
315
let create (a:array int) : suffixArray
MARCHE Claude's avatar
MARCHE Claude committed
316
  ensures { result.values = a }
MARCHE Claude's avatar
MARCHE Claude committed
317
 =
MARCHE Claude's avatar
MARCHE Claude committed
318
 let n = a.length in
MARCHE Claude's avatar
MARCHE Claude committed
319
 let suf = Array.make n 0 in
MARCHE Claude's avatar
MARCHE Claude committed
320
 for i = 0 to n-1 do
321
   invariant { forall j:int. 0 <= j < i -> suf[j] = j }
MARCHE Claude's avatar
MARCHE Claude committed
322
   suf[i] <- i done;
MARCHE Claude's avatar
MARCHE Claude committed
323 324
 sort a suf;
 { values = a; suffixes = suf }
325

MARCHE Claude's avatar
MARCHE Claude committed
326
let lcp (s:suffixArray) (i:int) : int
MARCHE Claude's avatar
MARCHE Claude committed
327
  requires { 0 < i < s.values.length }
328
  ensures { is_longest_common_prefix s.values s.suffixes[i-1] s.suffixes[i] result }
MARCHE Claude's avatar
MARCHE Claude committed
329
  =
MARCHE Claude's avatar
MARCHE Claude committed
330
   LCP.lcp s.values s.suffixes[i] s.suffixes[i-1]
MARCHE Claude's avatar
MARCHE Claude committed
331

MARCHE Claude's avatar
MARCHE Claude committed
332
(*
MARCHE Claude's avatar
MARCHE Claude committed
333
let test () =
MARCHE Claude's avatar
MARCHE Claude committed
334 335 336
  let arr = Array.make 4 0 in
  arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
  let sa = create arr in
337 338 339 340
  assert { sa.suffixes[0] = 0 };
  assert { sa.suffixes[1] = 1 };
  assert { sa.suffixes[2] = 2 };
  assert { sa.suffixes[3] = 3 };
MARCHE Claude's avatar
MARCHE Claude committed
341
  let x = lcp sa 1 in
342
  check {x = 0};
MARCHE Claude's avatar
MARCHE Claude committed
343 344 345 346
  (* int[] brr = {1,2,3,5}; *)
  let brr = Array.make 4 0 in
  brr[0]<-1; brr[1]<-2; brr[2]<-3; brr[3]<-5;
  let sa = create brr in
MARCHE Claude's avatar
MARCHE Claude committed
347
  let x = lcp sa 1 in
348
  check {x = 0 (* TODO *)};
MARCHE Claude's avatar
MARCHE Claude committed
349 350 351 352
  (* int[] crr = {1,2,3,5}; *)
  let crr = Array.make 4 0 in
  crr[0]<-1; crr[1]<-2; crr[2]<-3; crr[3]<-5;
  let sa = create crr in
MARCHE Claude's avatar
MARCHE Claude committed
353
  let x = lcp sa 2 in
354
  check {x = 0 (* TODO *)};
MARCHE Claude's avatar
MARCHE Claude committed
355 356 357 358
  (* int[] drr = {1,2,3,3}; *)
  let drr = Array.make 4 0 in
  drr[0]<-1; drr[1]<-2; drr[2]<-3; drr[3]<-3;
  let sa = create drr in
MARCHE Claude's avatar
MARCHE Claude committed
359
  let x = lcp sa 2 in
360
  check {x = 0 (* TODO *)}
MARCHE Claude's avatar
MARCHE Claude committed
361
*)
362 363 364

end

MARCHE Claude's avatar
MARCHE Claude committed
365 366 367



MARCHE Claude's avatar
MARCHE Claude committed
368
(** {2 Fourth module: Longest Repeated Substring} *) 
MARCHE Claude's avatar
MARCHE Claude committed
369

MARCHE Claude's avatar
MARCHE Claude committed
370
module LRS 
MARCHE Claude's avatar
MARCHE Claude committed
371

MARCHE Claude's avatar
MARCHE Claude committed
372 373 374
  use import int.Int
  use import ref.Ref
  use import array.Array
375
  use map.MapInjection
MARCHE Claude's avatar
MARCHE Claude committed
376 377 378 379 380
  use import LCP
  use import PrefixSort
  use import SuffixArray


MARCHE Claude's avatar
MARCHE Claude committed
381
(** additional properties relating [le] and [longest_common_prefix] *)
MARCHE Claude's avatar
MARCHE Claude committed
382

MARCHE Claude's avatar
MARCHE Claude committed
383
(* needed for [lrs] function, last before last assert *)
MARCHE Claude's avatar
MARCHE Claude committed
384 385 386 387 388 389 390 391
lemma lcp_sym :
  forall a:array int, x y l:int.
     0 <= x <= a.length /\ 0 <= y <= a.length ->
       is_longest_common_prefix a x y l -> is_longest_common_prefix a y x l


use import int.MinMax

MARCHE Claude's avatar
MARCHE Claude committed
392 393
(** allows CVC to prove the next lemma *)
lemma le_le_common_prefix:
MARCHE Claude's avatar
MARCHE Claude committed
394 395 396 397
    forall a:array int, x y z l:int.
     le a x y /\ le a y z ->
     is_common_prefix a x z l -> is_common_prefix a y z l

MARCHE Claude's avatar
MARCHE Claude committed
398
(** proved by Alt-Ergo and CVC. But only by Alt-Ergo if previous lemma is removed *)
MARCHE Claude's avatar
MARCHE Claude committed
399 400 401 402 403 404
  lemma le_le_longest_common_prefix:
    forall a:array int, x y z l m :int.
     le a x y /\ le a y z ->
     is_longest_common_prefix a x z l /\ is_longest_common_prefix a y z m
     -> l <= m

MARCHE Claude's avatar
MARCHE Claude committed
405

MARCHE Claude's avatar
MARCHE Claude committed
406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433
  val solStart : ref int
  val solLength : ref int
  val ghost solStart2 : ref int

  let lrs (a:array int) : unit
    requires { a.length > 0 }
    ensures { 0 <= !solLength <= a.length }
    ensures { 0 <= !solStart <= a.length }
    ensures { 0 <= !solStart2 <= a.length /\ !solStart <> !solStart2 /\
              LCP.is_longest_common_prefix a !solStart !solStart2 !solLength }
    ensures { forall x y l:int.
                0 <= x < y < a.length /\
                LCP.is_longest_common_prefix a x y l ->
                !solLength >= l }
  =
    let sa = SuffixArray.create a in
    assert { permutation sa.SuffixArray.suffixes.elts
                         sa.SuffixArray.suffixes.length };
    solStart := 0;
    solLength := 0;
    solStart2 := a.length;
    for i=1 to a.length - 1 do
      invariant { 0 <= !solLength <= a.length }
      invariant { 0 <= !solStart <= a.length }
      invariant {
           0 <= !solStart2 <= a.length /\ !solStart <> !solStart2 /\
           LCP.is_longest_common_prefix a !solStart !solStart2 !solLength }
      invariant { forall j k l:int.
434 435 436 437
                  0 <= j < k < i /\
                  LCP.is_longest_common_prefix a
                    sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] l ->
                  !solLength >= l }
MARCHE Claude's avatar
MARCHE Claude committed
438 439 440 441 442 443 444 445
      let l = SuffixArray.lcp sa i in
      assert { forall j:int. 0 <= j < i ->
                  le a sa.SuffixArray.suffixes[j]
                     sa.SuffixArray.suffixes[i] };
      assert { forall j m:int. 0 <= j < i /\
                 LCP.is_longest_common_prefix a
                          sa.SuffixArray.suffixes[j]
                          sa.SuffixArray.suffixes[i] m ->
446
                  m <= l };
MARCHE Claude's avatar
MARCHE Claude committed
447
      assert { forall j k m:int. 0 <= j < k  < i-1 /\
448 449 450
                    LCP.is_longest_common_prefix a
                         sa.SuffixArray.suffixes[j]
                         sa.SuffixArray.suffixes[k] m -> !solLength >= m};
MARCHE Claude's avatar
MARCHE Claude committed
451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467
      if l > !solLength then begin
         solStart := SuffixArray.select sa i;
         solStart2 := SuffixArray.select sa (i-1);
         solLength := l
      end
    done;
    assert { let s = sa.SuffixArray.suffixes in
             MapInjection.surjective s.elts s.length };
    (** the following assert needs [lcp_sym] lemma *)
    assert { forall j k l:int.
                0 <= j < a.length /\ 0 <= k < a.length /\ j <> k /\
                 LCP.is_longest_common_prefix a 
                 sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] l ->
              !solLength >= l};
    assert { forall x y:int.
                0 <= x < y < a.length ->
                exists j k : int.
468 469
                  0 <= j < a.length /\ 0 <= k < a.length /\ j <> k /\
                  x = sa.SuffixArray.suffixes[j] /\
470
                  y = sa.SuffixArray.suffixes[k] };
MARCHE Claude's avatar
MARCHE Claude committed
471
    ()
472

MARCHE Claude's avatar
MARCHE Claude committed
473
(*
MARCHE Claude's avatar
MARCHE Claude committed
474 475 476 477
  let test () =
    let arr = Array.make 4 0 in
    arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-9;
    lrs arr;
478
    check { !solStart = 1 /\ !solLength = 1 }
MARCHE Claude's avatar
MARCHE Claude committed
479
*)
480 481 482

end