improved readability

examples/defunctionalization.mlw

@@ -147,7 +147,7 @@ use import Expr
 
 use HighOrd
 
-function eval_1 (e:expr) (k:int -> 'a) : 'a =
+function eval_1 (e:expr) (k: int->'a) : 'a =
   match e with
     | Cte n -> k n
     | Sub e1 e2 ->
@@ -161,7 +161,7 @@ function interpret_1 (p : prog) : int = eval_1 p (\ n. n)
 
 use import DirectSem
 
-lemma cps_correct_expr: forall e:expr, k:int -> 'a. eval_1 e k = k (eval_0 e)
+lemma cps_correct_expr: forall e:expr, k: int->'a. eval_1 e k = k (eval_0 e)
 
 lemma cps_correct: forall p. interpret_1 p = interpret_0 p
 

examples/defunctionalization/why3session.xml

@@ -187,7 +187,7 @@
        prover="2"
        timelimit="5"
        memlimit="4000"
-       obsolete="true"
+       obsolete="false"
        archived="false">
        <result status="timeout" time="4.98"/>
       </proof>
@@ -195,7 +195,7 @@
        prover="3"
        timelimit="5"
        memlimit="4000"
-       obsolete="true"
+       obsolete="false"
        archived="false">
        <result status="timeout" time="5.01"/>
       </proof>
@@ -203,7 +203,7 @@
        prover="4"
        timelimit="5"
        memlimit="4000"
-       obsolete="true"
+       obsolete="false"
        archived="false">
        <result status="timeout" time="5.02"/>
       </proof>
@@ -601,7 +601,7 @@
        memlimit="4000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="1.59"/>
+       <result status="valid" time="1.89"/>
       </proof>
      </goal>
      <goal
@@ -868,7 +868,7 @@
        prover="3"
        timelimit="5"
        memlimit="4000"
-       obsolete="true"
+       obsolete="false"
        archived="false">
        <result status="timeout" time="4.96"/>
       </proof>
@@ -876,7 +876,7 @@
        prover="4"
        timelimit="5"
        memlimit="4000"
-       obsolete="true"
+       obsolete="false"
        archived="false">
        <result status="timeout" time="4.99"/>
       </proof>
@@ -948,9 +948,9 @@
        prover="0"
        timelimit="5"
        memlimit="4000"
-       obsolete="true"
+       obsolete="false"
        archived="false">
-       <result status="unknown" time="0.36"/>
+       <result status="unknown" time="0.55"/>
       </proof>
       <proof
        prover="1"
@@ -972,7 +972,7 @@
        prover="3"
        timelimit="5"
        memlimit="4000"
-       obsolete="true"
+       obsolete="false"
        archived="false">
        <result status="timeout" time="4.97"/>
       </proof>
@@ -980,7 +980,7 @@
        prover="4"
        timelimit="5"
        memlimit="4000"
-       obsolete="true"
+       obsolete="false"
        archived="false">
        <result status="timeout" time="4.98"/>
       </proof>
@@ -1016,7 +1016,7 @@
        prover="2"
        timelimit="5"
        memlimit="4000"
-       obsolete="true"
+       obsolete="false"
        archived="false">
        <result status="timeout" time="4.99"/>
       </proof>
@@ -2155,7 +2155,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.18"/>
+     <result status="valid" time="1.58"/>
     </proof>
     <proof
      prover="1"
@@ -2650,7 +2650,7 @@
      prover="2"
      timelimit="5"
      memlimit="1000"
-     obsolete="true"
+     obsolete="false"
      archived="false">
      <result status="timeout" time="4.99"/>
     </proof>
@@ -3654,7 +3654,7 @@
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.10"/>
+       <result status="valid" time="0.22"/>
       </proof>
       <proof
        prover="2"
@@ -3734,7 +3734,7 @@
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="1.81"/>
+       <result status="valid" time="2.82"/>
       </proof>
      </goal>
      <goal
@@ -3754,7 +3754,7 @@
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="3.44"/>
+       <result status="valid" time="4.70"/>
       </proof>
       <proof
        prover="1"
@@ -3770,7 +3770,7 @@
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.43"/>
+       <result status="valid" time="0.65"/>
       </proof>
      </goal>
     </transf>

examples/fact.mlw

@@ -5,9 +5,11 @@ module FactRecursive
 
   use import int.Fact
 
-  let rec fact_rec (x:int) : int variant {x} =
-    requires { x >= 0 } ensures { result = fact x }
-    if x = 0 then 1 else x * fact_rec (x-1)
+  let rec fact_rec (x:int) : int 
+    requires { x >= 0 } 
+    variant  { x } 
+    ensures  { result = fact x }
+  = if x = 0 then 1 else x * fact_rec (x-1)
 
   let test0 () = fact_rec 0
   let test1 () = fact_rec 1
@@ -27,7 +29,8 @@ module FactImperative
   = let y = ref 0 in
     let r = ref 1 in
     while !y < x do
-      invariant { 0 <= !y <= x /\ !r = fact !y }
+      invariant { 0 <= !y <= x }
+      invariant { !r = fact !y }
       variant { x - !y }
       y := !y + 1;
       r := !r * !y