verifythis_fm2012_LRS.mlw 15.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 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 119
(** This lemma helps to 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
120
lemma longest_common_prefix_succ:
121 122 123
  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

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

127
(** the first function, that computes the longest common prefix *)
MARCHE Claude's avatar
MARCHE Claude committed
128 129 130
let lcp (a:array int) (x y:int) : int
  requires { 0 <= x <= a.length }
  requires { 0 <= y <= a.length }
131
  ensures { is_longest_common_prefix a x y result }
MARCHE Claude's avatar
MARCHE Claude committed
132 133 134 135
  = 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 }
136
      variant { n - !l }
MARCHE Claude's avatar
MARCHE Claude committed
137 138 139 140
      incr l
    done;
    !l

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

MARCHE Claude's avatar
MARCHE Claude committed
181 182 183 184 185 186
  exception BenchFailure

  let bench () raises { BenchFailure -> true } =
    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
187 188
    if x <> 1 then raise BenchFailure;
    x
MARCHE Claude's avatar
MARCHE Claude committed
189

MARCHE Claude's avatar
MARCHE Claude committed
190
end
MARCHE Claude's avatar
MARCHE Claude committed
191

MARCHE Claude's avatar
MARCHE Claude committed
192

193 194
(** {2 Second module: sorting suffixes } *)
module SuffixSort
MARCHE Claude's avatar
MARCHE Claude committed
195

MARCHE Claude's avatar
MARCHE Claude committed
196 197
  use import int.Int
  use import ref.Refint
MARCHE Claude's avatar
MARCHE Claude committed
198
  use import array.Array
MARCHE Claude's avatar
MARCHE Claude committed
199
  use LCP
MARCHE Claude's avatar
MARCHE Claude committed
200 201

  (** order by prefix *)
202
  predicate lt (a : array int) (x y:int) =
MARCHE Claude's avatar
MARCHE Claude committed
203
     let n = a.length in
204
     0 <= x <= n /\ 0 <= y <= n /\
MARCHE Claude's avatar
MARCHE Claude committed
205
     exists l:int. LCP.is_common_prefix a x y l /\
206
     (y+l < n /\ (x+l = n \/ a[x+l] < a[y+l]))
MARCHE Claude's avatar
MARCHE Claude committed
207

208 209


MARCHE Claude's avatar
MARCHE Claude committed
210
(** comparison function, that decides the order of prefixes *)
MARCHE Claude's avatar
MARCHE Claude committed
211
let compare (a:array int) (x y:int) : int
212 213
  requires { 0 <= x <= a.length }
  requires { 0 <= y <= a.length }
214
  ensures { result = 0 -> x = y }
215 216
  ensures { result < 0 -> lt a x y }
  ensures { result > 0 -> lt a y x }
MARCHE Claude's avatar
MARCHE Claude committed
217
  =
218
  if x = y then 0 else
MARCHE Claude's avatar
MARCHE Claude committed
219
  let n = a.length in
MARCHE Claude's avatar
MARCHE Claude committed
220
  let l = LCP.lcp a x y in
MARCHE Claude's avatar
MARCHE Claude committed
221 222 223 224
  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
225 226
  absurd

MARCHE Claude's avatar
MARCHE Claude committed
227

228
  use map.MapInjection
229 230 231
  (** [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
232 233 234 235

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

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

MARCHE Claude's avatar
MARCHE Claude committed
238 239 240
  (* 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
241
      0 <= x <= a.length -> LCP.is_longest_common_prefix a x x (a.length - x)
MARCHE Claude's avatar
MARCHE Claude committed
242

243 244
  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
245

MARCHE Claude's avatar
MARCHE Claude committed
246 247
  (** spec of sorted in increasing prefix order *)
  use map.Map
MARCHE Claude's avatar
MARCHE Claude committed
248

249 250 251
  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
252

253
  predicate sorted (a : array int) (data:array int) =
254
    sorted_sub a data.elts 0 data.length
MARCHE Claude's avatar
MARCHE Claude committed
255

256
let sort (a:array int) (data : array int)
257
  requires { data.length = a.length }
258
  requires { range data }
259
  ensures { sorted a data }
260
  ensures { ArrayPermut.permut_all (old data) data }
MARCHE Claude's avatar
MARCHE Claude committed
261 262
  =
   'Init:
MARCHE Claude's avatar
MARCHE Claude committed
263
   for i = 0 to data.length - 1 do
264
     invariant { ArrayPermut.permut_all (at data 'Init) data   }
265
     invariant { sorted_sub a data.elts 0 i  }
266
     invariant { range data }
MARCHE Claude's avatar
MARCHE Claude committed
267 268 269
     let j = ref i in
     while !j > 0 && compare a data[!j-1] data[!j] > 0 do
       invariant { 0 <= !j <= i }
270
       invariant { range data }
271
       invariant { ArrayPermut.permut_all (at data 'Init) data   }
272 273
       invariant { sorted_sub a data.elts 0 !j }
       invariant { sorted_sub a data.elts !j (i+1) }
274 275
       invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
                     le a data[k1] data[k2] }
276
       variant { !j }
MARCHE Claude's avatar
MARCHE Claude committed
277 278 279 280 281
       'L:
       let b = !j - 1 in
       let t = data[!j] in
       data[!j] <- data[b];
       data[b] <- t;
282
       assert { ArrayPermut.exchange (at data 'L) data (!j-1) !j };
MARCHE Claude's avatar
MARCHE Claude committed
283
       decr j
284 285 286
     done;
     (* needed to prove the invariant [sorted_sub a data.elts 0 i] *)
     assert { !j > 0 -> le a data[!j-1] data[!j] }
287
   done
MARCHE Claude's avatar
MARCHE Claude committed
288

289

MARCHE Claude's avatar
MARCHE Claude committed
290 291
end

MARCHE Claude's avatar
MARCHE Claude committed
292

293 294 295 296 297 298 299 300 301 302 303 304 305 306
module SuffixSort_test

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

  exception BenchFailure

  let bench () raises { BenchFailure -> true } =
    let arr = Array.make 4 0 in
    (* [7,8,8,6] *)
    arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-6;
    let suf = Array.make 4 0 in
307 308 309 310
    for i = 0 to 3 do 
      invariant { forall j:int. 0 <= j < i -> suf[j] = j }
      suf[i] <- i 
    done;
311 312 313 314 315
    SuffixSort.sort arr suf;
    (* should be [3,0,2,1] *)
    if suf[0] <> 3 then raise BenchFailure;
    if suf[1] <> 0 then raise BenchFailure;
    if suf[2] <> 2 then raise BenchFailure;
316 317
    if suf[3] <> 1 then raise BenchFailure;
    suf
318 319

end
MARCHE Claude's avatar
MARCHE Claude committed
320 321 322 323




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

MARCHE Claude's avatar
MARCHE Claude committed
326

MARCHE Claude's avatar
MARCHE Claude committed
327 328
module SuffixArray

MARCHE Claude's avatar
MARCHE Claude committed
329
use import int.Int
MARCHE Claude's avatar
MARCHE Claude committed
330
use import array.Array
MARCHE Claude's avatar
MARCHE Claude committed
331 332 333
use LCP
use SuffixSort
use map.Map
MARCHE Claude's avatar
MARCHE Claude committed
334
use map.MapInjection
MARCHE Claude's avatar
MARCHE Claude committed
335

MARCHE Claude's avatar
MARCHE Claude committed
336 337
predicate permutation (m:Map.map int int) (u : int) =
  MapInjection.range m u /\ MapInjection.injective m u
MARCHE Claude's avatar
MARCHE Claude committed
338

MARCHE Claude's avatar
MARCHE Claude committed
339 340 341 342
type suffixArray = {
    values : array int;
    suffixes : array int;
}
MARCHE Claude's avatar
MARCHE Claude committed
343 344
invariant { self.values.length = self.suffixes.length /\
  permutation self.suffixes.elts self.suffixes.length /\
MARCHE Claude's avatar
MARCHE Claude committed
345
  SuffixSort.sorted self.values self.suffixes }
346

MARCHE Claude's avatar
MARCHE Claude committed
347
let select (s:suffixArray) (i:int) : int
MARCHE Claude's avatar
MARCHE Claude committed
348
  requires { 0 <= i < s.values.length }
MARCHE Claude's avatar
MARCHE Claude committed
349 350 351
  ensures { result = s.suffixes[i] }
  = s.suffixes[i]

352
use array.ArrayPermut
MARCHE Claude's avatar
MARCHE Claude committed
353

MARCHE Claude's avatar
MARCHE Claude committed
354
(** needed to establish invariant in function [create] *)
355
lemma permut_permutation : forall a1 a2:array int.
356
  ArrayPermut.permut_all a1 a2 /\ permutation a1.elts a1.length ->
357
    permutation a2.elts a2.length
MARCHE Claude's avatar
MARCHE Claude committed
358

MARCHE Claude's avatar
MARCHE Claude committed
359
(** constructor of suffixArray structure *)
MARCHE Claude's avatar
MARCHE Claude committed
360
let create (a:array int) : suffixArray
MARCHE Claude's avatar
MARCHE Claude committed
361
  ensures { result.values = a }
362 363 364 365 366 367 368
= 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 }
369

MARCHE Claude's avatar
MARCHE Claude committed
370
let lcp (s:suffixArray) (i:int) : int
MARCHE Claude's avatar
MARCHE Claude committed
371
  requires { 0 < i < s.values.length }
372
  ensures { LCP.is_longest_common_prefix s.values
MARCHE Claude's avatar
MARCHE Claude committed
373
              s.suffixes[i-1] s.suffixes[i] result }
374
= LCP.lcp s.values s.suffixes[i] s.suffixes[i-1]
MARCHE Claude's avatar
MARCHE Claude committed
375

376 377
end

378 379 380



381 382 383 384 385
module SuffixArray_test

use import array.Array
use import SuffixArray

MARCHE Claude's avatar
MARCHE Claude committed
386
(*
MARCHE Claude's avatar
MARCHE Claude committed
387
let test () =
MARCHE Claude's avatar
MARCHE Claude committed
388 389 390
  let arr = Array.make 4 0 in
  arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
  let sa = create arr in
391 392 393 394
  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
395
  let x = lcp sa 1 in
396
  check {x = 0};
MARCHE Claude's avatar
MARCHE Claude committed
397 398 399 400
  (* 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
401
  let x = lcp sa 1 in
402
  check {x = 0 (* TODO *)};
MARCHE Claude's avatar
MARCHE Claude committed
403 404 405 406
  (* 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
407
  let x = lcp sa 2 in
408
  check {x = 0 (* TODO *)};
MARCHE Claude's avatar
MARCHE Claude committed
409 410 411 412
  (* 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
413
  let x = lcp sa 2 in
414
  check {x = 0 (* TODO *)}
MARCHE Claude's avatar
MARCHE Claude committed
415
*)
416

MARCHE Claude's avatar
MARCHE Claude committed
417 418 419 420
  exception BenchFailure

  let bench () raises { BenchFailure -> true } =
    let arr = Array.make 4 0 in
421 422
    (* [7,8,8,6] *)
    arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-6;
MARCHE Claude's avatar
MARCHE Claude committed
423
    let sa = create arr in
424 425
    if sa.suffixes[0] <> 3 then raise BenchFailure;
    if sa.suffixes[1] <> 0 then raise BenchFailure;
MARCHE Claude's avatar
MARCHE Claude committed
426
    if sa.suffixes[2] <> 2 then raise BenchFailure;
427 428
    if sa.suffixes[3] <> 1 then raise BenchFailure;
    sa
MARCHE Claude's avatar
MARCHE Claude committed
429

430
end
MARCHE Claude's avatar
MARCHE Claude committed
431 432


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

435
module LRS
MARCHE Claude's avatar
MARCHE Claude committed
436

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


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

MARCHE Claude's avatar
MARCHE Claude committed
448
(* needed for [lrs] function, last before last assert *)
MARCHE Claude's avatar
MARCHE Claude committed
449 450 451
lemma lcp_sym :
  forall a:array int, x y l:int.
     0 <= x <= a.length /\ 0 <= y <= a.length ->
452
       LCP.is_longest_common_prefix a x y l ->
MARCHE Claude's avatar
MARCHE Claude committed
453
       LCP.is_longest_common_prefix a y x l
MARCHE Claude's avatar
MARCHE Claude committed
454 455


MARCHE Claude's avatar
MARCHE Claude committed
456 457
(** allows CVC to prove the next lemma *)
lemma le_le_common_prefix:
MARCHE Claude's avatar
MARCHE Claude committed
458
    forall a:array int, x y z l:int.
MARCHE Claude's avatar
MARCHE Claude committed
459 460
     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
461

MARCHE Claude's avatar
MARCHE Claude committed
462
(** proved by Alt-Ergo and CVC. But only by Alt-Ergo if previous lemma is removed *)
MARCHE Claude's avatar
MARCHE Claude committed
463 464
  lemma le_le_longest_common_prefix:
    forall a:array int, x y z l m :int.
MARCHE Claude's avatar
MARCHE Claude committed
465
     SuffixSort.le a x y /\ SuffixSort.le a y z ->
466
     LCP.is_longest_common_prefix a x z l /\
MARCHE Claude's avatar
MARCHE Claude committed
467 468
     LCP.is_longest_common_prefix a y z m
       -> l <= m
MARCHE Claude's avatar
MARCHE Claude committed
469

MARCHE Claude's avatar
MARCHE Claude committed
470

MARCHE Claude's avatar
MARCHE Claude committed
471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496
  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.
497 498 499 500
                  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
501 502 503 504 505 506 507 508 509 510
      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 /\
511
                 LCP.is_longest_common_prefix a
MARCHE Claude's avatar
MARCHE Claude committed
512 513
                 sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] l ->
              !solLength >= l};
MARCHE Claude's avatar
MARCHE Claude committed
514
    (* we state explicitly that sa.suffixes is surjective *)
MARCHE Claude's avatar
MARCHE Claude committed
515 516 517
    assert { forall x y:int.
                0 <= x < y < a.length ->
                exists j k : int.
518 519
                  0 <= j < a.length /\ 0 <= k < a.length /\ j <> k /\
                  x = sa.SuffixArray.suffixes[j] /\
520
                  y = sa.SuffixArray.suffixes[k] };
MARCHE Claude's avatar
MARCHE Claude committed
521
    ()
522

523 524 525 526 527
end


module LRS_test

528 529 530 531 532
  use import array.Array
  use import ref.Ref
  use import LRS

  exception BenchFailure
533

534
  let bench () raises { BenchFailure -> true } =
MARCHE Claude's avatar
MARCHE Claude committed
535
    let arr = Array.make 4 0 in
536 537
    (* [7,8,8,6] *)
    arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-6;
MARCHE Claude's avatar
MARCHE Claude committed
538
    lrs arr;
539
    if !solStart <> 1 then raise BenchFailure;
540 541
    if !solLength <> 1 then raise BenchFailure;
    (!solStart, !solLength)
542 543

end