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

examples: yet another binary search program

parent 0c00a03b
(* yet another binary search *)
module BinarySearch
use import int.Int
use import int.ComputerDivision
logic f int : int
axiom f_monotonic : forall x y : int. x <= y -> f x <= f y
let rec binary_search target lo hi variant { hi-lo } =
{ f lo < target <= f hi }
if lo < hi-1 then
let mid = div (lo + hi) 2 in
if f mid < target then
binary_search target mid hi
else
binary_search target lo mid
else
hi
{ f result = target and
forall x : int. x < result -> f x <> target }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/binary_search2.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