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

binary_search_c: wip

parent b417e82a
......@@ -55,6 +55,119 @@ module M1
end
(* next step: we want to add array bound checking
to do so, we
1. introduce the notion of blocksize in the model
2. add a program function "get_" with a precondition, to be used in the code
(instead of the pure function "get")
*)
module M2
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
logic block_size memory pointer : int
parameter get_ :p : pointer -> ofs : int ->
{ 0 <= ofs < block_size mem p }
int reads mem
{ result = get mem p ofs }
exception Return int
let binary_search (t : pointer) (n : int) (v : int) =
{ n <= block_size mem t and
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_ t m < v then l := m + 1
else if get_ 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
(* Finally, let us prove the absence of arithmetic overflow
*)
module M3
use import int.Int
use import int.ComputerDivision
use import module stdlib.Ref
type int32
logic to_int int32 : int
axiom int32_domain : forall x:int32. -2147483648 <= to_int x <= 2147483647
parameter of_int :
x:int -> { -2147483648 <= x <= 2147483647 } int32 { to_int result = x }
type pointer
type memory
logic get memory pointer int : int32
parameter mem : ref memory
logic block_size memory pointer : int
parameter get_ : p:pointer -> ofs:int32 ->
{ 0 <= to_int ofs < block_size mem p }
int32 reads mem
{ result = get mem p (to_int ofs) }
exception Return int32
let binary_search (t : pointer) (n : int32) (v : int32) =
{ 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) }
try
let l = ref (of_int 0) in
let u = ref (of_int (to_int n - 1)) in
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 }
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
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)
done;
raise (Return (of_int (-1)))
with Return r ->
r
end
{ (to_int result >= 0 and get mem t (to_int result) = v) or
(to_int result = -1 and forall k:int. 0<=k<to_int n -> get mem t k <> v) }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/binary_search_c.gui"
......
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