verifythis_fm2012_lcp.mlw 13.1 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
  (forall i:int. 0 <= i < l -> a[x+i] = a[y+i])

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
104

105
(*
MARCHE Claude's avatar
MARCHE Claude committed
106 107 108 109
function longest_common_prefix (a:array int) (x y:int) :int

axiom lcp_spec:
  forall a:array int, x y:int, l:int.
110
  0 <= x <= a.length /\ 0 <= y <= a.length ->
MARCHE Claude's avatar
MARCHE Claude committed
111 112
  (l = longest_common_prefix a x y <->
   is_common_prefix a x y l /\ not is_common_prefix a x y (l+1))
113 114 115 116
*)

predicate is_longest_common_prefix (a:array int) (x y:int) (l:int) =
  is_common_prefix a x y l /\ not (is_common_prefix a x y (l+1))
MARCHE Claude's avatar
MARCHE Claude committed
117

MARCHE Claude's avatar
MARCHE Claude committed
118 119 120 121 122
use import ref.Refint

let lcp (a:array int) (x y:int) : int
  requires { 0 <= x <= a.length }
  requires { 0 <= y <= a.length }
123
  ensures { is_longest_common_prefix a x y result }
MARCHE Claude's avatar
MARCHE Claude committed
124 125 126 127 128 129 130 131 132
  = 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


MARCHE Claude's avatar
MARCHE Claude committed
133
lemma lcp_is_cp :
134
  forall a:array int, x y l:int.
135
     0 <= x <= a.length /\ 0 <= y <= a.length ->
136
     is_longest_common_prefix a x y l ->
MARCHE Claude's avatar
MARCHE Claude committed
137 138
     is_common_prefix a x y l

MARCHE Claude's avatar
MARCHE Claude committed
139
lemma lcp_eq :
140
  forall a:array int, x y l:int.
141
     0 <= x <= a.length /\ 0 <= y <= a.length ->
142
     is_longest_common_prefix a x y l ->
MARCHE Claude's avatar
MARCHE Claude committed
143 144 145
     forall i:int. 0 <= i < l -> a[x+i] = a[y+i]

lemma lcp_refl :
MARCHE Claude's avatar
MARCHE Claude committed
146
  forall a:array int, x:int.
147
     0 <= x <= a.length -> is_longest_common_prefix a x x (a.length - x)
MARCHE Claude's avatar
MARCHE Claude committed
148

149
lemma lcp_sym :
150
  forall a:array int, x y l:int.
MARCHE Claude's avatar
MARCHE Claude committed
151
     0 <= x <= a.length /\ 0 <= y <= a.length ->
152
       is_longest_common_prefix a x y l -> is_longest_common_prefix a y x l
153

MARCHE Claude's avatar
MARCHE Claude committed
154 155 156 157
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
158
  assert { is_common_prefix arr 1 2 1};
159
  check { x = 1 };
MARCHE Claude's avatar
MARCHE Claude committed
160 161 162 163
  (* 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
164
  assert { is_common_prefix brr 1 2 0};
165
  check { x = 0 };
MARCHE Claude's avatar
MARCHE Claude committed
166 167 168 169
  (* 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
170
  assert { is_common_prefix crr 2 3 0};
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
  check {x = 1}
178

MARCHE Claude's avatar
MARCHE Claude committed
179

MARCHE Claude's avatar
MARCHE Claude committed
180
  predicate le (a : array int) (x y:int) =
MARCHE Claude's avatar
MARCHE Claude committed
181
     let n = a.length in
182
     0 <= x <= n /\ 0 <= y <= n /\
183 184 185
     exists l:int. is_common_prefix a x y l /\
     (x+l = n \/
      (x+l < n /\ y+l < n /\ a[x+l] <= a[y+l]))
MARCHE Claude's avatar
MARCHE Claude committed
186

MARCHE Claude's avatar
MARCHE Claude committed
187
  lemma le_refl :
MARCHE Claude's avatar
MARCHE Claude committed
188
    forall a:array int, x :int.
189
    0 <= x <= a.length -> le a x x
MARCHE Claude's avatar
MARCHE Claude committed
190

MARCHE Claude's avatar
MARCHE Claude committed
191 192
  lemma le_trans :
    forall a:array int, x y z:int.
193 194 195 196 197 198
    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
199

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

217 218 219
  use map.Map
  use map.MapPermut
  use map.MapInjection
MARCHE Claude's avatar
MARCHE Claude committed
220

221
  predicate permutation (m:Map.map int int) (u : int) =
222
    MapInjection.range m u /\ MapInjection.injective m u
MARCHE Claude's avatar
MARCHE Claude committed
223

224 225 226
  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
227

MARCHE Claude's avatar
MARCHE Claude committed
228
  predicate sorted (a : array int) (data:array int) =
229
    sorted_sub a data.elts 0 data.length
MARCHE Claude's avatar
MARCHE Claude committed
230

MARCHE Claude's avatar
MARCHE Claude committed
231
  let sort (a:array int) (data : array int)
232
  requires { data.length = a.length }
MARCHE Claude's avatar
MARCHE Claude committed
233
  requires { MapInjection.range data.elts data.length }
MARCHE Claude's avatar
MARCHE Claude committed
234
  ensures { sorted a data }
235
  ensures { permut (old data) data }
MARCHE Claude's avatar
MARCHE Claude committed
236 237
  =
   'Init:
MARCHE Claude's avatar
MARCHE Claude committed
238
   for i = 0 to data.length - 1 do
MARCHE Claude's avatar
MARCHE Claude committed
239
     invariant { permut (at data 'Init) data   }
240
     invariant { sorted_sub a data.elts 0 i  }
MARCHE Claude's avatar
MARCHE Claude committed
241
     invariant { MapInjection.range data.elts data.length }
MARCHE Claude's avatar
MARCHE Claude committed
242 243 244
     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
245
       invariant { MapInjection.range data.elts data.length }
MARCHE Claude's avatar
MARCHE Claude committed
246
       invariant { permut (at data 'Init) data   }
247 248
       invariant { sorted_sub a data.elts 0 !j }
       invariant { sorted_sub a data.elts !j (i+1) }
MARCHE Claude's avatar
MARCHE Claude committed
249 250
       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
251 252 253 254 255
       '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
256
       assert { exchange (at data 'L) data (!j-1) !j };
MARCHE Claude's avatar
MARCHE Claude committed
257
       decr j
MARCHE Claude's avatar
MARCHE Claude committed
258
     done
259
   done
MARCHE Claude's avatar
MARCHE Claude committed
260

MARCHE Claude's avatar
MARCHE Claude committed
261

262
(* additional properties relating le and longest_common_prefix, needed
MARCHE Claude's avatar
MARCHE Claude committed
263
   for SuffixArray and LRS
264 265 266

*)

MARCHE Claude's avatar
MARCHE Claude committed
267 268 269 270 271 272 273 274 275

(*
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.
276
  permut a1 a2 -> permutation a1.elts a1.length -> permutation a2.elts a2.length
MARCHE Claude's avatar
MARCHE Claude committed
277

MARCHE Claude's avatar
MARCHE Claude committed
278 279
  use import int.MinMax

280
(*
MARCHE Claude's avatar
MARCHE Claude committed
281 282 283 284 285
  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)
286 287 288 289 290
*)
  lemma lcp_le_le_aux:
    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
291

292
  lemma lcp_le_le:
293
    forall a:array int, x y z l m :int.
294
     le a x y /\ le a y z ->
295 296
     is_longest_common_prefix a x z l /\ is_longest_common_prefix a y z m
     -> l <= m
297

MARCHE Claude's avatar
MARCHE Claude committed
298 299
end

MARCHE Claude's avatar
MARCHE Claude committed
300 301 302 303 304





MARCHE Claude's avatar
MARCHE Claude committed
305 306 307 308 309 310 311 312 313 314 315
module SuffixArray

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

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

316 317
use map.MapInjection

MARCHE Claude's avatar
MARCHE Claude committed
318
predicate inv(s:suffixArray) =
MARCHE Claude's avatar
MARCHE Claude committed
319
  s.values.length = s.suffixes.length /\
320
  permutation s.suffixes.elts s.suffixes.length /\
MARCHE Claude's avatar
MARCHE Claude committed
321
  sorted s.values s.suffixes
MARCHE Claude's avatar
MARCHE Claude committed
322

MARCHE Claude's avatar
MARCHE Claude committed
323
let select (s:suffixArray) (i:int) : int
MARCHE Claude's avatar
MARCHE Claude committed
324 325 326 327
  requires { inv s /\ 0 <= i < s.values.length }
  ensures { result = s.suffixes[i] }
  = s.suffixes[i]

MARCHE Claude's avatar
MARCHE Claude committed
328
let create (a:array int) : suffixArray
329
  ensures { result.values = a /\ inv result }
MARCHE Claude's avatar
MARCHE Claude committed
330
 =
MARCHE Claude's avatar
MARCHE Claude committed
331
 let n = a.length in
MARCHE Claude's avatar
MARCHE Claude committed
332
 let suf = Array.make n 0 in
MARCHE Claude's avatar
MARCHE Claude committed
333
 for i = 0 to n-1 do
334
   invariant { forall j:int. 0 <= j < i -> suf[j] = j }
MARCHE Claude's avatar
MARCHE Claude committed
335
   suf[i] <- i done;
MARCHE Claude's avatar
MARCHE Claude committed
336 337
 sort a suf;
 { values = a; suffixes = suf }
338

MARCHE Claude's avatar
MARCHE Claude committed
339
let lcp (s:suffixArray) (i:int) : int
MARCHE Claude's avatar
MARCHE Claude committed
340 341
  requires { inv s }
  requires { 0 < i < s.values.length }
342
  ensures { is_longest_common_prefix s.values s.suffixes[i-1] s.suffixes[i] result }
MARCHE Claude's avatar
MARCHE Claude committed
343
  =
MARCHE Claude's avatar
MARCHE Claude committed
344
   LCP.lcp s.values s.suffixes[i] s.suffixes[i-1]
MARCHE Claude's avatar
MARCHE Claude committed
345

MARCHE Claude's avatar
MARCHE Claude committed
346
(*
MARCHE Claude's avatar
MARCHE Claude committed
347 348 349 350
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
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 382




MARCHE Claude's avatar
MARCHE Claude committed
383
module LRS "longest repeated substring"
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
389
  use LCP
MARCHE Claude's avatar
MARCHE Claude committed
390 391 392 393
  use SuffixArray

    val solStart : ref int
    val solLength : ref int
MARCHE Claude's avatar
MARCHE Claude committed
394
    val ghost solStart2 : ref int
MARCHE Claude's avatar
MARCHE Claude committed
395

MARCHE Claude's avatar
MARCHE Claude committed
396
    let lrs (a:array int) : unit
397 398 399
      requires { a.length > 0 }
      ensures { 0 <= !solLength <= a.length }
      ensures { 0 <= !solStart <= a.length }
MARCHE Claude's avatar
MARCHE Claude committed
400
      ensures { 0 <= !solStart2 <= a.length /\ !solStart <> !solStart2 /\
401 402 403 404 405
                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 }
406
    =
MARCHE Claude's avatar
MARCHE Claude committed
407
      let sa = SuffixArray.create a in
408 409
      assert { LCP.permutation sa.SuffixArray.suffixes.elts
                               sa.SuffixArray.suffixes.length };
MARCHE Claude's avatar
MARCHE Claude committed
410 411
      solStart := 0;
      solLength := 0;
MARCHE Claude's avatar
MARCHE Claude committed
412
      solStart2 := a.length;
MARCHE Claude's avatar
MARCHE Claude committed
413
      for i=1 to a.length - 1 do
414 415
        invariant { 0 <= !solLength <= a.length }
        invariant { 0 <= !solStart <= a.length }
416
        invariant {
417 418 419 420 421 422 423 424
             0 <= !solStart2 <= a.length /\ !solStart <> !solStart2 /\
             LCP.is_longest_common_prefix a !solStart !solStart2 !solLength }
        invariant { forall j k l:int.
                  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
425
         let l = SuffixArray.lcp sa i in
426 427 428
         assert { forall j:int. 0 <= j < i ->
                    LCP.le a sa.SuffixArray.suffixes[j]
                             sa.SuffixArray.suffixes[i] };
429 430
         assert { forall j m:int. 0 <= j < i /\
                    LCP.is_longest_common_prefix a
431
                             sa.SuffixArray.suffixes[j]
432 433 434 435 436 437
                             sa.SuffixArray.suffixes[i] m ->
                  m <= l };
         assert { forall j k m:int. 0 <= j < k  < i-1 /\
                    LCP.is_longest_common_prefix a
                         sa.SuffixArray.suffixes[j]
                         sa.SuffixArray.suffixes[k] m -> !solLength >= m};
MARCHE Claude's avatar
MARCHE Claude committed
438 439
         if l > !solLength then begin
            solStart := SuffixArray.select sa i;
MARCHE Claude's avatar
MARCHE Claude committed
440
            solStart2 := SuffixArray.select sa (i-1);
MARCHE Claude's avatar
MARCHE Claude committed
441 442
            solLength := l
         end
443 444 445
      done;
      assert { let s = sa.SuffixArray.suffixes in
               MapInjection.surjective s.elts s.length };
446 447 448 449 450
      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};
451 452 453 454 455
      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] /\
456 457
                  y = sa.SuffixArray.suffixes[k] };
      ()
458

MARCHE Claude's avatar
MARCHE Claude committed
459
(*
MARCHE Claude's avatar
MARCHE Claude committed
460 461 462 463
  let test () =
    let arr = Array.make 4 0 in
    arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-9;
    lrs arr;
464
    check { !solStart = 1 /\ !solLength = 1 }
MARCHE Claude's avatar
MARCHE Claude committed
465
*)
466 467 468 469

end


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