machine arithmetic: a first experiment

examples/programs/binary_search.mlw

@@ -83,6 +83,48 @@ module BinarySearchAnyMidPoint
 
 end
 
+(* binary search using 32-bit integers *)
+
+module BinarySearchInt32
+
+  use import module arith.Int32
+  use import module ref.Ref
+  use import module array.Array
+
+  (* the code and its specification *)
+
+  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) =
+    { 0 <= length a <= max_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 = !l + div (!u - !l) 2 in
+        assert { !l <= m <= !u };
+        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"

examples/programs/binary_search/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session
- name="programs/binary_search/why3session.xml">
+ name="examples/programs/binary_search/why3session.xml">
  <prover
   id="alt-ergo"
   name="Alt-Ergo"
-  version="0.94"/>
- <prover
-  id="alt-ergo-0.93.1"
-  name="Alt-Ergo"
   version="0.93.1"/>
  <prover
   id="coq"
   name="Coq"
-  version="8.3pl2"/>
+  version="8.2pl1"/>
  <prover
   id="cvc3-2.2"
   name="CVC3"
   version="2.2"/>
- <prover
-  id="cvc3-2.4"
-  name="CVC3"
-  version="2.4.1"/>
- <prover
-  id="eprover"
-  name="Eprover"
-  version="1.4 Namring"/>
  <prover
   id="gappa"
   name="Gappa"
-  version="0.15.1"/>
+  version="0.15.0"/>
  <prover
   id="simplify"
   name="Simplify"
   version="1.5.4"/>
- <prover
-  id="spass"
-  name="Spass"
-  version="3.7"/>
- <prover
-  id="vampire"
-  name="Vampire"
-  version="0.6"/>
- <prover
-  id="verit"
-  name="veriT"
-  version="dev"/>
  <prover
   id="yices"
   name="Yices"
-  version="1.0.25"/>
+  version="1.0"/>
  <prover
   id="z3-2"
   name="Z3"
   version="2.19"/>
- <prover
-  id="z3-3"
-  name="Z3"
-  version="3.2"/>
  <file
   name="../binary_search.mlw"
   verified="true"
@@ -69,7 +41,7 @@
    <goal
     name="WP_parameter binary_search"
     expl="parameter binary_search"
-    sum="05b308271de57dac7bc9311c80a79391"
+    sum="2d4368f5fd910b1ceb69adef571ead55"
     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">
@@ -78,14 +50,14 @@
      timelimit="10"
      edited=""
      obsolete="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.08"/>
     </proof>
     <proof
      prover="alt-ergo"
      timelimit="10"
      edited=""
      obsolete="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.06"/>
     </proof>
    </goal>
   </theory>
@@ -96,7 +68,7 @@
    <goal
     name="WP_parameter binary_search"
     expl="parameter binary_search"
-    sum="332e80ad2cab058df73928f0e1009412"
+    sum="d5cd94966f7526a19692c7d56b842e9f"
     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">
@@ -105,7 +77,27 @@
      timelimit="10"
      edited=""
      obsolete="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.06"/>
+    </proof>
+   </goal>
+  </theory>
+  <theory
+   name="WP BinarySearchInt32"
+   verified="true"
+   expanded="true">
+   <goal
+    name="WP_parameter binary_search"
+    expl="parameter binary_search"
+    sum="3f43f4cc865166a924a323c51975d7de"
+    proved="true"
+    expanded="true"
+    shape="iainfix <=V4V3Lainfix -V3V4Lainfix +V4adivV5c2iainfix <agetV2V6V1ainfix <ainfix -V3V7ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V3Aainfix <=V7V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V3V0Aainfix <=c0V7Iainfix =V7ainfix +V6c1FAainfix <=ainfix +V6c1amax_intAainfix <=amin_intainfix +V6c1iainfix >agetV2V6V1ainfix <ainfix -V9V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V10V9Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V9V0Aainfix <=c0V4Iainfix =V9ainfix -V6c1FAainfix <=ainfix -V6c1amax_intAainfix <=amin_intainfix -V6c1ainfix =agetV2V6V1Aainfix <V6V0Aainfix <=c0V6Aainfix <V6V0Aainfix <=c0V6Aainfix <V6V0Aainfix <=c0V6Aainfix <=V6V3Aainfix <=V4V6Aainfix <=ainfix +V4adivV5c2amax_intAainfix <=amin_intainfix +V4adivV5c2Aainfix <=ainfix -V3V4amax_intAainfix <=amin_intainfix -V3V4ainfix =agetV2V11V1NIainfix <V11V0Aainfix <=c0V11FIainfix <=V12V3Aainfix <=V4V12Iainfix =agetV2V12V1Iainfix <V12V0Aainfix <=c0V12FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V13ainfix -V0c1Aainfix <=c0V13Iainfix =agetV2V13V1Iainfix <V13V0Aainfix <=c0V13FAainfix <ainfix -V0c1V0Aainfix <=c0c0Aainfix <=ainfix -V0c1amax_intAainfix <=amin_intainfix -V0c1Iainfix <=agetV2V14agetV2V15Iainfix <V15V0Aainfix <=V14V15Aainfix <=c0V14FAainfix <=V0amax_intAainfix <=c0V0FFF">
+    <proof
+     prover="alt-ergo"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="valid" time="0.59"/>
     </proof>
    </goal>
   </theory>

modules/arith.mlw

@@ -11,6 +11,30 @@ module Int
 end
 
 (* machine arithmetic (32-bit integers, etc.) will go here *)
+module Int32
+
+  use export int.Int
+
+  function min_int : int = -2147483648
+  function max_int : int =  2147483647
+
+  let (+) (x: int) (y:int) =
+    { min_int <= x + y <= max_int } x + y { result = x + y }
+  let (-) (x: int) (y:int) =
+    { min_int <= x - y <= max_int } x - y { result = x - y }
+
+  let (-_) (x: int) =
+    { min_int <= -x <= max_int } -x { result = -x  }
+
+  let ( * ) (x: int) (y:int) =
+    { min_int <= x * y <= max_int } x * y { result = x * y }
+
+  use export int.ComputerDivision
+
+  let (/) (x: int) (y:int) =
+    { y <> 0 && min_int <= div x y <= max_int } div x y { result = div x y }
+
+end
 
 module Real