a better way to provide that the length of string is nonnegative

parent 9de8eea0
......@@ -163,8 +163,6 @@ 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.
......@@ -485,7 +485,7 @@ module OCaml
ensures { result <-> x = y }
val partial length (s: string) : int63
ensures { result = length s }
ensures { result = length s >= 0 }
val sub (s: string) (start: int63) (len: int63) : string
requires { 0 <= start <= length s }
......
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