verifythis_fm2012_LRS.mlw 13.6 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 }
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
  use map.MapInjection
217 218 219
  (** [range a] is true when for each [i], [a[i]] is between [0] at
      [a.length-1] *)
  predicate range (a:array int) = MapInjection.range a.elts a.length
220 221 222 223

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

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

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

231 232
  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
233

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

237 238 239
  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
240

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

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

MARCHE Claude's avatar
MARCHE Claude committed
276 277
end

MARCHE Claude's avatar
MARCHE Claude committed
278 279 280 281 282





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

MARCHE Claude's avatar
MARCHE Claude committed
285

MARCHE Claude's avatar
MARCHE Claude committed
286 287
module SuffixArray

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

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

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

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

311
use array.ArrayPermut
MARCHE Claude's avatar
MARCHE Claude committed
312

MARCHE Claude's avatar
MARCHE Claude committed
313
(** needed to establish invariant in function [create] *)
314
lemma permut_permutation : forall a1 a2:array int.
315
  ArrayPermut.permut a1 a2 /\ permutation a1.elts a1.length ->
316
    permutation a2.elts a2.length
MARCHE Claude's avatar
MARCHE Claude committed
317

MARCHE Claude's avatar
MARCHE Claude committed
318
(** constructor of suffixArray structure *)
MARCHE Claude's avatar
MARCHE Claude committed
319
let create (a:array int) : suffixArray
MARCHE Claude's avatar
MARCHE Claude committed
320
  ensures { result.values = a }
321 322 323 324 325 326 327
= 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 }
328

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

335 336
end

337 338 339 340




341 342 343 344 345
module SuffixArray_test

use import array.Array
use import SuffixArray

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

end

MARCHE Claude's avatar
MARCHE Claude committed
379 380


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

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

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


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

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


MARCHE Claude's avatar
MARCHE Claude committed
404 405
(** allows CVC to prove the next lemma *)
lemma le_le_common_prefix:
MARCHE Claude's avatar
MARCHE Claude committed
406
    forall a:array int, x y z l:int.
MARCHE Claude's avatar
MARCHE Claude committed
407 408
     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
409

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

MARCHE Claude's avatar
MARCHE Claude committed
418

MARCHE Claude's avatar
MARCHE Claude committed
419 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
  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.
445 446 447 448
                  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
449 450 451 452 453 454 455 456 457 458
      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;
    (** the following assert needs [lcp_sym] lemma *)
    assert { forall j k l:int.
                0 <= j < a.length /\ 0 <= k < a.length /\ j <> k /\
459
                 LCP.is_longest_common_prefix a
MARCHE Claude's avatar
MARCHE Claude committed
460 461
                 sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] l ->
              !solLength >= l};
MARCHE Claude's avatar
MARCHE Claude committed
462
    (* we state explicitly that sa.suffixes is surjective *)
MARCHE Claude's avatar
MARCHE Claude committed
463 464 465
    assert { forall x y:int.
                0 <= x < y < a.length ->
                exists j k : int.
466 467
                  0 <= j < a.length /\ 0 <= k < a.length /\ j <> k /\
                  x = sa.SuffixArray.suffixes[j] /\
468
                  y = sa.SuffixArray.suffixes[k] };
MARCHE Claude's avatar
MARCHE Claude committed
469
    ()
470

471 472 473 474 475 476 477 478 479
end


module LRS_test

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

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

end