verifythis_fm2012_lcp.mlw 13.7 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 99
predicate is_common_prefix (a:array int) (x y l:int) =
  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
(** [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]
111 112 113
    are identical. *)
predicate is_longest_common_prefix (a:array int) (x y l:int) =
  is_common_prefix a x y l /\
114 115
  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 137 138
  = 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;
    !l

139 140 141 142 143

end

module LCP_test

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

use import array.Array
use import LCP

MARCHE Claude's avatar
MARCHE Claude committed
149
let test () =
MARCHE Claude's avatar
MARCHE Claude committed
150 151 152
  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
153
  assert { is_common_prefix arr 1 2 1};
154
  assert { not is_common_prefix arr 1 2 2};
155
  check { x = 1 };
MARCHE Claude's avatar
MARCHE Claude committed
156 157 158 159
  (* 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
160
  assert { is_common_prefix brr 1 2 0};
161
  assert { not is_common_prefix brr 1 2 1};
162
  check { x = 0 };
MARCHE Claude's avatar
MARCHE Claude committed
163 164 165 166
  (* 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
167
  assert { is_common_prefix crr 2 3 0};
168
  assert { not is_common_prefix crr 2 3 1};
169
  check { x = 0 };
MARCHE Claude's avatar
MARCHE Claude committed
170 171 172 173
  (* 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
174
  assert { is_common_prefix drr 2 3 1};
175
  assert { not is_common_prefix drr 2 3 2};
176
  check {x = 1}
177

MARCHE Claude's avatar
MARCHE Claude committed
178

MARCHE Claude's avatar
MARCHE Claude committed
179 180
end

181 182
(** {2 Second module: sorting suffixes } *)
module SuffixSort
MARCHE Claude's avatar
MARCHE Claude committed
183

MARCHE Claude's avatar
MARCHE Claude committed
184 185
  use import int.Int
  use import ref.Refint
MARCHE Claude's avatar
MARCHE Claude committed
186
  use import array.Array
MARCHE Claude's avatar
MARCHE Claude committed
187
  use LCP
MARCHE Claude's avatar
MARCHE Claude committed
188 189

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

196 197


MARCHE Claude's avatar
MARCHE Claude committed
198
(** comparison function, that decides the order of prefixes *)
MARCHE Claude's avatar
MARCHE Claude committed
199
let compare (a:array int) (x y:int) : int
200 201
  requires { 0 <= x <= a.length }
  requires { 0 <= y <= a.length }
MARCHE Claude's avatar
MARCHE Claude committed
202
  ensures { result = 0 -> x = y }
203 204
  ensures { result < 0 -> lt a x y }
  ensures { result > 0 -> lt a y x }
MARCHE Claude's avatar
MARCHE Claude committed
205
  =
206
  if x = y then 0 else
MARCHE Claude's avatar
MARCHE Claude committed
207
  let n = a.length in
MARCHE Claude's avatar
MARCHE Claude committed
208
  let l = LCP.lcp a x y in
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

216 217 218 219 220 221
  (** for the [range] predicate used below *)
  use map.MapInjection

  (** for the [permut] predicate (permutation of elements) *)
  use array.ArrayPermut

MARCHE Claude's avatar
MARCHE Claude committed
222
  predicate le (a : array int) (x y:int) = x = y \/ lt a x y
223

MARCHE Claude's avatar
MARCHE Claude committed
224 225 226
  (* 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.
MARCHE Claude's avatar
MARCHE Claude committed
227
      0 <= x <= a.length -> LCP.is_longest_common_prefix a x x (a.length - x)
MARCHE Claude's avatar
MARCHE Claude committed
228

229 230
  lemma le_trans : forall a:array int, x y z:int.
    le a x y /\ le a y z -> le a x z
MARCHE Claude's avatar
MARCHE Claude committed
231

MARCHE Claude's avatar
MARCHE Claude committed
232 233
  (** spec of sorted in increasing prefix order *)
  use map.Map
MARCHE Claude's avatar
MARCHE Claude committed
234

235 236 237
  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
238

MARCHE Claude's avatar
MARCHE Claude committed
239
  predicate sorted (a : array int) (data:array int) =
240
    sorted_sub a data.elts 0 data.length
MARCHE Claude's avatar
MARCHE Claude committed
241

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

MARCHE Claude's avatar
MARCHE Claude committed
274 275
end

MARCHE Claude's avatar
MARCHE Claude committed
276 277 278 279 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

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

MARCHE Claude's avatar
MARCHE Claude committed
286
use import int.Int
MARCHE Claude's avatar
MARCHE Claude committed
287
use import array.Array
MARCHE Claude's avatar
MARCHE Claude committed
288 289 290
use LCP
use SuffixSort
use map.Map
MARCHE Claude's avatar
MARCHE Claude committed
291
use map.MapInjection
MARCHE Claude's avatar
MARCHE Claude committed
292

MARCHE Claude's avatar
MARCHE Claude committed
293

MARCHE Claude's avatar
MARCHE Claude committed
294 295
predicate permutation (m:Map.map int int) (u : int) =
  MapInjection.range m u /\ MapInjection.injective m u
MARCHE Claude's avatar
MARCHE Claude committed
296

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

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

MARCHE Claude's avatar
MARCHE Claude committed
310
use import array.ArrayPermut
MARCHE Claude's avatar
MARCHE Claude committed
311

MARCHE Claude's avatar
MARCHE Claude committed
312
(** needed to establish invariant in function [create] *)
313 314 315
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
316

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

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

334 335
end

336 337 338 339




340 341 342 343 344
module SuffixArray_test

use import array.Array
use import SuffixArray

MARCHE Claude's avatar
MARCHE Claude committed
345
(*
MARCHE Claude's avatar
MARCHE Claude committed
346
let test () =
MARCHE Claude's avatar
MARCHE Claude committed
347 348 349
  let arr = Array.make 4 0 in
  arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
  let sa = create arr in
350 351 352 353
  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
354
  let x = lcp sa 1 in
355
  check {x = 0};
MARCHE Claude's avatar
MARCHE Claude committed
356 357 358 359
  (* 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
360
  let x = lcp sa 1 in
361
  check {x = 0 (* TODO *)};
MARCHE Claude's avatar
MARCHE Claude committed
362 363 364 365
  (* 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
366
  let x = lcp sa 2 in
367
  check {x = 0 (* TODO *)};
MARCHE Claude's avatar
MARCHE Claude committed
368 369 370 371
  (* 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
372
  let x = lcp sa 2 in
373
  check {x = 0 (* TODO *)}
MARCHE Claude's avatar
MARCHE Claude committed
374
*)
375 376 377

end

MARCHE Claude's avatar
MARCHE Claude committed
378 379


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

382
module LRS
MARCHE Claude's avatar
MARCHE Claude committed
383

MARCHE Claude's avatar
MARCHE Claude committed
384 385 386
  use import int.Int
  use import ref.Ref
  use import array.Array
387
  use map.MapInjection
MARCHE Claude's avatar
MARCHE Claude committed
388
  use LCP
389
  use SuffixSort
MARCHE Claude's avatar
MARCHE Claude committed
390
  use SuffixArray
MARCHE Claude's avatar
MARCHE Claude committed
391 392


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

MARCHE Claude's avatar
MARCHE Claude committed
395
(* needed for [lrs] function, last before last assert *)
MARCHE Claude's avatar
MARCHE Claude committed
396 397 398
lemma lcp_sym :
  forall a:array int, x y l:int.
     0 <= x <= a.length /\ 0 <= y <= a.length ->
399
       LCP.is_longest_common_prefix a x y l ->
MARCHE Claude's avatar
MARCHE Claude committed
400
       LCP.is_longest_common_prefix a y x l
MARCHE Claude's avatar
MARCHE Claude committed
401 402 403 404


use import int.MinMax

MARCHE Claude's avatar
MARCHE Claude committed
405 406
(** allows CVC to prove the next lemma *)
lemma le_le_common_prefix:
MARCHE Claude's avatar
MARCHE Claude committed
407
    forall a:array int, x y z l:int.
MARCHE Claude's avatar
MARCHE Claude committed
408 409
     SuffixSort.le a x y /\ SuffixSort.le a y z ->
     LCP.is_common_prefix a x z l -> LCP.is_common_prefix a y z l
MARCHE Claude's avatar
MARCHE Claude committed
410

MARCHE Claude's avatar
MARCHE Claude committed
411
(** proved by Alt-Ergo and CVC. But only by Alt-Ergo if previous lemma is removed *)
MARCHE Claude's avatar
MARCHE Claude committed
412 413
  lemma le_le_longest_common_prefix:
    forall a:array int, x y z l m :int.
MARCHE Claude's avatar
MARCHE Claude committed
414
     SuffixSort.le a x y /\ SuffixSort.le a y z ->
415
     LCP.is_longest_common_prefix a x z l /\
MARCHE Claude's avatar
MARCHE Claude committed
416 417
     LCP.is_longest_common_prefix a y z m
       -> l <= m
MARCHE Claude's avatar
MARCHE Claude committed
418

MARCHE Claude's avatar
MARCHE Claude committed
419

MARCHE Claude's avatar
MARCHE Claude committed
420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445
  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
    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.
446 447 448 449
                  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
450 451 452 453 454 455 456
      let l = SuffixArray.lcp sa i in
      if l > !solLength then begin
         solStart := SuffixArray.select sa i;
         solStart2 := SuffixArray.select sa (i-1);
         solLength := l
      end
    done;
MARCHE Claude's avatar
MARCHE Claude committed
457
    (* we state explicitly that sa.suffixes is surjective *)
MARCHE Claude's avatar
MARCHE Claude committed
458 459 460 461 462
    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 /\
463
                 LCP.is_longest_common_prefix a
MARCHE Claude's avatar
MARCHE Claude committed
464 465 466 467 468
                 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.
469 470
                  0 <= j < a.length /\ 0 <= k < a.length /\ j <> k /\
                  x = sa.SuffixArray.suffixes[j] /\
471
                  y = sa.SuffixArray.suffixes[k] };
MARCHE Claude's avatar
MARCHE Claude committed
472
    ()
473

474 475 476 477 478 479 480 481 482
end


module LRS_test

use import array.Array
use import ref.Ref
use import LRS

MARCHE Claude's avatar
MARCHE Claude committed
483
(*
MARCHE Claude's avatar
MARCHE Claude committed
484 485 486 487
  let test () =
    let arr = Array.make 4 0 in
    arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-9;
    lrs arr;
488
    check { !solStart = 1 /\ !solLength = 1 }
MARCHE Claude's avatar
MARCHE Claude committed
489
*)
490 491 492

end