verifythis_fm2012_lcp.mlw 14.5 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 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;
        while (x+l<a.length && y+l<a.length && a[x+l]==a[y+l]) {
            l++;
        }
        return l;
    }






MARCHE Claude's avatar
MARCHE Claude committed
34
ADVANCED
35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
========



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
56
array.
57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75

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.

*)

MARCHE Claude's avatar
MARCHE Claude committed
76 77 78


module LCP "longest common prefix"
MARCHE Claude's avatar
MARCHE Claude committed
79 80

use import int.Int
81
use import array.Array
82 83
use import array.ArrayPermut

MARCHE Claude's avatar
MARCHE Claude committed
84

MARCHE Claude's avatar
MARCHE Claude committed
85 86
predicate is_common_prefix (a:array int) (x y:int) (l:int) =
  0 <= l /\ x+l <= a.length /\ y+l <= a.length /\
MARCHE Claude's avatar
MARCHE Claude committed
87 88 89 90
  (forall i:int. 0 <= i < l -> a[x+i] = a[y+i])

lemma common_prefix_eq:
  forall a:array int, x:int.
91
     0 <= x <= a.length -> is_common_prefix a x x (a.length - x)
MARCHE Claude's avatar
MARCHE Claude committed
92 93 94

lemma common_prefix_eq2:
  forall a:array int, x:int.
95
     0 <= x <= a.length -> not (is_common_prefix a x x (a.length - x + 1))
MARCHE Claude's avatar
MARCHE Claude committed
96 97 98 99 100 101 102 103 104 105

lemma not_common_prefix_if_last_different:
  forall a:array int, x y:int, l:int.
    0 < l /\ x+l < a.length /\ y+l < a.length /\ a[x+(l-1)] <> a[y+(l-1)] ->
      not is_common_prefix a x y l

function longest_common_prefix (a:array int) (x y:int) :int

axiom lcp_spec:
  forall a:array int, x y:int, l:int.
106
  0 <= x <= a.length /\ 0 <= y <= a.length ->
MARCHE Claude's avatar
MARCHE Claude committed
107 108
  (l = longest_common_prefix a x y <->
   is_common_prefix a x y l /\ not is_common_prefix a x y (l+1))
MARCHE Claude's avatar
MARCHE Claude committed
109

MARCHE Claude's avatar
MARCHE Claude committed
110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
use import ref.Refint

let lcp (a:array int) (x y:int) : int
  requires { 0 <= x <= a.length }
  requires { 0 <= y <= a.length }
  ensures { result = longest_common_prefix a x y }
  = 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;
    assert { is_common_prefix a x y !l };
    assert { x + !l < n /\ y + !l < n -> a[x + !l] <> a[y + !l] };
    assert { not is_common_prefix a x y (!l+1) };
    !l


MARCHE Claude's avatar
MARCHE Claude committed
128 129
lemma lcp_is_cp :
  forall a:array int, x y:int.
130
     0 <= x <= a.length /\ 0 <= y <= a.length ->
MARCHE Claude's avatar
MARCHE Claude committed
131 132 133
     let l = longest_common_prefix a x y in
     is_common_prefix a x y l

MARCHE Claude's avatar
MARCHE Claude committed
134
lemma lcp_eq :
MARCHE Claude's avatar
MARCHE Claude committed
135
  forall a:array int, x y:int.
136
     0 <= x <= a.length /\ 0 <= y <= a.length ->
MARCHE Claude's avatar
MARCHE Claude committed
137 138 139 140
     let l = longest_common_prefix a x y in
     forall i:int. 0 <= i < l -> a[x+i] = a[y+i]

lemma lcp_refl :
MARCHE Claude's avatar
MARCHE Claude committed
141
  forall a:array int, x:int.
142
     0 <= x <= a.length -> longest_common_prefix a x x = a.length - x
MARCHE Claude's avatar
MARCHE Claude committed
143

144 145
lemma lcp_sym :
  forall a:array int, x y:int.
MARCHE Claude's avatar
MARCHE Claude committed
146
     0 <= x <= a.length /\ 0 <= y <= a.length ->
147 148
       longest_common_prefix a x y = longest_common_prefix a y x

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

MARCHE Claude's avatar
MARCHE Claude committed
174

MARCHE Claude's avatar
MARCHE Claude committed
175
  predicate le (a : array int) (x y:int) =
MARCHE Claude's avatar
MARCHE Claude committed
176
     let n = a.length in
177
     0 <= x <= n /\ 0 <= y <= n /\
MARCHE Claude's avatar
MARCHE Claude committed
178 179 180 181
     let l = longest_common_prefix a x y in
     x+l = n \/
     (x+l < n /\ y+l < n /\ a[x+l] <= a[y+l])

MARCHE Claude's avatar
MARCHE Claude committed
182
  lemma le_refl :
MARCHE Claude's avatar
MARCHE Claude committed
183
    forall a:array int, x :int.
184
    0 <= x <= a.length -> le a x x
MARCHE Claude's avatar
MARCHE Claude committed
185

MARCHE Claude's avatar
MARCHE Claude committed
186 187
  lemma le_trans :
    forall a:array int, x y z:int.
188 189 190 191 192 193
    0 <= x <= a.length /\ 0 <= y <= a.length /\
    0 <= z <= a.length /\ le a x y /\ le a y z -> le a x z

  lemma le_asym :
    forall a:array int, x y:int.
    0 <= x <= a.length /\ 0 <= y <= a.length /\ not (le a x y) -> le a y x
MARCHE Claude's avatar
MARCHE Claude committed
194

MARCHE Claude's avatar
MARCHE Claude committed
195
let compare (a:array int) (x y:int) : int
196 197
  requires { 0 <= x <= a.length }
  requires { 0 <= y <= a.length }
MARCHE Claude's avatar
MARCHE Claude committed
198 199 200
  ensures { result = 0 -> x = y }
  ensures { result < 0 -> le a x y }
  ensures { result > 0 -> le a y x }
MARCHE Claude's avatar
MARCHE Claude committed
201
  =
202
  if x = y then 0 else
MARCHE Claude's avatar
MARCHE Claude committed
203 204
  let n = a.length in
  let l = lcp a x y in
MARCHE Claude's avatar
MARCHE Claude committed
205
  assert { is_common_prefix a x y l };
MARCHE Claude's avatar
MARCHE Claude committed
206 207 208 209
  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
210 211
  absurd

MARCHE Claude's avatar
MARCHE Claude committed
212 213 214
  predicate sorted_sub (a : array int) (data:array int) (l u:int) =
    forall i1 i2 : int. l <= i1 <= i2 < u -> le a data[i1] data[i2]

MARCHE Claude's avatar
MARCHE Claude committed
215
(*
MARCHE Claude's avatar
MARCHE Claude committed
216 217
  lemma sorted_le:
    forall a data: array int, l u i x:int.
MARCHE Claude's avatar
MARCHE Claude committed
218
    l <= i < u /\ sorted_sub a data l u /\ le a x data[l] ->
MARCHE Claude's avatar
MARCHE Claude committed
219 220 221 222
    le a x data[i]

  lemma sorted_ge:
    forall a data: array int, l u i x:int.
MARCHE Claude's avatar
MARCHE Claude committed
223
    sorted_sub a data l u /\ le a data[u-1] x /\ l <= i < u ->
MARCHE Claude's avatar
MARCHE Claude committed
224 225
    le a data[i] x

MARCHE Claude's avatar
MARCHE Claude committed
226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242
  lemma sorted_sub_sub:
    forall a data:array int, l u l' u':int.
    l <= l' /\ u' <= u ->
    sorted_sub a data l u ->
    sorted_sub a data l' u'

  lemma sorted_sub_add:
    forall a data:array int, l u:int.
    sorted_sub a data (l+1) u /\ le a data[l] data[l+1] ->
    sorted_sub a data l u

  lemma sorted_sub_concat:
    forall a data:array int, l m u:int.
    l <= m <= u /\ sorted_sub a data l m /\ sorted_sub a data m u /\
    le a data[m-1] data[m] ->
    sorted_sub a data l u

MARCHE Claude's avatar
MARCHE Claude committed
243 244 245 246 247 248 249 250 251
  lemma sorted_sub_set:
    forall a data:array int, l u i v:int.
    sorted_sub a data l u /\ u <= i ->
    sorted_sub a (data[i<-v]) l u

  lemma sorted_sub_set2:
    forall a data:array int, l u i v:int.
    sorted_sub a data l u /\ u <= i ->
    sorted_sub a { length = a.length; elts = Map.set data.elts i v } l u
MARCHE Claude's avatar
MARCHE Claude committed
252 253 254 255 256 257 258 259 260 261 262 263 264 265
*)

use map.Map
use map.MapPermut
use map.MapInjection

predicate map_permutation (m:Map.map int int) (u : int) =
  MapInjection.range m u /\
  MapInjection.injective m u

predicate permutation (a:array int) =
  map_permutation a.elts a.length


MARCHE Claude's avatar
MARCHE Claude committed
266

MARCHE Claude's avatar
MARCHE Claude committed
267 268
  predicate sorted (a : array int) (data:array int) =
    sorted_sub a data 0 data.length
MARCHE Claude's avatar
MARCHE Claude committed
269

MARCHE Claude's avatar
MARCHE Claude committed
270
  let sort (a:array int) (data : array int)
271
  requires { data.length = a.length }
MARCHE Claude's avatar
MARCHE Claude committed
272
  requires { MapInjection.range data.elts data.length }
MARCHE Claude's avatar
MARCHE Claude committed
273
  ensures { sorted a data }
274
  ensures { permut (old data) data }
MARCHE Claude's avatar
MARCHE Claude committed
275 276
  =
   'Init:
MARCHE Claude's avatar
MARCHE Claude committed
277
   for i = 0 to data.length - 1 do
MARCHE Claude's avatar
MARCHE Claude committed
278
     invariant { permut (at data 'Init) data   }
MARCHE Claude's avatar
MARCHE Claude committed
279
     invariant { sorted_sub a data 0 i  }
MARCHE Claude's avatar
MARCHE Claude committed
280
     invariant { MapInjection.range data.elts data.length }
MARCHE Claude's avatar
MARCHE Claude committed
281 282 283
     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
284
       invariant { MapInjection.range data.elts data.length }
MARCHE Claude's avatar
MARCHE Claude committed
285
       invariant { permut (at data 'Init) data   }
MARCHE Claude's avatar
MARCHE Claude committed
286 287 288 289
       invariant { sorted_sub a data 0 !j }
       invariant { sorted_sub a data !j (i+1) }
       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
290
       'L:
MARCHE Claude's avatar
MARCHE Claude committed
291
(*
MARCHE Claude's avatar
MARCHE Claude committed
292
       assert { le a data[!j] data[!j-1] };
MARCHE Claude's avatar
MARCHE Claude committed
293 294 295
       assert { forall k:int. !j+1 <= k <= i -> le a data[!j-1] data[k] };
       assert { sorted_sub a data 0 (!j-1) };
       assert { sorted_sub a data (!j+1) (i+1) };
MARCHE Claude's avatar
MARCHE Claude committed
296
*)
MARCHE Claude's avatar
MARCHE Claude committed
297 298 299
       let b = !j - 1 in
       let t = data[!j] in
       data[!j] <- data[b];
MARCHE Claude's avatar
MARCHE Claude committed
300
(*
MARCHE Claude's avatar
MARCHE Claude committed
301
       assert { sorted_sub a data 0 (!j-1) };
MARCHE Claude's avatar
MARCHE Claude committed
302 303 304
       assert { sorted_sub a data (!j+1) (i+1) };
       assert { forall k:int. !j <= k <= i -> le a data[!j] data[k] };
       assert { sorted_sub a data !j (i+1) };
MARCHE Claude's avatar
MARCHE Claude committed
305
*)
MARCHE Claude's avatar
MARCHE Claude committed
306
       data[b] <- t;
MARCHE Claude's avatar
MARCHE Claude committed
307
(*
MARCHE Claude's avatar
MARCHE Claude committed
308 309
       assert { le a data[!j-1] data[!j] };
       assert { forall k:int. !j <= k <=i -> le a data[!j] data[k] };
MARCHE Claude's avatar
MARCHE Claude committed
310
       assert { sorted_sub a data 0 (!j-1) };
MARCHE Claude's avatar
MARCHE Claude committed
311
       assert { sorted_sub a data !j (i+1) };
MARCHE Claude's avatar
MARCHE Claude committed
312 313
*)
       assert { exchange (at data 'L) data (!j-1) !j };
MARCHE Claude's avatar
MARCHE Claude committed
314
       decr j
MARCHE Claude's avatar
MARCHE Claude committed
315 316
     done
(*;
MARCHE Claude's avatar
MARCHE Claude committed
317
     assert { !j > 0 -> le a data[!j-1] data[!j] }
MARCHE Claude's avatar
MARCHE Claude committed
318
*)   done
MARCHE Claude's avatar
MARCHE Claude committed
319

MARCHE Claude's avatar
MARCHE Claude committed
320

321
(* additional properties relating le and longest_common_prefix, needed
MARCHE Claude's avatar
MARCHE Claude committed
322
   for SuffixArray and LRS
323 324 325

*)

MARCHE Claude's avatar
MARCHE Claude committed
326 327 328 329 330 331 332 333 334 335 336

(*
lemma map_permut_permutation :
  forall m1 m2:Map.map int int, u:int [MapPermut.permut_sub m1 m2 0 u].
  MapPermut.permut_sub m1 m2 0 u -> map_permutation m1 u -> map_permutation m2 u
*)

lemma permut_permutation :
  forall a1 a2:array int.
  permut a1 a2 -> permutation a1 -> permutation a2

MARCHE Claude's avatar
MARCHE Claude committed
337 338 339 340 341 342 343 344
  use import int.MinMax

  lemma lcp_le_le_min:
    forall a:array int, x y z:int [le a x y, le a y z].
     le a x y /\ le a y z ->
     longest_common_prefix a x z =
       min (longest_common_prefix a x y) (longest_common_prefix a y z)

345 346 347 348 349
  lemma lcp_le_le:
    forall a:array int, x y z:int.
     le a x y /\ le a y z ->
     longest_common_prefix a x z <= longest_common_prefix a y z

MARCHE Claude's avatar
MARCHE Claude committed
350 351
end

MARCHE Claude's avatar
MARCHE Claude committed
352 353 354 355 356





MARCHE Claude's avatar
MARCHE Claude committed
357 358 359 360 361 362 363 364 365 366 367
module SuffixArray

use import int.Int
use import array.Array
use import LCP

type suffixArray = {
    values : array int;
    suffixes : array int;
}

368 369
use map.MapInjection

MARCHE Claude's avatar
MARCHE Claude committed
370
predicate inv(s:suffixArray) =
MARCHE Claude's avatar
MARCHE Claude committed
371 372 373
  s.values.length = s.suffixes.length /\
  permutation s.suffixes /\
  sorted s.values s.suffixes
MARCHE Claude's avatar
MARCHE Claude committed
374

MARCHE Claude's avatar
MARCHE Claude committed
375
let select (s:suffixArray) (i:int) : int
MARCHE Claude's avatar
MARCHE Claude committed
376 377 378 379
  requires { inv s /\ 0 <= i < s.values.length }
  ensures { result = s.suffixes[i] }
  = s.suffixes[i]

MARCHE Claude's avatar
MARCHE Claude committed
380
let create (a:array int) : suffixArray
MARCHE Claude's avatar
MARCHE Claude committed
381
  requires { a.length >= 0 }
382
  ensures { result.values = a /\ inv result }
MARCHE Claude's avatar
MARCHE Claude committed
383
 =
MARCHE Claude's avatar
MARCHE Claude committed
384
 let n = a.length in
MARCHE Claude's avatar
MARCHE Claude committed
385
 let suf = Array.make n 0 in
MARCHE Claude's avatar
MARCHE Claude committed
386
 for i = 0 to n-1 do
387
   invariant { forall j:int. 0 <= j < i -> suf[j] = j }
MARCHE Claude's avatar
MARCHE Claude committed
388
   suf[i] <- i done;
MARCHE Claude's avatar
MARCHE Claude committed
389 390
 sort a suf;
 { values = a; suffixes = suf }
391

MARCHE Claude's avatar
MARCHE Claude committed
392
let lcp (s:suffixArray) (i:int) : int
MARCHE Claude's avatar
MARCHE Claude committed
393 394
  requires { inv s }
  requires { 0 < i < s.values.length }
395
  ensures { result =
MARCHE Claude's avatar
MARCHE Claude committed
396
            longest_common_prefix s.values s.suffixes[i-1] s.suffixes[i] }
MARCHE Claude's avatar
MARCHE Claude committed
397
  =
MARCHE Claude's avatar
MARCHE Claude committed
398
   LCP.lcp s.values s.suffixes[i] s.suffixes[i-1]
MARCHE Claude's avatar
MARCHE Claude committed
399

MARCHE Claude's avatar
MARCHE Claude committed
400
(*
MARCHE Claude's avatar
MARCHE Claude committed
401 402 403 404
let test2 () =
  let arr = Array.make 4 0 in
  arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
  let sa = create arr in
405 406 407 408
  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
409
  let x = lcp sa 1 in
410
  check {x = 0};
MARCHE Claude's avatar
MARCHE Claude committed
411 412 413 414
  (* 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
415
  let x = lcp sa 1 in
416
  check {x = 0 (* TODO *)};
MARCHE Claude's avatar
MARCHE Claude committed
417 418 419 420
  (* 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
421
  let x = lcp sa 2 in
422
  check {x = 0 (* TODO *)};
MARCHE Claude's avatar
MARCHE Claude committed
423 424 425 426
  (* 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
427
  let x = lcp sa 2 in
428
  check {x = 0 (* TODO *)}
MARCHE Claude's avatar
MARCHE Claude committed
429
*)
430 431 432

end

MARCHE Claude's avatar
MARCHE Claude committed
433 434 435 436




MARCHE Claude's avatar
MARCHE Claude committed
437
module LRS "longest repeated substring"
MARCHE Claude's avatar
MARCHE Claude committed
438

MARCHE Claude's avatar
MARCHE Claude committed
439 440 441
  use import int.Int
  use import ref.Ref
  use import array.Array
442
  use map.MapInjection
443
  use LCP
MARCHE Claude's avatar
MARCHE Claude committed
444 445 446 447
  use SuffixArray

    val solStart : ref int
    val solLength : ref int
MARCHE Claude's avatar
MARCHE Claude committed
448
    val ghost solStart2 : ref int
MARCHE Claude's avatar
MARCHE Claude committed
449

MARCHE Claude's avatar
MARCHE Claude committed
450
    let lrs (a:array int) : unit
451 452 453
      requires { a.length > 0 }
      ensures { 0 <= !solLength <= a.length }
      ensures { 0 <= !solStart <= a.length }
MARCHE Claude's avatar
MARCHE Claude committed
454 455
      ensures { 0 <= !solStart2 <= a.length /\ !solStart <> !solStart2 /\
                !solLength = LCP.longest_common_prefix a !solStart !solStart2 }
456 457 458
      ensures { forall x y:int.
                  0 <= x < y < a.length ->
                  !solLength >= LCP.longest_common_prefix a x y }
459
    =
MARCHE Claude's avatar
MARCHE Claude committed
460
      let sa = SuffixArray.create a in
461
      assert { LCP.permutation sa.SuffixArray.suffixes };
MARCHE Claude's avatar
MARCHE Claude committed
462 463
      solStart := 0;
      solLength := 0;
MARCHE Claude's avatar
MARCHE Claude committed
464
      solStart2 := a.length;
MARCHE Claude's avatar
MARCHE Claude committed
465
      for i=1 to a.length - 1 do
466 467
        invariant { 0 <= !solLength <= a.length }
        invariant { 0 <= !solStart <= a.length }
MARCHE Claude's avatar
MARCHE Claude committed
468 469 470
        invariant { 
                  0 <= !solStart2 <= a.length /\ !solStart <> !solStart2 /\
                  !solLength = LCP.longest_common_prefix a !solStart !solStart2 }
471 472 473 474
        invariant { forall j k:int.
                  0 <= j < k < i ->
                  !solLength >= LCP.longest_common_prefix a
                    sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] }
MARCHE Claude's avatar
MARCHE Claude committed
475
         let l = SuffixArray.lcp sa i in
476 477 478 479 480 481
         assert { forall j:int. 0 <= j < i ->
                    LCP.le a sa.SuffixArray.suffixes[j]
                             sa.SuffixArray.suffixes[i] };
         assert { forall j:int. 0 <= j < i ->
                    LCP.longest_common_prefix a
                             sa.SuffixArray.suffixes[j]
MARCHE Claude's avatar
MARCHE Claude committed
482
                             sa.SuffixArray.suffixes[i]
483 484 485 486 487
                  <= l };
         assert { forall j k:int. 0 <= j < k  < i-1 ->
                    !solLength >= LCP.longest_common_prefix a
                             sa.SuffixArray.suffixes[j]
                             sa.SuffixArray.suffixes[k] };
MARCHE Claude's avatar
MARCHE Claude committed
488 489
         if l > !solLength then begin
            solStart := SuffixArray.select sa i;
MARCHE Claude's avatar
MARCHE Claude committed
490
            solStart2 := SuffixArray.select sa (i-1);
MARCHE Claude's avatar
MARCHE Claude committed
491 492
            solLength := l
         end
493 494 495 496 497 498 499 500 501 502 503 504 505
      done;
      assert { let s = sa.SuffixArray.suffixes in
               MapInjection.surjective s.elts s.length };
      assert { forall j k:int.
                  0 <= j < a.length /\ 0 <= k < a.length /\ j <> k ->
                  !solLength >= LCP.longest_common_prefix a
                    sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] };
      assert { forall x y:int.
                  0 <= x < y < a.length ->
                  exists j k : int.
                  0 <= j < a.length /\ 0 <= k < a.length /\ j <> k /\
                  x = sa.SuffixArray.suffixes[j] /\
                  y = sa.SuffixArray.suffixes[k] }
506

MARCHE Claude's avatar
MARCHE Claude committed
507
(*
MARCHE Claude's avatar
MARCHE Claude committed
508 509 510 511
  let test () =
    let arr = Array.make 4 0 in
    arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-9;
    lrs arr;
512
    check { !solStart = 1 /\ !solLength = 1 }
MARCHE Claude's avatar
MARCHE Claude committed
513
*)
514 515 516 517

end


MARCHE Claude's avatar
MARCHE Claude committed
518
(* Based on code by Robert Sedgewick and Kevin Wayne. *)