lcp.mlw 1014 Bytes
 Jean-Christophe Filliatre committed Jan 29, 2013 1 2 3 4 5 6 7 8 9 `````` (* {1 The VerifyThis competition at FM2012: Problem 1} See {h this web page} Authors: Jean-Christophe Filliâtre and Andrei Paskevich *) module LCP `````` Andrei Paskevich committed Jun 15, 2018 10 11 12 `````` use int.Int use ref.Refint use array.Array `````` Jean-Christophe Filliatre committed Jan 29, 2013 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 `````` predicate eqseq (a: array int) (x y: int) (len: int) = 0 <= len /\ x + len <= length a /\ y + len <= length a /\ forall i: int. 0 <= i < len -> a[x + i] = a[y + i] lemma not_eqseq: forall a: array int, x y: int, i: int. 0 <= i -> a[x + i] <> a[y + i] -> forall len: int. i < len -> not (eqseq a x y len) let lcp (a: array int) (x: int) (y: int) : int requires { 0 <= x < length a /\ 0 <= y < length a } ensures { eqseq a x y result } ensures { forall len: int. result < len -> not (eqseq a x y len) } = let l = ref 0 in while x + !l < length a && y + !l < length a && a[x + !l] = a[y + !l] do invariant { eqseq a x y !l } variant { length a - !l } incr l done; !l end``````