examples/kmp.mlw

   1 (**************************************************************************)
   2 (*                                                                        *)
   3 (* Proof of the Knuth-Morris-Pratt Algorithm.                             *)
   4 (*                                                                        *)
   5 (* Jean-Christophe Filliâtre (LRI, Université Paris Sud)                  *)
   6 (* November 1998                                                          *)
   7 (*                                                                        *)
   8 (**************************************************************************)
   9
  10 module KnuthMorrisPratt
  11
  12   use int.Int
  13   use ref.Ref
  14   use array.Array
  15
  16   type char
  17   val eq (x y : char) : bool ensures { result = True <-> x = y }
  18
  19   predicate matches (a1: array char) (i1: int)
  20                     (a2: array char) (i2: int) (n: int) =
  21     0 <= i1 <= length a1 - n /\
  22     0 <= i2 <= length a2 - n /\
  23     forall i: int. 0 <= i < n -> a1[i1 + i] = a2[i2 + i]
  24
  25   lemma matches_empty:
  26     forall a1 a2: array char, i1 i2: int.
  27     0 <= i1 <= length a1 ->
  28     0 <= i2 <= length a2 ->
  29     matches a1 i1 a2 i2 0
  30
  31   lemma matches_right_extension:
  32     forall a1 a2: array char, i1 i2 n: int.
  33     matches a1 i1 a2 i2 n ->
  34     i1 <= length a1 - n - 1 ->
  35     i2 <= length a2 - n - 1 ->
  36     a1[i1 + n] = a2[i2 + n] ->
  37     matches a1 i1 a2 i2 (n + 1)
  38
  39   lemma matches_contradiction_at_first:
  40     forall a1 a2: array char, i1 i2 n: int.
  41     0 < n -> a1[i1] <> a2[i2] -> not (matches a1 i1 a2 i2 n)
  42
  43   lemma matches_contradiction_at_i :
  44     forall a1 a2: array char, i1 i2 i n: int.
  45     0 < n ->
  46     0 <= i < n ->
  47     a1[i1 + i] <> a2[i2 + i] -> not (matches a1 i1 a2 i2 n)
  48
  49   lemma matches_right_weakening:
  50     forall a1 a2: array char, i1 i2 n n': int.
  51     matches a1 i1 a2 i2 n -> n' < n -> matches a1 i1 a2 i2 n'
  52
  53   lemma matches_left_weakening:
  54     forall a1 a2: array char, i1 i2 n n': int.
  55     matches a1 (i1 - (n - n')) a2 (i2 - (n - n')) n ->
  56     n' < n -> matches a1 i1 a2 i2 n'
  57
  58   lemma matches_sym:
  59     forall a1 a2: array char, i1 i2 n: int.
  60     matches a1 i1 a2 i2 n -> matches a2 i2 a1 i1 n
  61
  62   lemma matches_trans:
  63     forall a1 a2 a3: array char, i1 i2 i3 n: int.
  64     matches a1 i1 a2 i2 n -> matches a2 i2 a3 i3 n -> matches a1 i1 a3 i3 n
  65
  66   predicate is_next (p: array char) (j n: int) =
  67     0 <= n < j /\
  68     matches p (j - n) p 0 n /\
  69     forall z: int. n < z < j -> not (matches p (j - z) p 0 z)
  70
  71   lemma next_iteration:
  72     forall p a: array char, i j n: int.
  73     0 < j < length p ->
  74     j <= i <= length a ->
  75     matches a (i - j) p 0 j -> is_next p j n -> matches a (i - n) p 0 n
  76
  77   lemma next_is_maximal:
  78     forall p a: array char, i j n k: int.
  79     0 < j < length p ->
  80     j <= i <= length a ->
  81     i - j < k < i - n ->
  82     matches a (i - j) p 0 j ->
  83     is_next p j n -> not (matches a k p 0 (length p))
  84
  85   lemma next_1_0:
  86     forall p: array char. 1 <= length p -> is_next p 1 0
  87
  88   (* We first compute a table next with the procedure initnext.
  89    * That table only depends on the pattern. *)
  90
  91   let initnext (p: array char)
  92     requires { 1 <= length p }
  93     ensures  { length result = length p &&
  94       forall j:int. 0 < j < p.length -> is_next p j result[j] }
  95   = let m = length p in
  96     let next = make m 0 in
  97     if 1 < m then begin
  98       next[1] <- 0;
  99       let i = ref 1 in
 100       let j = ref 0 in
 101       while !i < m - 1 do
 102         invariant { 0 <= !j < !i <= m }
 103         invariant { matches p (!i - !j) p 0 !j }
 104         invariant { forall z:int.
 105           !j+1 < z < !i+1 -> not matches p (!i + 1 - z) p 0 z }
 106         invariant { forall k:int. 0 < k <= !i -> is_next p k next[k] }
 107         variant { m - !i, !j }
 108         if eq p[!i] p[!j] then begin
 109           i := !i + 1; j := !j + 1; next[!i] <- !j
 110         end else
 111           if !j = 0 then begin i := !i + 1; next[!i] <- 0 end else j := next[!j]
 112       done
 113     end;
 114     next
 115
 116
 117   (* The algorithm looks for an occurrence of the pattern p in a text a
 118    * which is an array of length N.
 119    * The function kmp returns an index i within 0..N-1 if there is an occurrence
 120    * at the position i and N otherwise. *)
 121
 122   predicate first_occur (p a: array char) (r: int) =
 123     (0 <= r < length a -> matches a r p 0 (length p)) /\
 124     (forall k: int. 0 <= k < r -> not (matches a k p 0 (length p)))
 125
 126   let kmp (p a: array char)
 127     requires { 1 <= length p }
 128     ensures  { first_occur p a result }
 129   = let m = length p in
 130     let n = length a in
 131     let i = ref 0 in
 132     let j = ref 0 in
 133     let next = initnext p in
 134     while !j < m && !i < n do
 135       invariant { 0 <= !j <= m /\ !j <= !i <= n }
 136       invariant { matches a (!i - !j) p 0 !j }
 137       invariant { forall k:int. 0 <= k < !i - !j -> not (matches a k p 0 m) }
 138       variant { n - !i, !j }
 139       if eq a[!i] p[!j] then begin
 140         i := !i+1; j := !j+1
 141       end else
 142         if !j = 0 then i := !i+1 else j := next[!j]
 143     done;
 144     if !j = m then !i - m else !i
 145
 146 end