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

new program binary_search_c (manul model of a C program)

parent 677ca607
(* We illustrate the use of Why for the verification of C programs on
"the challenge of binary search" (Jon Bentley's Programming Pearls).
int binary_search(int* t, int n, int v) {
int l = 0, u = n-1;
while (l <= u) {
int m = (l + u) / 2;
if (t[m] < v)
l = m + 1;
else if (t[m] > v)
u = m - 1;
else
return m;
}
return -1;
*)
module M1
use import int.Int
use import int.ComputerDivision
use import module stdlib.Ref
type pointer
type memory
logic get memory pointer int : int
parameter mem : ref memory
exception Return int
let binary_search (t : pointer) (n : int) (v : int) =
{ forall k1 k2:int.
0 <= k1 <= k2 <= n-1 -> get mem t k1 <= get mem t k2 }
try
let l = ref 0 in
let u = ref (n-1) in
while !l <= !u do
invariant { 0 <= l and u <= n-1 and
forall k:int. 0 <= k < n -> get mem t k = v -> l <= k <= u }
variant { u-l }
let m = div (!l + !u) 2 in
if get !mem t m < v then l := m + 1
else if get !mem t m > v then u := m - 1
else raise (Return m)
done;
raise (Return (-1))
with Return r ->
r
end
{ (result >= 0 and get mem t result = v) or
(result = -1 and forall k:int. 0<=k<n -> get mem t k <> v) }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/binary_search_c.gui"
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