improved session of string_search with a lemma

parent 2be948e8
......@@ -163,6 +163,8 @@ module BadShiftTable
= assert { (substring text j m)[i + m - j] = c } in
()
lemma length_nonneg: forall s. length s >= 0
let search (bst: bad_shift_table) (text: string) : int63
requires { length bst.pat <= length text }
ensures { -1 <= result <= length text - length bst.pat }
......
This diff is collapsed.
......@@ -86,6 +86,8 @@ module String
function length string : int
(** `length s` is the length of the string `s`. *)
(* axiom length_nonneg: forall s. length s >= 0 *)
axiom length_empty: length "" = 0
axiom length_concat: forall s1 s2.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment