binary search: a slight generalization

parent 9ab0704b
......@@ -2,7 +2,7 @@
A classical example. Searches a sorted array for a given value v. *)
module M
module BinarySearch
use import int.Int
use import int.ComputerDivision
......@@ -42,6 +42,47 @@ module M
end
(* A generalization: the midpoint is computed by some abstract function.
The only requirement is that is lies between l and u. *)
module BinarySearchAnyMidPoint
use import int.Int
use import module ref.Ref
use import module array.Array
exception Break int (* raised to exit the loop *)
exception Not_found (* raised to signal a search failure *)
val midpoint: l:int -> u:int -> { l <= u } int { l <= result <= u }
let binary_search (a :array int) (v : int) =
{ forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
try
let l = ref 0 in
let u = ref (length a - 1) in
while !l <= !u do
invariant {
0 <= !l /\ !u < length a /\
forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
variant { !u - !l }
let m = midpoint !l !u in
if a[m] < v then
l := m + 1
else if a[m] > v then
u := m - 1
else
raise (Break m)
done;
raise Not_found
with Break i ->
i
end
{ 0 <= result < length a /\ a[result] = v }
| Not_found -> { forall i:int. 0 <= i < length a -> a[i] <> v }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/binary_search.gui"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/binary_search/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../binary_search.mlw" verified="true" expanded="true">
<theory name="WP M" verified="true" expanded="true">
<goal name="WP_parameter binary_search" expl="parameter binary_search" sum="a0cb3811cc2d2e6a7091476e65c97c65" proved="true" expanded="true" shape="iainfix <=V4V3iainfix <agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V3V5ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V6V3Aainfix <=V5V6Iainfix =agetV2V6V1Iainfix <V6V0Aainfix <=c0V6FAainfix <V3V0Aainfix <=c0V5Iainfix =V5ainfix +ainfix +V4adivainfix -V3V4c2c1Fiainfix >agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V7V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V7Aainfix <=V4V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V7V0Aainfix <=c0V4Iainfix =V7ainfix -ainfix +V4adivainfix -V3V4c2c1Fainfix =agetV2ainfix +V4adivainfix -V3V4c2V1Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <=ainfix +V4adivainfix -V3V4c2V3Aainfix <=V4ainfix +V4adivainfix -V3V4c2ainfix =agetV2V9V1NIainfix <V9V0Aainfix <=c0V9FIainfix <=V10V3Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V11ainfix -V0c1Aainfix <=c0V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V12agetV2V13Iainfix <V13V0Aainfix <=V12V13Aainfix <=c0V12FFFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<why3session
name="examples/programs/binary_search/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.2pl1"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="0.7 Dhajea"/>
<prover
id="gappa"
name="Gappa"
version="0.14.0"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="yices"
name="Yices"
version="1.0.13"/>
<prover
id="z3"
name="Z3"
version="2.13"/>
<file
name="../binary_search.mlw"
verified="true"
expanded="true">
<theory
name="WP BinarySearch"
verified="true"
expanded="true">
<goal
name="WP_parameter binary_search"
expl="parameter binary_search"
sum="a0cb3811cc2d2e6a7091476e65c97c65"
proved="true"
expanded="true"
shape="iainfix <=V4V3iainfix <agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V3V5ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V6V3Aainfix <=V5V6Iainfix =agetV2V6V1Iainfix <V6V0Aainfix <=c0V6FAainfix <V3V0Aainfix <=c0V5Iainfix =V5ainfix +ainfix +V4adivainfix -V3V4c2c1Fiainfix >agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V7V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V7Aainfix <=V4V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V7V0Aainfix <=c0V4Iainfix =V7ainfix -ainfix +V4adivainfix -V3V4c2c1Fainfix =agetV2ainfix +V4adivainfix -V3V4c2V1Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <=ainfix +V4adivainfix -V3V4c2V3Aainfix <=V4ainfix +V4adivainfix -V3V4c2ainfix =agetV2V9V1NIainfix <V9V0Aainfix <=c0V9FIainfix <=V10V3Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V11ainfix -V0c1Aainfix <=c0V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V12agetV2V13Iainfix <V13V0Aainfix <=V12V13Aainfix <=c0V12FFFF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
<theory
name="WP BinarySearchAnyMidPoint"
verified="true"
expanded="true">
<goal
name="WP_parameter binary_search"
expl="parameter binary_search"
sum="27673a8148872a1c3e9b89cd8a3d6015"
proved="true"
expanded="true"
shape="iainfix <=V4V3iainfix <agetV2V5V1ainfix <ainfix -V3V6ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V7V3Aainfix <=V6V7Iainfix =agetV2V7V1Iainfix <V7V0Aainfix <=c0V7FAainfix <V3V0Aainfix <=c0V6Iainfix =V6ainfix +V5c1Fiainfix >agetV2V5V1ainfix <ainfix -V8V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V9V8Aainfix <=V4V9Iainfix =agetV2V9V1Iainfix <V9V0Aainfix <=c0V9FAainfix <V8V0Aainfix <=c0V4Iainfix =V8ainfix -V5c1Fainfix =agetV2V5V1Aainfix <V5V0Aainfix <=c0V5Aainfix <V5V0Aainfix <=c0V5Aainfix <V5V0Aainfix <=c0V5Iainfix <=V5V3Aainfix <=V4V5FAainfix <=V4V3ainfix =agetV2V10V1NIainfix <V10V0Aainfix <=c0V10FIainfix <=V11V3Aainfix <=V4V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V12ainfix -V0c1Aainfix <=c0V12Iainfix =agetV2V12V1Iainfix <V12V0Aainfix <=c0V12FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V13agetV2V14Iainfix <V14V0Aainfix <=V13V14Aainfix <=c0V13FFFF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
......
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