why3/examples/string_search.mlw

(** String search

    Author: Jean-Christophe Filliâtre (CNRS)
    from a SPARK demo by Claire Dross (Adacore) *)

module Spec

  use int.Int
  use string.Char
  use string.String

  (* ***** all this to be moved to String? ***** *)
  predicate (==) (x y: string) = eq_string x y

  predicate matches (pat text: string) (p: int) =
    0 <= p <= length text - length pat /\
    substring text p (length pat) == pat
  (* ***** *)

end

module Occurs

  use int.Int
  use mach.int.Int63
  use string.String
  use string.Char
  use string.OCaml
  use Spec

  let partial occurs (pat text: string) (p: int63) : bool
    requires { 0 <= p <= length text - length pat }
    ensures  { result <-> matches pat text p }
  = let (ghost n) = length text in
    let m = length pat in
    for i = 0 to m - 1 do
      invariant { substring text p i == substring pat 0 i }
      assert { p + i <= n };
      if not (eq_char text[p + i] pat[i]) then return false
    done;
    true

end

module Naive

  use int.Int
  use mach.int.Int63
  use string.String
  use string.Char
  use string.OCaml
  use Spec
  use Occurs

  let partial search1 (pat text: string) : int63
    requires { length pat <= length text }
    ensures  { -1 <= result <= length text - length pat }
    ensures  { if result = -1 then
                 forall j. not (matches pat text j)
               else
                 matches pat text result }
  =
    let m = length pat in
    let n = length text in
    for i = 0 to n - m do
      invariant { forall j. 0 <= j < i -> substring text j m <> pat }
      if occurs pat text i then return i;
    done;
    -1

  let partial search2 (pat text: string) : int63
    requires { length pat <= length text }
    ensures  { -1 <= result <= length text - length pat }
    ensures  { if result = -1 then
                 forall j. not (matches pat text j)
               else
                 matches pat text result }
  =
    let m = length pat in
    let n = length text in
    for i = 0 to n - m do
      invariant { forall j. 0 <= j < i -> substring text j m <> pat }
      if sub text i m = pat then return i;
    done;
   -1

end

module BadShiftTable

  use int.Int
  use mach.int.Int63
  use string.String
  use string.Char
  use string.OCaml
  use Spec
  use Occurs

  clone fmap.MapImp as M with type key = char

  (*
   ------------------------+---+----------------
                           | C |
   -----+-----+---+--------+---+----------------
        | ... | C | ..!C.. |
        +-----+---+--------+
          0                  m
                <----sht c--->
  *)
  type bad_shift_table = {
    pat: string;
    sht: M.t int63;
  }
  invariant { forall j c. 0 <= j < length pat -> c = pat[j] ->
              M.mem c sht }
  invariant { forall c. M.mem c sht -> 1 <= sht c <= length pat + 1 }
  invariant { forall c. M.mem c sht -> forall j. 1 <= j < sht c ->
              pat[length pat - j] <> c }
  by { pat = ""; sht = M.create () }

  let partial make_table (pat: string) : bad_shift_table
  = let m = length pat in
    let sht = M.create () in
    for i = 0 to m - 1 do
      invariant { forall j c. 0 <= j < i -> c = pat[j] -> M.mem c sht }
      invariant { forall c. M.mem c sht -> 1 <= sht c <= m + 1 }
      invariant { forall c. M.mem c sht -> forall j. m - sht c < j < i ->
                  pat[j] <> c }
      M.add pat[i] (m - i) sht;
    done;
    { pat = pat; sht = sht }

  let lemma shift (bst: bad_shift_table) (text: string) (i: int63)
    requires { 0 <= i <= length text - length bst.pat }
    requires { M.mem text[i + length bst.pat] bst.sht }
    ensures  { forall j. i < j < i + M.find text[i + length bst.pat] bst.sht ->
               j <= length text - length bst.pat ->
               substring text j (length bst.pat) <> bst.pat }
  = let m = String.length bst.pat in
    let c = Char.get text (to_int i + m) in
    let lemma aux (j: int)
      requires { i < j < i + M.find c bst.sht }
      requires { j <= length text - m }
      ensures  { substring text j m <> bst.pat }
    = assert { (substring text j m)[i + m - j] = c };
      assert { bst.pat[m - (j - i)] <> c } in
    ()

  let lemma no_shift (bst: bad_shift_table) (text: string) (i: int63)
    requires { 0 <= i < length text - length bst.pat }
    requires { not (M.mem text[i + length bst.pat] bst.sht) }
    ensures  { forall j. i < j <= i + length bst.pat ->
               j <= length text - length bst.pat ->
               substring text j (length bst.pat) <> bst.pat }
  = let m = String.length bst.pat in
    let c = Char.get text (to_int i + m) in
    assert { forall j. 0 <= j < m -> bst.pat[j] <> c };
    let lemma aux (j: int)
      requires { i < j <= i + m }
      requires { j <= length text - m }
      ensures  { substring text j m <> bst.pat }
    = assert { (substring text j m)[i + m - j] = c } in
    ()

  let partial search (bst: bad_shift_table) (text: string) : int63
    requires { length bst.pat <= length text }
    ensures  { -1 <= result <= length text - length bst.pat }
    ensures  { if result = -1 then
                 forall j. not (matches bst.pat text j)
               else
                 matches bst.pat text result }
  = let pat = bst.pat in
    let m = length pat in
    let n = length text in
    let ref i = 0 in
    while i <= n - m do
      invariant { 0 <= i <= n }
      invariant { forall j. 0 <= j < i -> j <= n - m ->
                  substring text j m <> pat }
      variant   { n - m - i }
      if occurs pat text i then return i;
      if i = n - m then break;
      let c = text[i + m] in
      i <- i + if M.mem c bst.sht then (shift    bst text i; M.find c bst.sht)
                                  else (no_shift bst text i; m + 1)
    done;
   -1

end