Commit 189ef30c authored by MARCHE Claude's avatar MARCHE Claude
Browse files

updated session

parent bc114561
......@@ -2,103 +2,108 @@
<!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" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.3" timelimit="10" memlimit="1000"/>
<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="1" name="Z3" version="4.3.1" timelimit="10" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.3" timelimit="10" memlimit="1000"/>
<file name="../binary_search.mlw" expanded="true">
<theory name="BinarySearch" sum="6edf021e1310395e54f253f514978225" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1" timelimit="10"><result status="valid" time="0.17"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="0.17"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="BinarySearchAnyMidPoint" sum="cf35a6556f511e3fa459bea0349c2cf8" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1" timelimit="10"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="902b39131261e18de4c4c65692531fe9" expanded="true">
<theory name="BinarySearchInt32" sum="b925c06b9515754650453539b3a5bc0f" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.22"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.22"/></proof>
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter binary_search.1" expl="1. integer overflow">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="WP_parameter binary_search.2" expl="2. integer overflow">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="WP_parameter binary_search.3" expl="3. integer overflow">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter binary_search.4" expl="4. loop invariant init">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter binary_search.5" expl="5. loop invariant init">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter binary_search.6" expl="6. integer overflow">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter binary_search.7" expl="7. integer overflow">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="WP_parameter binary_search.8" expl="8. division by zero">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter binary_search.9" expl="9. integer overflow">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="31"/></proof>
</goal>
<goal name="WP_parameter binary_search.10" expl="10. integer overflow">
<proof prover="1"><result status="valid" time="0.32"/></proof>
<proof prover="2"><result status="valid" time="0.56" steps="45"/></proof>
</goal>
<goal name="WP_parameter binary_search.11" expl="11. assertion">
<proof prover="1"><result status="valid" time="0.92"/></proof>
<proof prover="2"><result status="valid" time="0.92" steps="63"/></proof>
</goal>
<goal name="WP_parameter binary_search.12" expl="12. index in array bounds">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="WP_parameter binary_search.13" expl="13. integer overflow">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="WP_parameter binary_search.14" expl="14. integer overflow">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="43"/></proof>
</goal>
<goal name="WP_parameter binary_search.15" expl="15. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="30"/></proof>
</goal>
<goal name="WP_parameter binary_search.16" expl="16. loop invariant preservation">
<proof prover="1"><result status="valid" time="5.14"/></proof>
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="6.82" steps="106"/></proof>
</goal>
<goal name="WP_parameter binary_search.17" expl="17. loop variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="30"/></proof>
</goal>
<goal name="WP_parameter binary_search.18" expl="18. index in array bounds">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="WP_parameter binary_search.19" expl="19. integer overflow">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="WP_parameter binary_search.20" expl="20. integer overflow">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="WP_parameter binary_search.21" expl="21. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="WP_parameter binary_search.22" expl="22. loop invariant preservation">
<proof prover="1"><result status="valid" time="4.86"/></proof>
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.02"/></proof>
<proof prover="2" timelimit="60"><result status="valid" time="9.98" steps="107"/></proof>
</goal>
<goal name="WP_parameter binary_search.23" expl="23. loop variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="WP_parameter binary_search.24" expl="24. postcondition">
<proof prover="1"><result status="valid" time="0.74"/></proof>
<proof prover="2"><result status="valid" time="1.37" steps="57"/></proof>
</goal>
<goal name="WP_parameter binary_search.25" expl="25. exceptional postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
</transf>
</goal>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment