test floats

examples/check-builtin/floats.why

+
+theory TestGappa
+
+   use import real.Real
+   use import real.Abs
+   use import real.Square
+   use import floating_point.Rounding
+   use floating_point.Single
+   use import floating_point.Double
+
+  goal Round_single_01:
+    Single.round NearestTiesToEven 0.1 = 0x1.99999ap-4
+
+  goal Round_double_01:
+    Double.round NearestTiesToEven 0.1 = 0x1.999999999999ap-4
+
+   goal Test00: forall x:real.  abs x <= 2.0 -> -3.0 <= x
+
+   goal Test01:
+       forall x:double.
+          -2.0 <= value x <= 2.0 ->
+             abs((value x) * (value x) -
+                 round NearestTiesToEven ((value x) * (value x))) <= 0x1p-52
+
+   goal Test02:
+       forall x y:double.
+          abs (value x) <= 2.0 ->
+            y = x ->
+             abs((value y) * (value y) -
+                 round NearestTiesToEven ((value x) * (value x))) <= 0x1p-52
+
+   goal Test03:
+       forall x y z:double.
+          abs (value x) <= 2.0 ->
+          value y = round NearestTiesToEven ((value x) * (value x)) ->
+          z = y ->
+          sqrt ((value z - (value x)*(value x))*(value y - (value x)*(value x))) <= 0x1p-52
+
+
+end
+
+
+

examples/check-builtin/floats/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session SYSTEM "why3session.dtd">
+<why3session
+ name="examples/check-builtin/floats/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="../floats.why"
+  verified="true"
+  expanded="true">
+  <theory
+   name="TestGappa"
+   verified="true"
+   expanded="true">
+   <goal
+    name="Round_single_01"
+    sum="4350d059bf72b21b36729eaccc394959"
+    proved="true"
+    expanded="true"
+    shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.99999ap-4">
+    <proof
+     prover="gappa"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+   </goal>
+   <goal
+    name="Round_double_01"
+    sum="fc4b69caf28748e651e23f375e300b70"
+    proved="true"
+    expanded="true"
+    shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.999999999999ap-4">
+    <proof
+     prover="gappa"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+   </goal>
+   <goal
+    name="Test00"
+    sum="d126875bf4fc484b4b44c2b52b9da437"
+    proved="true"
+    expanded="true"
+    shape="ainfix <=aprefix -c3.0V0Iainfix <=aabsV0c2.0F">
+    <proof
+     prover="cvc3"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="valid" time="0.02"/>
+    </proof>
+    <proof
+     prover="alt-ergo"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="valid" time="0.03"/>
+    </proof>
+    <proof
+     prover="z3"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="valid" time="0.05"/>
+    </proof>
+    <proof
+     prover="gappa"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+   </goal>
+   <goal
+    name="Test01"
+    sum="bcbfbae3da81b362e99b319253ef2a20"
+    proved="true"
+    expanded="true"
+    shape="ainfix <=aabsainfix -ainfix *avalueV0avalueV0aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix <=avalueV0c2.0Aainfix <=aprefix -c2.0avalueV0F">
+    <proof
+     prover="gappa"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+   </goal>
+   <goal
+    name="Test02"
+    sum="1d3e20e12a14b6bd91a25d057da3b098"
+    proved="true"
+    expanded="true"
+    shape="ainfix <=aabsainfix -ainfix *avalueV1avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix =V1V0Iainfix <=aabsavalueV0c2.0F">
+    <proof
+     prover="gappa"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+   </goal>
+   <goal
+    name="Test03"
+    sum="42c26c3443d67722883a37dfe8f9253c"
+    proved="true"
+    expanded="true"
+    shape="ainfix <=asqrtainfix *ainfix -avalueV2ainfix *avalueV0avalueV0ainfix -avalueV1ainfix *avalueV0avalueV0c0x1.p-52Iainfix =V2V1Iainfix =avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0Iainfix <=aabsavalueV0c2.0F">
+    <proof
+     prover="gappa"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+   </goal>
+  </theory>
+ </file>
+</why3session>

tests/test-gappa.why

@@ -5,27 +5,34 @@ theory TestGappa
    use import real.Abs
    use import real.Square
    use import floating_point.Rounding
+   use floating_point.Single
    use import floating_point.Double
 
+  lemma Round_single_01:
+    Single.round NearestTiesToEven 0.1 = 0x1.99999ap-4
+
+  lemma Round_double_01:
+    Double.round NearestTiesToEven 0.1 = 0x1.999999999999ap-4
+
    lemma Test00: forall x:real.  abs x <= 2.0 -> -3.0 <= x
 
-   lemma Test01: 
+   lemma Test01:
        forall x:double.
           -2.0 <= value x <= 2.0 ->
-             abs((value x) * (value x) - 
+             abs((value x) * (value x) -
                  round NearestTiesToEven ((value x) * (value x))) <= 0x1p-52
 
-   lemma Test02: 
+   lemma Test02:
        forall x y:double.
-          abs (value x) <= 2.0 -> 
+          abs (value x) <= 2.0 ->
             y = x ->
-             abs((value y) * (value y) - 
+             abs((value y) * (value y) -
                  round NearestTiesToEven ((value x) * (value x))) <= 0x1p-52
 
-   lemma Test03: 
+   lemma Test03:
        forall x y z:double.
-          abs (value x) <= 2.0 -> 
-          value y = round NearestTiesToEven ((value x) * (value x)) -> 
+          abs (value x) <= 2.0 ->
+          value y = round NearestTiesToEven ((value x) * (value x)) ->
           z = y ->
           sqrt ((value z - (value x)*(value x))*(value y - (value x)*(value x))) <= 0x1p-52
 

theories/floating_point.why

@@ -81,19 +81,30 @@ theory GenFloat
   axiom Round_up_neg:
     forall x:real. round Up (-x) = - round Down x
 
-end
-
-theory GenFloatFull
-
-  use import GenFloat
   use import SpecialValues
 
   (* special values *)
   function class t : class
   function sign t  : sign
 
+  predicate is_finite (x:t) = class x = Finite
+  predicate is_infinite (x:t) = class x = Infinite
+  predicate is_NaN (x:t) = class x = NaN
+  predicate is_not_NaN (x:t) = is_finite x \/ is_infinite x
+  predicate is_minus_infinity (x:t) = is_infinite x /\ sign x = Neg
+  predicate is_plus_infinity (x:t) = is_infinite x /\ sign x = Pos
+  predicate is_gen_zero (x:t) = is_finite x /\ value x = 0.0
+  predicate is_gen_zero_plus (x:t) = is_gen_zero x /\ sign x = Pos
+  predicate is_gen_zero_minus (x:t) = is_gen_zero x /\ sign x = Neg
+
+  predicate le (x:t) (y:t) =
+     (is_finite x /\ is_finite y /\ value x <= value y)
+     \/ (is_minus_infinity x /\ is_not_NaN y)
+     \/ (is_not_NaN x /\ is_plus_infinity y)
+
 end
 
+
 theory Single
 
   type single
@@ -124,15 +135,4 @@ theory Double
 
 end
 
-theory Test
-
-  use import Rounding
-  use Single
-  use Double
-
-  lemma Round_single_01: Single.round NearestTiesToEven 0.1 = 0x1.99999ap-4
-
-  lemma Round_double_01: Double.round NearestTiesToEven 0.1 = 0x1.999999999999ap-4
-
-end