lcp.mlw 1014 Bytes
Newer Older
1 2 3 4 5 6 7 8 9

(* {1 The VerifyThis competition at FM2012: Problem 1}

   See {h <a href="http://fm2012.verifythis.org/challenges">this web page</a>}

   Authors: Jean-Christophe Filliâtre and Andrei Paskevich *)

module LCP

10 11 12
  use int.Int
  use ref.Refint
  use array.Array
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