Commit 6afca432 authored by MARCHE Claude's avatar MARCHE Claude

updated sessions

parent 3af79fbd
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="2" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo63.mlw" proved="true"> <file name="../algo63.mlw" proved="true">
<theory name="Algo63" proved="true" sum="b882ca24fd9e33b8497d2ffd24d75517"> <theory name="Algo63" proved="true" sum="97df5190bde02efd9e0de8cdbea3356f">
<goal name="VC exchange" expl="VC for exchange" proved="true"> <goal name="VC exchange" expl="VC for exchange" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="62"/></proof> <proof prover="2"><result status="valid" time="0.03" steps="62"/></proof>
</goal> </goal>
......
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="3" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../algo63.mlw" proved="true"> <file name="../algo63.mlw" proved="true">
<theory name="Algo63" proved="true" sum="b882ca24fd9e33b8497d2ffd24d75517"> <theory name="Algo63" proved="true" sum="97df5190bde02efd9e0de8cdbea3356f">
<goal name="VC exchange" expl="VC for exchange" proved="true"> <goal name="VC exchange" expl="VC for exchange" proved="true">
<transf name="split_goal_wp" proved="true" > <transf name="split_goal_wp" proved="true" >
<goal name="VC exchange.0" expl="index in array bounds" proved="true"> <goal name="VC exchange.0" expl="index in array bounds" proved="true">
......
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo64.mlw" proved="true"> <file name="../algo64.mlw" proved="true">
<theory name="Algo64" proved="true" sum="53d17c1a5a0d90843aaf1177717a079b"> <theory name="Algo64" proved="true" sum="d424a975b8a7b2f1bb6825629de9143a">
<goal name="VC quicksort" expl="VC for quicksort" proved="true"> <goal name="VC quicksort" expl="VC for quicksort" proved="true">
<proof prover="0"><result status="valid" time="0.67" steps="2087"/></proof> <proof prover="0"><result status="valid" time="0.67" steps="2087"/></proof>
</goal> </goal>
......
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo65.mlw" proved="true"> <file name="../algo65.mlw" proved="true">
<theory name="Algo65" proved="true" sum="db2c890cb561211fa36098a88daddfac"> <theory name="Algo65" proved="true" sum="06510cf0c04926152c626875f383e149">
<goal name="VC find" expl="VC for find" proved="true"> <goal name="VC find" expl="VC for find" proved="true">
<proof prover="0"><result status="valid" time="0.52" steps="1688"/></proof> <proof prover="0"><result status="valid" time="0.52" steps="1688"/></proof>
</goal> </goal>
......
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../all_distinct.mlw" proved="true"> <file name="../all_distinct.mlw" proved="true">
<theory name="AllDistinct" proved="true" sum="6f38713a3ec25b0a6b1d31017b344871"> <theory name="AllDistinct" proved="true" sum="ffbeb873677b943d48c32a50ca55f83a">
<goal name="VC all_distinct" expl="VC for all_distinct" proved="true"> <goal name="VC all_distinct" expl="VC for all_distinct" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="270"/></proof> <proof prover="0"><result status="valid" time="0.06" steps="270"/></proof>
</goal> </goal>
......
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../arm.mlw" proved="true"> <file name="../arm.mlw" proved="true">
<theory name="M" proved="true" sum="66462041b72873a3bb20b0ae331ca7a0"> <theory name="M" proved="true" sum="eade0a495f21f73e713558097e8dc30a">
<goal name="VC insertion_sort" expl="VC for insertion_sort" proved="true"> <goal name="VC insertion_sort" expl="VC for insertion_sort" proved="true">
<proof prover="0"><result status="valid" time="0.11" steps="135"/></proof> <proof prover="0"><result status="valid" time="0.11" steps="135"/></proof>
</goal> </goal>
......
...@@ -3,14 +3,14 @@ ...@@ -3,14 +3,14 @@
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../assigning_meanings_to_programs.mlw" expanded="true"> <file name="../assigning_meanings_to_programs.mlw" proved="true">
<theory name="Sum" sum="464fbc01e7969eb94479e6f6762a1672" expanded="true"> <theory name="Sum" proved="true" sum="f8b6d21736575c9d96e33f6e4488d7f8">
<goal name="VC sum" expl="VC for sum" expanded="true"> <goal name="VC sum" expl="VC for sum" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="39"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="39"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="Division" sum="ce38e3995afc25e5981ed2086f16a1aa" expanded="true"> <theory name="Division" proved="true" sum="ce38e3995afc25e5981ed2086f16a1aa">
<goal name="VC division" expl="VC for division" expanded="true"> <goal name="VC division" expl="VC for division" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof> <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
</goal> </goal>
</theory> </theory>
......
...@@ -3,19 +3,19 @@ ...@@ -3,19 +3,19 @@
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../balance.mlw" expanded="true"> <file name="../balance.mlw" proved="true">
<theory name="Roberval" sum="d41d8cd98f00b204e9800998ecf8427e"> <theory name="Roberval" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory> </theory>
<theory name="Puzzle8" sum="cd15b414a487f5dee1d992c22c5e3264"> <theory name="Puzzle8" proved="true" sum="5190f9ec34a89ac2cdcb13553fb118d0">
<goal name="VC solve3" expl="VC for solve3"> <goal name="VC solve3" expl="VC for solve3" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="47"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="47"/></proof>
</goal> </goal>
<goal name="VC solve8" expl="VC for solve8"> <goal name="VC solve8" expl="VC for solve8" proved="true">
<proof prover="0"><result status="valid" time="0.13" steps="291"/></proof> <proof prover="0"><result status="valid" time="0.13" steps="291"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="Puzzle12" sum="6ea315cb4493db13a7fa4541d6a0e474" expanded="true"> <theory name="Puzzle12" proved="true" sum="16c107f90c6f5ce13152f8283a51361c">
<goal name="VC solve12" expl="VC for solve12" expanded="true"> <goal name="VC solve12" expl="VC for solve12" proved="true">
<proof prover="0"><result status="valid" time="0.53" steps="1379"/></proof> <proof prover="0"><result status="valid" time="0.53" steps="1379"/></proof>
</goal> </goal>
</theory> </theory>
......
...@@ -5,17 +5,17 @@ ...@@ -5,17 +5,17 @@
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="3" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../binary_search.mlw" proved="true"> <file name="../binary_search.mlw" proved="true">
<theory name="BinarySearch" proved="true" sum="a87eac5cc232a78b8d8da4a5e55ee897"> <theory name="BinarySearch" proved="true" sum="d31e4317db720e4fcc15037002211036">
<goal name="VC binary_search" expl="VC for binary_search" proved="true"> <goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="3"><result status="valid" time="0.05" steps="88"/></proof> <proof prover="3"><result status="valid" time="0.05" steps="88"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="BinarySearchAnyMidPoint" proved="true" sum="6461e35169c0e5653c907b27049a389f"> <theory name="BinarySearchAnyMidPoint" proved="true" sum="6ddfd27f10cde251a7e1595797c95b78">
<goal name="VC binary_search" expl="VC for binary_search" proved="true"> <goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="63"/></proof> <proof prover="3"><result status="valid" time="0.01" steps="63"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="BinarySearchBranchless" proved="true" sum="3b2dad84c0bdc39e32b7664b11a669ff"> <theory name="BinarySearchBranchless" proved="true" sum="2a9abf885782d1699240f4f90a15db6f">
<goal name="VC binary_search" expl="VC for binary_search" proved="true"> <goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="147"/></proof> <proof prover="0"><result status="valid" time="0.06" steps="147"/></proof>
</goal> </goal>
...@@ -25,7 +25,7 @@ ...@@ -25,7 +25,7 @@
<proof prover="3"><result status="valid" time="8.18" steps="11481"/></proof> <proof prover="3"><result status="valid" time="8.18" steps="11481"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="BinarySearchBoolean" proved="true" sum="0022604a394766cd083f25712d0f873a"> <theory name="BinarySearchBoolean" proved="true" sum="30b8723bec4ae48757a979bd59ddcac1">
<goal name="VC binary_search" expl="VC for binary_search" proved="true"> <goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="3"><result status="valid" time="0.08" steps="194"/></proof> <proof prover="3"><result status="valid" time="0.08" steps="194"/></proof>
</goal> </goal>
......
...@@ -4,12 +4,12 @@ ...@@ -4,12 +4,12 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../binary_search_vc_sp.mlw" proved="true"> <file name="../binary_search_vc_sp.mlw" proved="true">
<theory name="BinarySearch" proved="true" sum="9993e5984f553599fa3101436646fad3"> <theory name="BinarySearch" proved="true" sum="986e3c732646924bbc22bb3d4ec369ee">
<goal name="VC binary_search" expl="VC for binary_search" proved="true"> <goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof> <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="BinarySearchAnyMidPoint" proved="true" sum="3973fb0e710d4ec1c08923db54c5f93f"> <theory name="BinarySearchAnyMidPoint" proved="true" sum="1706e9372b3999d5866c48e66a5223f9">
<goal name="VC binary_search" expl="VC for binary_search" proved="true"> <goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof> <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal> </goal>
...@@ -19,7 +19,7 @@ ...@@ -19,7 +19,7 @@
<proof prover="0"><result status="valid" time="0.10"/></proof> <proof prover="0"><result status="valid" time="0.10"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="BinarySearchBoolean" proved="true" sum="0022604a394766cd083f25712d0f873a"> <theory name="BinarySearchBoolean" proved="true" sum="30b8723bec4ae48757a979bd59ddcac1">
<goal name="VC binary_search" expl="VC for binary_search" proved="true"> <goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="0.06"/></proof> <proof prover="0"><result status="valid" time="0.06"/></proof>
</goal> </goal>
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../binary_sort.mlw" proved="true"> <file name="../binary_sort.mlw" proved="true">
<theory name="BinarySort" proved="true" sum="c1c832159f18a903011e9a535c30f2f6"> <theory name="BinarySort" proved="true" sum="62d22e1f5b6d78cb6d29fe59a962a286">
<goal name="VC occ_shift" expl="VC for occ_shift" proved="true"> <goal name="VC occ_shift" expl="VC for occ_shift" proved="true">
<proof prover="0"><result status="valid" time="0.54"/></proof> <proof prover="0"><result status="valid" time="0.54"/></proof>
</goal> </goal>
...@@ -78,7 +78,7 @@ ...@@ -78,7 +78,7 @@
<goal name="VC binary_sort.21" expl="loop invariant preservation" proved="true"> <goal name="VC binary_sort.21" expl="loop invariant preservation" proved="true">
<transf name="case" proved="true" arg1="(j=k)"> <transf name="case" proved="true" arg1="(j=k)">
<goal name="VC binary_sort.21.0" expl="true case (loop invariant preservation)" proved="true"> <goal name="VC binary_sort.21.0" expl="true case (loop invariant preservation)" proved="true">
<proof prover="1" timelimit="10" memlimit="4000"><result status="valid" time="1.66" steps="1019"/></proof> <proof prover="1" timelimit="10" memlimit="4000"><result status="valid" time="1.66" steps="1017"/></proof>
</goal> </goal>
<goal name="VC binary_sort.21.1" expl="false case (loop invariant preservation)" proved="true"> <goal name="VC binary_sort.21.1" expl="false case (loop invariant preservation)" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.75" steps="689"/></proof> <proof prover="1" timelimit="1"><result status="valid" time="0.75" steps="689"/></proof>
......
...@@ -140,7 +140,7 @@ ...@@ -140,7 +140,7 @@
<proof prover="4"><result status="valid" time="0.02"/></proof> <proof prover="4"><result status="valid" time="0.02"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="Test_imperial_violet" proved="true" sum="4e2bdcbea51830917c9997009c023511"> <theory name="Test_imperial_violet" proved="true" sum="84681d2248f09c3369c67ed1fbedc075">
<goal name="bv32_bounds_bv" proved="true"> <goal name="bv32_bounds_bv" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof> <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal> </goal>
...@@ -180,7 +180,7 @@ ...@@ -180,7 +180,7 @@
<proof prover="3"><result status="valid" time="0.02" steps="137"/></proof> <proof prover="3"><result status="valid" time="0.02" steps="137"/></proof>
</goal> </goal>
<goal name="VC add.7" expl="loop invariant preservation" proved="true"> <goal name="VC add.7" expl="loop invariant preservation" proved="true">
<proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="2.36" steps="2919"/></proof> <proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="2.36" steps="2847"/></proof>
</goal> </goal>
<goal name="VC add.8" expl="postcondition" proved="true"> <goal name="VC add.8" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.06"/></proof> <proof prover="4"><result status="valid" time="0.06"/></proof>
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
<prover id="11" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="11" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="12" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="12" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bitwalker.mlw" proved="true"> <file name="../bitwalker.mlw" proved="true">
<theory name="Bitwalker" proved="true" sum="0efcbd982faa8c64c2d86689d8f43c03"> <theory name="Bitwalker" proved="true" sum="9f78b35011f44d38f665317325a6307e">
<goal name="nth64" proved="true"> <goal name="nth64" proved="true">
<proof prover="10"><result status="valid" time="0.02" steps="91"/></proof> <proof prover="10"><result status="valid" time="0.02" steps="91"/></proof>
</goal> </goal>
...@@ -48,7 +48,7 @@ ...@@ -48,7 +48,7 @@
<proof prover="11"><result status="valid" time="0.08"/></proof> <proof prover="11"><result status="valid" time="0.08"/></proof>
</goal> </goal>
<goal name="VC poke_64bit_bv.5" expl="postcondition" proved="true"> <goal name="VC poke_64bit_bv.5" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.27"/></proof> <proof prover="11"><result status="valid" time="0.12"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -160,7 +160,7 @@ ...@@ -160,7 +160,7 @@
<proof prover="11"><result status="valid" time="0.16"/></proof> <proof prover="11"><result status="valid" time="0.16"/></proof>
</goal> </goal>
<goal name="VC peek.16" expl="loop invariant preservation" proved="true"> <goal name="VC peek.16" expl="loop invariant preservation" proved="true">
<proof prover="11"><result status="valid" time="0.81"/></proof> <proof prover="11"><result status="valid" time="1.36"/></proof>
</goal> </goal>
<goal name="VC peek.17" expl="loop invariant preservation" proved="true"> <goal name="VC peek.17" expl="loop invariant preservation" proved="true">
<proof prover="11"><result status="valid" time="0.12"/></proof> <proof prover="11"><result status="valid" time="0.12"/></proof>
...@@ -264,7 +264,7 @@ ...@@ -264,7 +264,7 @@
<proof prover="12"><result status="valid" time="0.02"/></proof> <proof prover="12"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC poke.5" expl="postcondition" proved="true"> <goal name="VC poke.5" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof> <proof prover="12"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC poke.6" expl="postcondition" proved="true"> <goal name="VC poke.6" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof> <proof prover="12"><result status="valid" time="0.02"/></proof>
...@@ -279,7 +279,7 @@ ...@@ -279,7 +279,7 @@
<proof prover="12"><result status="valid" time="0.02"/></proof> <proof prover="12"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC poke.10" expl="postcondition" proved="true"> <goal name="VC poke.10" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.01"/></proof> <proof prover="12"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC poke.11" expl="precondition" proved="true"> <goal name="VC poke.11" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.04"/></proof> <proof prover="12"><result status="valid" time="0.04"/></proof>
...@@ -359,13 +359,13 @@ ...@@ -359,13 +359,13 @@
<proof prover="12"><result status="valid" time="0.02"/></proof> <proof prover="12"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC poke.31" expl="postcondition" proved="true"> <goal name="VC poke.31" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.93"/></proof> <proof prover="11"><result status="valid" time="0.69"/></proof>
</goal> </goal>
<goal name="VC poke.32" expl="postcondition" proved="true"> <goal name="VC poke.32" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof> <proof prover="12"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC poke.33" expl="postcondition" proved="true"> <goal name="VC poke.33" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.38"/></proof> <proof prover="11"><result status="valid" time="0.62"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bubble_sort.mlw" proved="true"> <file name="../bubble_sort.mlw" proved="true">
<theory name="BubbleSort" proved="true" sum="6b92ef189b7fec9778d9694b28a1b549"> <theory name="BubbleSort" proved="true" sum="6a88fa014742f7a66d4e38a455762c82">
<goal name="VC bubble_sort" expl="VC for bubble_sort" proved="true"> <goal name="VC bubble_sort" expl="VC for bubble_sort" proved="true">
<transf name="split_goal_wp" proved="true" > <transf name="split_goal_wp" proved="true" >
<goal name="VC bubble_sort.0" expl="loop invariant init" proved="true"> <goal name="VC bubble_sort.0" expl="loop invariant init" proved="true">
...@@ -85,10 +85,10 @@ ...@@ -85,10 +85,10 @@
</transf> </transf>
</goal> </goal>
<goal name="VC test1" expl="VC for test1" proved="true"> <goal name="VC test1" expl="VC for test1" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="11"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="13"/></proof>
</goal> </goal>
<goal name="VC test2" expl="VC for test2" proved="true"> <goal name="VC test2" expl="VC for test2" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="38"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="40"/></proof>
</goal> </goal>
<goal name="VC bench" expl="VC for bench" proved="true"> <goal name="VC bench" expl="VC for bench" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="28"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
......
...@@ -5,21 +5,21 @@ ...@@ -5,21 +5,21 @@
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="6" steplimit="0" memlimit="1000"/> <prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="3" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../coincidence_count.mlw" expanded="true"> <file name="../coincidence_count.mlw" proved="true">
<theory name="CoincidenceCount" sum="b1548bbf632a991ba0139bb7832a9b2e" expanded="true"> <theory name="CoincidenceCount" proved="true" sum="ec636900f65b5990cb02f9b12ac3744e">
<goal name="drop_left" expl=""> <goal name="drop_left" proved="true">
<proof prover="2"><result status="valid" time="0.15" steps="337"/></proof> <proof prover="2"><result status="valid" time="0.15" steps="337"/></proof>
<proof prover="3"><result status="valid" time="0.06" steps="344"/></proof> <proof prover="3"><result status="valid" time="0.06" steps="344"/></proof>
</goal> </goal>
<goal name="not_mem_inter_r" expl=""> <goal name="not_mem_inter_r" proved="true">
<proof prover="1"><result status="valid" time="0.27" steps="391"/></proof> <proof prover="1"><result status="valid" time="0.27" steps="391"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="161"/></proof> <proof prover="3"><result status="valid" time="0.03" steps="161"/></proof>
</goal> </goal>
<goal name="not_mem_inter_l" expl=""> <goal name="not_mem_inter_l" proved="true">
<proof prover="1"><result status="valid" time="0.27" steps="391"/></proof> <proof prover="1"><result status="valid" time="0.27" steps="391"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="161"/></proof> <proof prover="3"><result status="valid" time="0.03" steps="161"/></proof>
</goal> </goal>
<goal name="VC coincidence_count" expl="VC for coincidence_count" expanded="true"> <goal name="VC coincidence_count" expl="VC for coincidence_count" proved="true">
<proof prover="3"><result status="valid" time="0.62" steps="2573"/></proof> <proof prover="3"><result status="valid" time="0.62" steps="2573"/></proof>
</goal> </goal>
</theory> </theory>
......
...@@ -4,14 +4,14 @@ ...@@ -4,14 +4,14 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../conjugate.mlw" proved="true"> <file name="../conjugate.mlw" proved="true">
<theory name="Conjugate" proved="true" sum="a4627d5b4c10a678bd8f3ac4153e1701"> <theory name="Conjugate" proved="true" sum="8540711dc8b8e51095325473d80b3aae">
<goal name="VC conjugate" expl="VC for conjugate" proved="true"> <goal name="VC conjugate" expl="VC for conjugate" proved="true">
<proof prover="0"><result status="valid" time="0.13" steps="318"/></proof> <proof prover="0"><result status="valid" time="0.13" steps="291"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="Test" proved="true" sum="7ce01eb912fe3360b61ea4643591d3f0"> <theory name="Test" proved="true" sum="b34bcfb14f9c545ff96d752da5743896">
<goal name="VC test" expl="VC for test" proved="true"> <goal name="VC test" expl="VC for test" proved="true">
<proof prover="0"><result status="valid" time="0.11" steps="96"/></proof> <proof prover="0"><result status="valid" time="0.11" steps="99"/></proof>
</goal> </goal>
<goal name="VC bench" expl="VC for bench" proved="true"> <goal name="VC bench" expl="VC for bench" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="12"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
......
...@@ -11,33 +11,47 @@ ...@@ -11,33 +11,47 @@
<proof prover="1"><result status="valid" time="2.86" steps="906"/></proof> <proof prover="1"><result status="valid" time="2.86" steps="906"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="ListCursorImpl" proved="true" sum="9c26980f775fc1daf0f91a03e3228b78"> <theory name="ListCursorImpl" proved="true" sum="5c9d2123d18fe945b303f391ec90daed">
<goal name="VC has_next" expl="VC for has_next" proved="true"> <goal name="VC cursor" expl="VC for cursor" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="12"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
<goal name="VC snoc_Cons" expl="VC for snoc_Cons" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="99"/></proof>
</goal> </goal>
<goal name="VC next" expl="VC for next" proved="true"> <goal name="VC next" expl="VC for next" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="56"/></proof> <proof prover="1"><result status="valid" time="0.13" steps="465"/></proof>
</goal> </goal>
<goal name="VC create" expl="VC for create" proved="true"> <goal name="VC has_next" expl="VC for has_next" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="33"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="66"/></proof>
</goal> </goal>
<goal name="VC create" expl="VC for create" proved="true"> <goal name="VC create" expl="VC for create" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="51"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="51"/></proof>
</goal> </goal>
<goal name="VC has_next" expl="VC for has_next" proved="true"> <goal name="ListCursor.VC create" expl="VC for create" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="66"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
<goal name="VC next" expl="VC for next" proved="true">
<proof prover="1"><result status="valid" time="0.13" steps="465"/></proof>
</goal> </goal>
<goal name="VC snoc_Cons" expl="VC for snoc_Cons" proved="true"> <goal name="ListCursor.C.VC next" expl="VC for next" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="99"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="56"/></proof>
</goal> </goal>
<goal name="VC cursor" expl="VC for cursor" proved="true"> <goal name="ListCursor.C.VC has_next" expl="VC for has_next" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="33"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="12"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="TestListCursor" proved="true" sum="33ee0b7261aba8db53cfa2c709b8e643"> <theory name="TestListCursor" proved="true" sum="5e03d6040df40972278e1bab8d1137ac">
<goal name="sum_of_list" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="sum_of_list.0" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="sum_of_list.0.0" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="sum_of_list.0.1" proved="true">
<proof prover="1"><result status="valid" time="3.48" steps="1147"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC list_sum" expl="VC for list_sum" proved="true"> <goal name="VC list_sum" expl="VC for list_sum" proved="true">
<transf name="split_goal_wp" proved="true" > <transf name="split_goal_wp" proved="true" >
<goal name="VC list_sum.0" expl="loop invariant init" proved="true"> <goal name="VC list_sum.0" expl="loop invariant init" proved="true">
...@@ -73,37 +87,35 @@ ...@@ -73,37 +87,35 @@
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="sum_of_list" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="sum_of_list.0" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="sum_of_list.0.0" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="sum_of_list.0.1" proved="true">
<proof prover="1"><result status="valid" time="3.48" steps="1147"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</theory> </theory>
<theory name="TestListCursorLink" proved="true" sum="d9ca5c2e030c4310aa371641265a3c3d"> <theory name="TestListCursorLink" proved="true" sum="57ad90333a0eff06c751d7979b07b08c">
<goal name="VC has_next" expl="VC for has_next" proved="true"> <goal name="TestListCursor.ListCursor.VC create" expl="VC for create" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="38"/></proof>
</goal> </goal>
<goal name="VC next" expl="VC for next" proved="true"> <goal name="TestListCursor.ListCursor.C.VC next" expl="VC for next" proved="true">
<proof prover="1"><result status="valid" time="0.03" steps="59"/></proof> <proof prover="1"><result status="valid" time="0.03" steps="59"/></proof>
</goal> </goal>
<goal name="VC create" expl="VC for create" proved="true"> <goal name="TestListCursor.ListCursor.C.VC has_next" expl="VC for has_next" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="38"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="ArrayCursorImpl" proved="true" sum="f36514ec4c22f2c7d3f35f8c338695c2"> <theory name="ArrayCursorImpl" proved="true" sum="06468482e282d9cf2035e73ba7373228">
<goal name="VC cursor" expl="VC for cursor" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="3"/></proof>
</goal>
<goal name="VC create" expl="VC for create" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="VC has_next" expl="VC for has_next" proved="true"> <goal name="VC has_next" expl="VC for has_next" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="12"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="19"/></proof>