examples/string_search.mlw

   1
   2 (** String search
   3
   4     Author: Jean-Christophe Filliâtre (CNRS)
   5     from a SPARK demo by Claire Dross (Adacore) *)
   6
   7 module Spec
   8
   9   use int.Int
  10   use string.Char
  11   use string.String
  12
  13   (* ***** all this to be moved to String? ***** *)
  14   predicate (==) (x y: string) = eq_string x y
  15
  16   predicate matches (pat text: string) (p: int) =
  17     0 <= p <= length text - length pat /\
  18     substring text p (length pat) == pat
  19   (* ***** *)
  20
  21 end
  22
  23 module Occurs
  24
  25   use int.Int
  26   use mach.int.Int63
  27   use string.String
  28   use string.Char
  29   use string.OCaml
  30   use Spec
  31
  32   let partial occurs (pat text: string) (p: int63) : bool
  33     requires { 0 <= p <= length text - length pat }
  34     ensures  { result <-> matches pat text p }
  35   = let (ghost n) = length text in
  36     let m = length pat in
  37     for i = 0 to m - 1 do
  38       invariant { substring text p i == substring pat 0 i }
  39       assert { p + i <= n };
  40       if not (eq_char text[p + i] pat[i]) then return false
  41     done;
  42     true
  43
  44 end
  45
  46 module Naive
  47
  48   use int.Int
  49   use mach.int.Int63
  50   use string.String
  51   use string.Char
  52   use string.OCaml
  53   use Spec
  54   use Occurs
  55
  56   let partial search1 (pat text: string) : int63
  57     requires { length pat <= length text }
  58     ensures  { -1 <= result <= length text - length pat }
  59     ensures  { if result = -1 then
  60                  forall j. not (matches pat text j)
  61                else
  62                  matches pat text result }
  63   =
  64     let m = length pat in
  65     let n = length text in
  66     for i = 0 to n - m do
  67       invariant { forall j. 0 <= j < i -> substring text j m <> pat }
  68       if occurs pat text i then return i;
  69     done;
  70     -1
  71
  72   let partial search2 (pat text: string) : int63
  73     requires { length pat <= length text }
  74     ensures  { -1 <= result <= length text - length pat }
  75     ensures  { if result = -1 then
  76                  forall j. not (matches pat text j)
  77                else
  78                  matches pat text result }
  79   =
  80     let m = length pat in
  81     let n = length text in
  82     for i = 0 to n - m do
  83       invariant { forall j. 0 <= j < i -> substring text j m <> pat }
  84       if sub text i m = pat then return i;
  85     done;
  86    -1
  87
  88 end
  89
  90 module BadShiftTable
  91
  92   use int.Int
  93   use mach.int.Int63
  94   use string.String
  95   use string.Char
  96   use string.OCaml
  97   use Spec
  98   use Occurs
  99
 100   clone fmap.MapImp as M with type key = char
 101
 102   (*
 103    ------------------------+---+----------------
 104                            | C |
 105    -----+-----+---+--------+---+----------------
 106         | ... | C | ..!C.. |
 107         +-----+---+--------+
 108           0                  m
 109                 <----sht c--->
 110   *)
 111   type bad_shift_table = {
 112     pat: string;
 113     sht: M.t int63;
 114   }
 115   invariant { forall j c. 0 <= j < length pat -> c = pat[j] ->
 116               M.mem c sht }
 117   invariant { forall c. M.mem c sht -> 1 <= sht c <= length pat + 1 }
 118   invariant { forall c. M.mem c sht -> forall j. 1 <= j < sht c ->
 119               pat[length pat - j] <> c }
 120   by { pat = ""; sht = M.create () }
 121
 122   let partial make_table (pat: string) : bad_shift_table
 123   = let m = length pat in
 124     let sht = M.create () in
 125     for i = 0 to m - 1 do
 126       invariant { forall j c. 0 <= j < i -> c = pat[j] -> M.mem c sht }
 127       invariant { forall c. M.mem c sht -> 1 <= sht c <= m + 1 }
 128       invariant { forall c. M.mem c sht -> forall j. m - sht c < j < i ->
 129                   pat[j] <> c }
 130       M.add pat[i] (m - i) sht;
 131     done;
 132     { pat = pat; sht = sht }
 133
 134   let lemma shift (bst: bad_shift_table) (text: string) (i: int63)
 135     requires { 0 <= i <= length text - length bst.pat }
 136     requires { M.mem text[i + length bst.pat] bst.sht }
 137     ensures  { forall j. i < j < i + M.find text[i + length bst.pat] bst.sht ->
 138                j <= length text - length bst.pat ->
 139                substring text j (length bst.pat) <> bst.pat }
 140   = let m = String.length bst.pat in
 141     let c = Char.get text (to_int i + m) in
 142     let lemma aux (j: int)
 143       requires { i < j < i + M.find c bst.sht }
 144       requires { j <= length text - m }
 145       ensures  { substring text j m <> bst.pat }
 146     = assert { (substring text j m)[i + m - j] = c };
 147       assert { bst.pat[m - (j - i)] <> c } in
 148     ()
 149
 150   let lemma no_shift (bst: bad_shift_table) (text: string) (i: int63)
 151     requires { 0 <= i < length text - length bst.pat }
 152     requires { not (M.mem text[i + length bst.pat] bst.sht) }
 153     ensures  { forall j. i < j <= i + length bst.pat ->
 154                j <= length text - length bst.pat ->
 155                substring text j (length bst.pat) <> bst.pat }
 156   = let m = String.length bst.pat in
 157     let c = Char.get text (to_int i + m) in
 158     assert { forall j. 0 <= j < m -> bst.pat[j] <> c };
 159     let lemma aux (j: int)
 160       requires { i < j <= i + m }
 161       requires { j <= length text - m }
 162       ensures  { substring text j m <> bst.pat }
 163     = assert { (substring text j m)[i + m - j] = c } in
 164     ()
 165
 166   let partial search (bst: bad_shift_table) (text: string) : int63
 167     requires { length bst.pat <= length text }
 168     ensures  { -1 <= result <= length text - length bst.pat }
 169     ensures  { if result = -1 then
 170                  forall j. not (matches bst.pat text j)
 171                else
 172                  matches bst.pat text result }
 173   = let pat = bst.pat in
 174     let m = length pat in
 175     let n = length text in
 176     let ref i = 0 in
 177     while i <= n - m do
 178       invariant { 0 <= i <= n }
 179       invariant { forall j. 0 <= j < i -> j <= n - m ->
 180                   substring text j m <> pat }
 181       variant   { n - m - i }
 182       if occurs pat text i then return i;
 183       if i = n - m then break;
 184       let c = text[i + m] in
 185       i <- i + if M.mem c bst.sht then (shift    bst text i; M.find c bst.sht)
 186                                   else (no_shift bst text i; m + 1)
 187     done;
 188    -1
 189
 190 end