Example: new proof for mccarthy function computation

examples/mccarthy.mlw

@@ -5,30 +5,29 @@ module McCarthy91
 
   use import int.Int
 
+  function spec (x: int) : int = if x <= 100 then 91 else x-10
+
   (* traditional recursive implementation *)
 
   let rec f91 (n:int) : int variant { 101-n }
-    ensures { result = if n <= 100 then 91 else n - 10 }
+    ensures { result = spec n }
   = if n <= 100 then
       f91 (f91 (n + 11))
     else
       n - 10
 
-
   (* non-recursive implementation using a while loop *)
 
   use import ref.Ref
 
-  function f (x: int) : int = if x <= 100 then 91 else x-10
-
   (* iter k x = f^k(x) *)
-  clone import int.Iter with type t = int, function f = f
+  clone import int.Iter with type t = int, function f = spec
 
-  let f91_nonrec (n0: int) ensures { result = f n0 }
+  let f91_nonrec (n0: int) ensures { result = spec n0 }
   = let e = ref 1 in
     let n = ref n0 in
     while !e > 0 do
-      invariant { !e >= 0 /\ iter !e !n = f n0 }
+      invariant { !e >= 0 /\ iter !e !n = spec n0 }
       variant   { 101 - !n + 10 * !e, !e }
       if !n > 100 then begin
         n := !n - 10;
@@ -40,4 +39,40 @@ module McCarthy91
     done;
     !n
 
+  (* Use a 'morally' irrelevant control flow from a recursive function
+     to ease proof (the recursive structure does not contribute to the
+     program execution). This is a technique for proving derecursified
+     programs. See verifythis_2016_tree_traversal for a more
+     complex example. *)
+
+  exception Stop
+
+  let f91_pseudorec (n0:int) : int
+    ensures { result = spec n0 }
+  = let e = ref 1 in
+    let n = ref n0 in
+    let bloc () : unit
+      requires { !e >= 0 }
+      ensures { !(old e) > 0 }
+      ensures { if !(old n) > 100 then !n = !(old n) - 10 /\ !e = !(old e) - 1
+        else !n = !(old n) + 11 /\ !e = !(old e) + 1 }
+      raises { Stop -> !e = !(old e) = 0 /\ !n = !(old n) }
+    = if not (!e > 0) then raise Stop;
+      if !n > 100 then begin
+        n := !n - 10;
+        e := !e - 1
+      end else begin
+        n := !n + 11;
+        e := !e + 1
+      end
+    in
+    let rec aux () : unit
+      requires { !e > 0 }
+      variant { 101 - !n }
+      ensures { !e = !(old e) - 1 /\ !n = spec !(old n) }
+      raises { Stop -> false }
+    = let u = !n in bloc (); if u <= 100 then (aux (); aux ()) in
+    try aux (); bloc (); absurd
+    with Stop -> !n end
+
 end

examples/mccarthy/why3session.xml

@@ -2,57 +2,17 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
-<prover id="2" name="Z3" version="3.2" timelimit="10" memlimit="0"/>
-<prover id="3" name="veriT" version="201310" timelimit="5" memlimit="4000"/>
-<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="10" memlimit="0"/>
+<prover id="0" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../mccarthy.mlw" expanded="true">
-<theory name="McCarthy91" sum="fc4723c0574acd30d3d960beb8743bed" expanded="true">
- <goal name="WP_parameter f91" expl="VC for f91" expanded="true">
- <proof prover="0" timelimit="2"><result status="valid" time="0.00"/></proof>
- <proof prover="2" timelimit="2"><result status="valid" time="0.02"/></proof>
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- <proof prover="4" timelimit="2"><result status="valid" time="0.02" steps="11"/></proof>
+<theory name="McCarthy91" sum="4a73db0e7cb62d49c98fa874799f159d" expanded="true">
+ <goal name="WP_parameter f91" expl="VC for f91">
+ <proof prover="0"><result status="valid" time="0.00" steps="15"/></proof>
  </goal>
- <goal name="WP_parameter f91_nonrec" expl="VC for f91_nonrec" expanded="true">
- <transf name="split_goal_wp" expanded="true">
-  <goal name="WP_parameter f91_nonrec.1" expl="1. loop invariant init" expanded="true">
-  <proof prover="0"><result status="valid" time="0.00"/></proof>
-  <proof prover="2"><result status="valid" time="0.00"/></proof>
-  <proof prover="3"><result status="valid" time="0.00"/></proof>
-  <proof prover="4"><result status="valid" time="0.01" steps="1"/></proof>
-  </goal>
-  <goal name="WP_parameter f91_nonrec.2" expl="2. loop invariant preservation" expanded="true">
-  <proof prover="0"><result status="valid" time="0.02"/></proof>
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
-  <proof prover="3"><result status="valid" time="0.00"/></proof>
-  <proof prover="4"><result status="valid" time="0.00" steps="22"/></proof>
-  </goal>
-  <goal name="WP_parameter f91_nonrec.3" expl="3. loop variant decrease" expanded="true">
-  <proof prover="0"><result status="valid" time="0.00"/></proof>
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
-  <proof prover="3"><result status="valid" time="0.00"/></proof>
-  <proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
-  </goal>
-  <goal name="WP_parameter f91_nonrec.4" expl="4. loop invariant preservation" expanded="true">
-  <proof prover="0"><result status="valid" time="0.03"/></proof>
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
-  <proof prover="3"><result status="valid" time="0.00"/></proof>
-  <proof prover="4"><result status="valid" time="0.24" steps="87"/></proof>
-  </goal>
-  <goal name="WP_parameter f91_nonrec.5" expl="5. loop variant decrease" expanded="true">
-  <proof prover="0"><result status="valid" time="0.02"/></proof>
-  <proof prover="2"><result status="valid" time="0.03"/></proof>
-  <proof prover="3"><result status="valid" time="0.00"/></proof>
-  <proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
-  </goal>
-  <goal name="WP_parameter f91_nonrec.6" expl="6. postcondition" expanded="true">
-  <proof prover="0"><result status="valid" time="0.02"/></proof>
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
-  <proof prover="3"><result status="valid" time="0.00"/></proof>
-  <proof prover="4"><result status="valid" time="0.02" steps="5"/></proof>
-  </goal>
- </transf>
+ <goal name="WP_parameter f91_nonrec" expl="VC for f91_nonrec">
+ <proof prover="0"><result status="valid" time="0.11" steps="171"/></proof>
+ </goal>
+ <goal name="WP_parameter f91_pseudorec" expl="VC for f91_pseudorec">
+ <proof prover="0"><result status="valid" time="0.02" steps="44"/></proof>
  </goal>
 </theory>
 </file>