updated proof sessions

examples/TODO

-add_list.mlw
 arm.mlw
 bag.mlw
 bellman_ford.mlw
@@ -16,12 +15,9 @@ division.mlw
 dyck.mlw
 edit_distance.mlw
 esterel.mlw
-euler001.mlw
-euler002.mlw
 ewd673.mlw
 fibonacci.mlw
 find.mlw
-finger_trees.mlw
 finite_tarski.mlw
 flag2.mlw
 foveoos11_challenge1.mlw
@@ -39,7 +35,6 @@ lcp.mlw
 linear_probing.mlw
 linked_list_rev.mlw
 maximum_subarray.mlw
-mergesort_list.mlw
 my_cosine.mlw
 optimal_replay.mlw
 patience.mlw
@@ -55,7 +50,6 @@ schorr_waite_via_recursion.mlw
 sieve.mlw
 skew_heaps.mlw
 snapshotable_trees.mlw
-sorted_list.mlw
 sudoku.mlw
 sum_of_digits.mlw
 there_and_back_again.mlw

examples/add_list/why3session.xml

@@ -2,31 +2,25 @@
 <!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="5" steplimit="0" memlimit="1000"/>
-<prover id="2" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../add_list.mlw" expanded="true">
+<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="4" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
+<file name="../add_list.mlw">
 <theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="AddListRec" sum="f062b1e05a91602624b37c4b34762555" expanded="true">
- <goal name="WP_parameter sum" expl="VC for sum" expanded="true">
- <proof prover="0"><result status="valid" time="0.01"/></proof>
- <proof prover="2"><result status="valid" time="0.02"/></proof>
- <proof prover="3"><result status="valid" time="0.02" steps="49"/></proof>
+<theory name="AddListRec" sum="b22282c439ddd5fa9976e2048ec06a22">
+ <goal name="VC sum" expl="VC for sum">
+ <proof prover="1"><result status="valid" time="0.02" steps="200"/></proof>
  </goal>
- <goal name="WP_parameter main" expl="VC for main" expanded="true">
- <proof prover="0"><result status="valid" time="0.02"/></proof>
- <proof prover="2"><result status="valid" time="0.02"/></proof>
+ <goal name="VC main" expl="VC for main">
+ <proof prover="4"><result status="valid" time="0.02"/></proof>
  </goal>
 </theory>
-<theory name="AddListImp" sum="7ac8c0163d88693d0911255c23bfb93d" expanded="true">
- <goal name="WP_parameter sum" expl="VC for sum" expanded="true">
- <proof prover="0"><result status="valid" time="0.02"/></proof>
- <proof prover="2"><result status="valid" time="0.02"/></proof>
+<theory name="AddListImp" sum="f7b23f93ac300ff2dca6f1bdf5f7fec6">
+ <goal name="VC sum" expl="VC for sum">
+ <proof prover="4"><result status="valid" time="0.02"/></proof>
  </goal>
- <goal name="WP_parameter main" expl="VC for main" expanded="true">
- <proof prover="0"><result status="valid" time="0.02"/></proof>
- <proof prover="2"><result status="valid" time="0.02"/></proof>
+ <goal name="VC main" expl="VC for main">
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
  </goal>
 </theory>
 </file>

examples/mergesort_list.mlw

@@ -288,6 +288,9 @@ module OCamlMergesort
     ensures { sorted result /\ permut result l }
   =
     let n = length l in
-    if n < 2 then l else sort n l
+    if n < 2 then begin
+      assert { sorted l by match l with
+               Nil | Cons _ Nil -> sorted l | _ -> false end }; l end
+    else sort n l
 
 end

examples/sorted_list/why3session.xml

@@ -2,14 +2,14 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../sorted_list.mlw" expanded="true">
-<theory name="FindInSortedList" sum="3c166ab8af8b25d4aa1158674a32d49e" expanded="true">
- <goal name="Sorted_not_mem" expanded="true">
- <proof prover="1"><result status="valid" time="0.03" steps="70"/></proof>
+<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
+<file name="../sorted_list.mlw">
+<theory name="FindInSortedList" sum="298058842c408886f5247ad3999c1d3d">
+ <goal name="Sorted_not_mem">
+ <proof prover="0"><result status="valid" time="0.03" steps="44"/></proof>
  </goal>
- <goal name="WP_parameter find" expl="VC for find" expanded="true">
- <proof prover="1"><result status="valid" time="0.02" steps="118"/></proof>
+ <goal name="VC find" expl="VC for find">
+ <proof prover="0"><result status="valid" time="0.01" steps="148"/></proof>
  </goal>
 </theory>
 </file>