updated proof sessions

parent 9a7ef34a
This diff is collapsed.
......@@ -2,64 +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"/>
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo64.mlw" expanded="true">
<theory name="Algo64" sum="8ab02ef07be464ccc7c31dda9dd33adb" expanded="true">
<goal name="WP_parameter quicksort" expl="VC for quicksort" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter quicksort.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter quicksort.2" expl="2. variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter quicksort.3" expl="3. precondition">
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter quicksort.4" expl="4. assertion">
<proof prover="1"><result status="valid" time="0.14" steps="131"/></proof>
</goal>
<goal name="WP_parameter quicksort.5" expl="5. variant decrease">
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter quicksort.6" expl="6. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter quicksort.7" expl="7. assertion">
<proof prover="1"><result status="valid" time="1.43" steps="657"/></proof>
</goal>
<goal name="WP_parameter quicksort.8" expl="8. postcondition">
<proof prover="1"><result status="valid" time="0.19" steps="315"/></proof>
</goal>
<goal name="WP_parameter quicksort.9" expl="9. postcondition">
<proof prover="1"><result status="valid" time="0.16" steps="95"/></proof>
</goal>
<goal name="WP_parameter quicksort.10" expl="10. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="WP_parameter quicksort.11" expl="11. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
</transf>
<theory name="Algo64" sum="7c69c2a40d3abe34b382bd05d3264741" expanded="true">
<goal name="VC quicksort" expl="VC for quicksort" expanded="true">
<proof prover="0"><result status="valid" time="0.67" steps="2087"/></proof>
</goal>
<goal name="WP_parameter qs" expl="VC for qs">
<transf name="split_goal_wp">
<goal name="WP_parameter qs.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="WP_parameter qs.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter qs.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter qs.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter qs.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
</transf>
<goal name="VC qs" expl="VC for qs" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,137 +2,11 @@
<!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"/>
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo65.mlw" expanded="true">
<theory name="Algo65" sum="83b400a3fbe590385036b24b91ab4989" expanded="true">
<goal name="WP_parameter find" expl="VC for find" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter find.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="WP_parameter find.2" expl="2. variant decrease">
<proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="WP_parameter find.3" expl="3. precondition">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter find.4" expl="4. assertion">
<proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter find.5" expl="5. assertion">
<proof prover="1"><result status="valid" time="0.02" steps="96"/></proof>
</goal>
<goal name="WP_parameter find.6" expl="6. assertion" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter find.6.1" expl="1. assertion" expanded="true">
<proof prover="1" timelimit="6"><result status="valid" time="0.22" steps="248"/></proof>
</goal>
<goal name="WP_parameter find.6.2" expl="2. assertion">
<proof prover="1"><result status="valid" time="0.13" steps="143"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter find.7" expl="7. variant decrease">
<proof prover="1"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter find.8" expl="8. precondition">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter find.9" expl="9. assertion">
<proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="WP_parameter find.10" expl="10. assertion">
<proof prover="1"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter find.11" expl="11. assertion">
<proof prover="1"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter find.12" expl="12. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter find.13" expl="13. postcondition">
<proof prover="1"><result status="valid" time="0.03" steps="19"/></proof>
</goal>
<goal name="WP_parameter find.14" expl="14. postcondition">
<proof prover="1"><result status="valid" time="0.03" steps="19"/></proof>
</goal>
<goal name="WP_parameter find.15" expl="15. assertion">
<proof prover="1"><result status="valid" time="0.02" steps="45"/></proof>
</goal>
<goal name="WP_parameter find.16" expl="16. assertion">
<proof prover="1"><result status="valid" time="0.16" steps="320"/></proof>
</goal>
<goal name="WP_parameter find.17" expl="17. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="96"/></proof>
</goal>
<goal name="WP_parameter find.18" expl="18. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="WP_parameter find.19" expl="19. postcondition">
<proof prover="1"><result status="valid" time="0.11" steps="170"/></proof>
</goal>
<goal name="WP_parameter find.20" expl="20. assertion">
<proof prover="1"><result status="valid" time="0.02" steps="29"/></proof>
</goal>
<goal name="WP_parameter find.21" expl="21. assertion">
<proof prover="1"><result status="valid" time="0.05" steps="38"/></proof>
</goal>
<goal name="WP_parameter find.22" expl="22. variant decrease">
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter find.23" expl="23. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter find.24" expl="24. assertion">
<proof prover="1"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="WP_parameter find.25" expl="25. assertion">
<proof prover="1"><result status="valid" time="0.04" steps="163"/></proof>
</goal>
<goal name="WP_parameter find.26" expl="26. assertion" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter find.26.1" expl="1. assertion" expanded="true">
<proof prover="1" timelimit="6"><result status="valid" time="0.30" steps="380"/></proof>
</goal>
<goal name="WP_parameter find.26.2" expl="2. assertion">
<proof prover="1"><result status="valid" time="0.08" steps="113"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter find.27" expl="27. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="87"/></proof>
</goal>
<goal name="WP_parameter find.28" expl="28. postcondition">
<proof prover="1"><result status="valid" time="0.19" steps="110"/></proof>
</goal>
<goal name="WP_parameter find.29" expl="29. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="WP_parameter find.30" expl="30. assertion">
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter find.31" expl="31. assertion">
<proof prover="1"><result status="valid" time="0.04" steps="38"/></proof>
</goal>
<goal name="WP_parameter find.32" expl="32. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter find.33" expl="33. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="35"/></proof>
</goal>
<goal name="WP_parameter find.34" expl="34. postcondition">
<proof prover="1" timelimit="15"><result status="valid" time="0.03" steps="33"/></proof>
</goal>
<goal name="WP_parameter find.35" expl="35. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter find.36" expl="36. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter find.37" expl="37. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
</transf>
<theory name="Algo65" sum="8e4aea5af5aced5c839547b7fc4cfcba" expanded="true">
<goal name="VC find" expl="VC for find" expanded="true">
<proof prover="0"><result status="valid" time="0.52" steps="1682"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,48 +2,11 @@
<!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="6" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../all_distinct.mlw" expanded="true">
<theory name="AllDistinct" sum="3b44ec37df3232d188580bcf31db876f" expanded="true">
<goal name="WP_parameter all_distinct" expl="VC for all_distinct" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter all_distinct.1" expl="1. array creation size" expanded="true">
<proof prover="1"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="WP_parameter all_distinct.2" expl="2. postcondition" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter all_distinct.3" expl="3. loop invariant init" expanded="true">
<proof prover="1"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter all_distinct.4" expl="4. loop invariant init" expanded="true">
<proof prover="1"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter all_distinct.5" expl="5. index in array bounds" expanded="true">
<proof prover="1"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter all_distinct.6" expl="6. type invariant" expanded="true">
<proof prover="1"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter all_distinct.7" expl="7. index in array bounds" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter all_distinct.8" expl="8. postcondition" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter all_distinct.9" expl="9. index in array bounds" expanded="true">
<proof prover="1"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter all_distinct.10" expl="10. loop invariant preservation" expanded="true">
<proof prover="1"><result status="valid" time="0.02" steps="36"/></proof>
</goal>
<goal name="WP_parameter all_distinct.11" expl="11. loop invariant preservation" expanded="true">
<proof prover="1"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
<goal name="WP_parameter all_distinct.12" expl="12. postcondition" expanded="true">
<proof prover="1"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
</transf>
<theory name="AllDistinct" sum="3cf9eeed2975b5e758119618743ac04e" expanded="true">
<goal name="VC all_distinct" expl="VC for all_distinct" expanded="true">
<proof prover="0"><result status="valid" time="0.06" steps="274"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,17 +2,16 @@
<!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" steplimit="0" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../assigning_meanings_to_programs.mlw">
<theory name="Sum" sum="606dc92ebecb74d906410b581994896f" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<proof prover="2"><result status="valid" time="0.02" steps="21"/></proof>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../assigning_meanings_to_programs.mlw" expanded="true">
<theory name="Sum" sum="2df142ed68cf2dc81faf43efec368dfa" expanded="true">
<goal name="VC sum" expl="VC for sum" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="39"/></proof>
</goal>
</theory>
<theory name="Division" sum="67dbd39ccfe310fac83f690ec134b490" expanded="true">
<goal name="WP_parameter division" expl="VC for division" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<theory name="Division" sum="3fe8cf0a6e9f26c89aa9adc5d5734b14" expanded="true">
<goal name="VC division" expl="VC for division" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="11" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../binary_multiplication.mlw" expanded="true">
<theory name="BinaryMultiplication" sum="94846d4b1de94154d88628a5fe380629" expanded="true">
<goal name="WP_parameter binary_mult" expl="VC for binary_mult" expanded="true">
<proof prover="0"><result status="valid" time="0.74" steps="47"/></proof>
<theory name="BinaryMultiplication" sum="f1eebc593f40a0c87893ba3fd42ece8d" expanded="true">
<goal name="VC binary_mult" expl="VC for binary_mult" expanded="true">
<proof prover="1"><result status="valid" time="0.05" steps="49"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,113 +2,26 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" 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"/>
<file name="../binary_search.mlw" expanded="true">
<theory name="BinarySearch" sum="7c8646b76f7105e1357a0dac5eef6893" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<proof prover="0" timelimit="10"><result status="valid" time="0.03"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="0.02"/></proof>
<proof prover="5" timelimit="10"><result status="valid" time="0.17" steps="59"/></proof>
<theory name="BinarySearch" sum="30f36cd3e3f915bf18779d8426d30dba" expanded="true">
<goal name="VC binary_search" expl="VC for binary_search" expanded="true">
<proof prover="3"><result status="valid" time="0.05" steps="88"/></proof>
</goal>
</theory>
<theory name="BinarySearchAnyMidPoint" sum="fd005960645f7d3c23e93b34d869829e" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<proof prover="0" timelimit="10"><result status="valid" time="0.03"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="0.02"/></proof>
<proof prover="5" timelimit="10"><result status="valid" time="0.02" steps="44"/></proof>
<theory name="BinarySearchAnyMidPoint" sum="654f4a7e01ae8b9d8802dd39a8391937" expanded="true">
<goal name="VC binary_search" expl="VC for binary_search" expanded="true">
<proof prover="3"><result status="valid" time="0.01" steps="63"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="036ce72ded3ca54d6f20eb4e72544982" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter binary_search.1" expl="1. integer overflow">
<proof prover="5"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
<goal name="WP_parameter binary_search.2" expl="2. integer overflow">
<proof prover="5"><result status="valid" time="0.01" steps="75"/></proof>
</goal>
<goal name="WP_parameter binary_search.3" expl="3. integer overflow">
<proof prover="5"><result status="valid" time="0.12" steps="105"/></proof>
</goal>
<goal name="WP_parameter binary_search.4" expl="4. loop invariant init">
<proof prover="5"><result status="valid" time="0.01" steps="76"/></proof>
</goal>
<goal name="WP_parameter binary_search.5" expl="5. loop invariant init">
<proof prover="5"><result status="valid" time="0.01" steps="79"/></proof>
</goal>
<goal name="WP_parameter binary_search.6" expl="6. integer overflow">
<proof prover="5"><result status="valid" time="0.02" steps="87"/></proof>
</goal>
<goal name="WP_parameter binary_search.7" expl="7. integer overflow">
<proof prover="5"><result status="valid" time="0.02" steps="91"/></proof>
</goal>
<goal name="WP_parameter binary_search.8" expl="8. division by zero">
<proof prover="5"><result status="valid" time="0.01" steps="84"/></proof>
</goal>
<goal name="WP_parameter binary_search.9" expl="9. integer overflow">
<proof prover="5"><result status="valid" time="0.04" steps="99"/></proof>
</goal>
<goal name="WP_parameter binary_search.10" expl="10. integer overflow">
<proof prover="5"><result status="valid" time="0.11" steps="127"/></proof>
</goal>
<goal name="WP_parameter binary_search.11" expl="11. assertion">
<proof prover="5"><result status="valid" time="0.27" steps="158"/></proof>
</goal>
<goal name="WP_parameter binary_search.12" expl="12. index in array bounds">
<proof prover="5"><result status="valid" time="0.01" steps="91"/></proof>
</goal>
<goal name="WP_parameter binary_search.13" expl="13. integer overflow">
<proof prover="5"><result status="valid" time="0.01" steps="95"/></proof>
</goal>
<goal name="WP_parameter binary_search.14" expl="14. integer overflow">
<proof prover="5"><result status="valid" time="0.03" steps="112"/></proof>
</goal>
<goal name="WP_parameter binary_search.15" expl="15. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.02" steps="99"/></proof>
</goal>
<goal name="WP_parameter binary_search.16" expl="16. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="3.48"/></proof>
<proof prover="5"><result status="valid" time="1.34" steps="202"/></proof>
</goal>
<goal name="WP_parameter binary_search.17" expl="17. loop variant decrease">
<proof prover="5"><result status="valid" time="0.02" steps="99"/></proof>
</goal>
<goal name="WP_parameter binary_search.18" expl="18. index in array bounds">
<proof prover="5"><result status="valid" time="0.01" steps="95"/></proof>
</goal>
<goal name="WP_parameter binary_search.19" expl="19. integer overflow">
<proof prover="5"><result status="valid" time="0.01" steps="97"/></proof>
</goal>
<goal name="WP_parameter binary_search.20" expl="20. integer overflow">
<proof prover="5"><result status="valid" time="0.02" steps="113"/></proof>
</goal>
<goal name="WP_parameter binary_search.21" expl="21. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.02" steps="101"/></proof>
</goal>
<goal name="WP_parameter binary_search.22" expl="22. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="3.46"/></proof>
<proof prover="5"><result status="valid" time="1.35" steps="203"/></proof>
</goal>
<goal name="WP_parameter binary_search.23" expl="23. loop variant decrease">
<proof prover="5"><result status="valid" time="0.02" steps="101"/></proof>
</goal>
<goal name="WP_parameter binary_search.24" expl="24. postcondition">
<proof prover="5"><result status="valid" time="0.08" steps="137"/></proof>
</goal>
<goal name="WP_parameter binary_search.25" expl="25. exceptional postcondition">
<proof prover="5"><result status="valid" time="0.01" steps="90"/></proof>
</goal>
</transf>
<theory name="BinarySearchInt32" sum="ffe998c5d427389d248ba1206038419f" expanded="true">
<goal name="VC binary_search" expl="VC for binary_search" expanded="true">
<proof prover="3"><result status="valid" time="2.52" steps="3684"/></proof>
</goal>
</theory>
<theory name="BinarySearchBoolean" sum="a5514ddedacede3daea09952d8e9ba38" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<proof prover="1"><result status="valid" time="0.07" steps="118"/></proof>
<theory name="BinarySearchBoolean" sum="11f0d4476d5bc0a21421ee04e1e8c88f" expanded="true">
<goal name="VC binary_search" expl="VC for binary_search" expanded="true">
<proof prover="3"><result status="valid" time="0.08" steps="194"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,86 +2,57 @@
<!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="30" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../binary_sqrt.mlw" expanded="true">
<theory name="BinarySqrt" sum="77fef8e995729374a1ce4e7237bca6a2" expanded="true">
<goal name="WP_parameter sqrt" expl="VC for sqrt" expanded="true">
<theory name="BinarySqrt" sum="f145abf28e9a527311e3e575fef6192b" expanded="true">
<goal name="VC sqrt" expl="VC for sqrt" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter sqrt.1" expl="1. postcondition">
<proof prover="7"><result status="valid" time="0.02"/></proof>
<goal name="VC sqrt.1" expl="1. assertion">
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="WP_parameter sqrt.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="12"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<goal name="VC sqrt.2" expl="2. assertion">
<proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="WP_parameter sqrt.3" expl="3. assertion">
<proof prover="7"><result status="valid" time="0.02"/></proof>
<goal name="VC sqrt.3" expl="3. assertion">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="WP_parameter sqrt.4" expl="4. assertion">
<proof prover="5"><result status="valid" time="0.02" steps="9"/></proof>
<goal name="VC sqrt.4" expl="4. assertion">
<proof prover="1"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="WP_parameter sqrt.5" expl="5. assertion">
<proof prover="5"><result status="valid" time="0.03" steps="27"/></proof>
<goal name="VC sqrt.5" expl="5. assertion">
<proof prover="1"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter sqrt.6" expl="6. assertion">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="7" timelimit="30"><result status="valid" time="0.01"/></proof>
<goal name="VC sqrt.6" expl="6. variant decrease">
<proof prover="1"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
<goal name="WP_parameter sqrt.7" expl="7. variant decrease">
<proof prover="5"><result status="valid" time="0.06" steps="33"/></proof>
<proof prover="6"><result status="valid" time="0.04"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<goal name="VC sqrt.7" expl="7. precondition">
<proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="WP_parameter sqrt.8" expl="8. precondition">
<proof prover="5"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<goal name="VC sqrt.8" expl="8. precondition">
<proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="WP_parameter sqrt.9" expl="9. precondition">
<proof prover="5"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<goal name="VC sqrt.9" expl="9. precondition">
<proof prover="1"><result status="valid" time="0.22" steps="126"/></proof>
</goal>
<goal name="WP_parameter sqrt.10" expl="10. precondition">
<proof prover="7"><result status="valid" time="0.01"/></proof>
<goal name="VC sqrt.10" expl="10. postcondition" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC sqrt.10.1" expl="1. VC for sqrt">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC sqrt.10.2" expl="2. VC for sqrt">
<proof prover="1"><undone/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sqrt.11" expl="11. postcondition">
<proof prover="5"><result status="valid" time="0.20" steps="22"/></proof>
<goal name="VC sqrt.11" expl="11. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sqrt_main" expl="VC for sqrt_main" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter sqrt_main.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter sqrt_main.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter sqrt_main.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter sqrt_main.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
<goal name="VC sqrt_main" expl="VC for sqrt_main" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
......@@ -2,96 +2,25 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.3.1" timelimit="10" 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="3" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../coincidence_count.mlw" expanded="true">
<theory name="CoincidenceCount" sum="17b09e5c8a51c7635f8c46ed79d78cff" expanded="true">
<theory name="CoincidenceCount" sum="40619067d27b67fafc68245658b265cc" expanded="true">
<goal name="drop_left">
<proof prover="2"><result status="valid" time="0.15" steps="486"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.15" steps="486"/></proof>
<proof prover="3"><result status="valid" time="0.06" steps="344"/></proof>
</goal>
<goal name="not_mem_inter_r">
<proof prover="1"><result status="valid" time="1.02" steps="585"/></proof>
<proof prover="1" obsolete="true"><result status="valid" time="1.02" steps="585"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="161"/></proof>
</goal>
<goal name="not_mem_inter_l">
<proof prover="1"><result status="valid" time="1.01" steps="585"/></proof>
<proof prover="1" obsolete="true"><result status="valid" time="1.01" steps="585"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="161"/></proof>
</goal>
<goal name="WP_parameter coincidence_count" expl="VC for coincidence_count" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter coincidence_count.1" expl="1. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.2" expl="2. loop invariant init">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.3" expl="3. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.4" expl="4. index in array bounds">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.5" expl="5. index in array bounds">
<proof prover="1"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.6" expl="6. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.7" expl="7. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.8" expl="8. loop invariant preservation">
<proof prover="1"><result status="valid" time="1.19" steps="375"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.9" expl="9. loop variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.10" expl="10. index in array bounds">
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.11" expl="11. index in array bounds">
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.12" expl="12. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.13" expl="13. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.14" expl="14. loop invariant preservation">
<proof prover="1"><result status="valid" time="1.29" steps="376"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.15" expl="15. loop variant decrease">
<proof prover="1"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.16" expl="16. assertion">
<proof prover="0"><result status="valid" time="2.19"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.17" expl="17. assertion">
<transf name="inline_goal">
<goal name="WP_parameter coincidence_count.17.1" expl="1. assertion">
<proof prover="1"><result status="valid" time="0.69" steps="302"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter coincidence_count.18" expl="18. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.19" expl="19. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.20" expl="20. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.70" steps="167"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.21" expl="21. loop variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>