Commit ffb4a169 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

binary_search_c: proof completed

parent 308f06a6
......@@ -141,7 +141,7 @@ module M3
exception Return int32
let binary_search (t : pointer) (n : int32) (v : int32) =
{ to_int n <= block_size mem t and
{ 0 <= to_int n <= block_size mem t and
forall k1 k2:int.
0 <= k1 <= k2 <= to_int n - 1 ->
to_int (get mem t k1) <= to_int (get mem t k2) }
......@@ -151,10 +151,15 @@ module M3
while to_int !l <= to_int !u do
invariant { 0 <= to_int l and to_int u <= to_int n - 1 and
forall k:int. 0 <= k < to_int n ->
get mem t k = v -> to_int l <= k <= to_int u }
to_int (get mem t k) = to_int v -> to_int l <= k <= to_int u }
variant { to_int u - to_int l }
let m = of_int (div (to_int (of_int (to_int !l + to_int !u)))
(to_int (of_int 2))) in
let m = of_int (to_int !l
+
to_int
(of_int
(div (to_int (of_int (to_int !u - to_int !l)))
(to_int (of_int 2)))))
in
if to_int (get_ t m) < to_int v then l := of_int (to_int m + 1)
else if to_int (get_ t m) > to_int v then u := of_int (to_int m - 1)
else raise (Return m)
......@@ -163,7 +168,7 @@ module M3
with Return r ->
r
end
{ (to_int result >= 0 and get mem t (to_int result) = v) or
{ (to_int result >= 0 and to_int (get mem t (to_int result)) = to_int v) or
(to_int result = -1 and forall k:int. 0<=k<to_int n -> get mem t k <> v) }
end
......
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