binary_search: yet another variant

examples/binary_search.mlw

@@ -14,7 +14,7 @@ module BinarySearch
   exception Break int (* raised to exit the loop *)
   exception Not_found (* raised to signal a search failure *)
 
-  let binary_search (a : array int) (v : int)
+  let binary_search (a : array int) (v : int) : int
     requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
     ensures  { 0 <= result < length a /\ a[result] = v }
     raises   { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
@@ -57,7 +57,7 @@ module BinarySearchAnyMidPoint
   val midpoint (l:int) (u:int) : int
     requires { l <= u } ensures { l <= result <= u }
 
-  let binary_search (a :array int) (v : int)
+  let binary_search (a :array int) (v : int) : int
     requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
     ensures  { 0 <= result < length a /\ a[result] = v }
     raises   { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
@@ -97,7 +97,7 @@ module BinarySearchInt32
   exception Break int32 (* raised to exit the loop *)
   exception Not_found   (* raised to signal a search failure *)
 
-  let binary_search (a : array int32) (v : int32)
+  let binary_search (a : array int32) (v : int32) : int32
     requires { forall i1 i2 : int. 0 <= i1 <= i2 < to_int a.length ->
                to_int a[i1] <= to_int a[i2] }
     ensures  { 0 <= to_int result < to_int a.length /\ a[to_int result] = v }
@@ -126,3 +126,35 @@ module BinarySearchInt32
     end
 
 end
+
+(* A particular case with Boolean values (0 or 1) and a sentinel 1 at the end.
+   We look for the first position containing a 1. *)
+
+module BinarySearchBoolean
+
+  use import int.Int
+  use import int.ComputerDivision
+  use import ref.Ref
+  use import array.Array
+
+  let binary_search (a: array int) : int
+    requires { 0 < a.length }
+    requires { forall i j. 0 <= i <= j < a.length -> 0 <= a[i] <= a[j] <= 1 }
+    requires { a[a.length - 1] = 1 }
+    ensures  { 0 <= result < a.length && a[result] = 1 }
+  =
+    let lo = ref 0 in
+    let hi = ref (length a - 1) in
+    while !lo < !hi do
+      invariant { 0 <= !lo <= !hi < a.length }
+      invariant { a[!hi] = 1 }
+      variant   { !hi - !lo }
+      let mid = !lo + div (!hi - !lo) 2 in
+      if a[mid] = 1 then
+        hi := mid
+      else
+        lo := mid + 1
+    done;
+    !lo
+
+end

examples/binary_search/why3session.xml

@@ -3,6 +3,7 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../binary_search.mlw" expanded="true">
@@ -105,5 +106,10 @@
  </transf>
  </goal>
 </theory>
+<theory name="BinarySearchBoolean" sum="fcc9811fb74b3662bb4626585c1e69cb" expanded="true">
+ <goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="61"/></proof>
+ </goal>
+</theory>
 </file>
 </why3session>