Skip to content

why3
why3
Commit 34c5aeb6 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

sessions: some updates for compatibility with Coq 8.5

parent 86a95cbe
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1983 additions and 2414 deletions
examples/algo64/why3session.xml
View file @ 34c5aeb6
......@@ -2,62 +2,62 @@
<!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.95.2" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" 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="0"><result status="valid" time="0.02" steps="5"/></proof>
<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="0"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter quicksort.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter quicksort.4" expl="4. assertion">
<proof prover="0"><result status="valid" time="0.14" steps="172"/></proof>
<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="0"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter quicksort.6" expl="6. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter quicksort.7" expl="7. assertion">
<proof prover="0"><result status="valid" time="2.07" steps="738"/></proof>
<proof prover="1"><result status="valid" time="2.95" steps="657"/></proof>
</goal>
<goal name="WP_parameter quicksort.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.53" steps="555"/></proof>
<proof prover="1"><result status="valid" time="0.53" steps="315"/></proof>
</goal>
<goal name="WP_parameter quicksort.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.16" steps="122"/></proof>
<proof prover="1"><result status="valid" time="0.16" steps="95"/></proof>
</goal>
<goal name="WP_parameter quicksort.10" expl="10. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="WP_parameter quicksort.11" expl="11. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
</transf>
</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="0"><result status="valid" time="0.02" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="WP_parameter qs.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="20"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter qs.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter qs.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter qs.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
</transf>
</goal>
......
examples/algo65/why3session.xml
View file @ 34c5aeb6
......@@ -2,135 +2,135 @@
<!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.95.2" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" 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="0"><result status="valid" time="0.00" steps="6"/></proof>
<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="0"><result status="valid" time="0.00" steps="11"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="WP_parameter find.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter find.4" expl="4. assertion">
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter find.5" expl="5. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="42"/></proof>
<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="0" timelimit="6"><result status="valid" time="0.19" steps="159"/></proof>
<proof prover="1" timelimit="6"><result status="valid" time="0.57" steps="248"/></proof>
</goal>
<goal name="WP_parameter find.6.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.11" steps="66"/></proof>
<proof prover="1"><result status="valid" time="0.35" steps="143"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter find.7" expl="7. variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter find.8" expl="8. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter find.9" expl="9. assertion">
<proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="WP_parameter find.10" expl="10. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter find.11" expl="11. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter find.12" expl="12. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="17"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter find.13" expl="13. postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="19"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="19"/></proof>
</goal>
<goal name="WP_parameter find.14" expl="14. postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="19"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="19"/></proof>
</goal>
<goal name="WP_parameter find.15" expl="15. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="65"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="45"/></proof>
</goal>
<goal name="WP_parameter find.16" expl="16. assertion">
<proof prover="0"><result status="valid" time="0.38" steps="178"/></proof>
<proof prover="1"><result status="valid" time="0.38" steps="320"/></proof>
</goal>
<goal name="WP_parameter find.17" expl="17. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="96"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="96"/></proof>
</goal>
<goal name="WP_parameter find.18" expl="18. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="32"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="WP_parameter find.19" expl="19. postcondition">
<proof prover="0"><result status="valid" time="0.31" steps="118"/></proof>
<proof prover="1"><result status="valid" time="0.31" steps="170"/></proof>
</goal>
<goal name="WP_parameter find.20" expl="20. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="36"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="29"/></proof>
</goal>
<goal name="WP_parameter find.21" expl="21. assertion">
<proof prover="0"><result status="valid" time="0.05" steps="48"/></proof>
<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="0"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter find.23" expl="23. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter find.24" expl="24. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="26"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="WP_parameter find.25" expl="25. assertion">
<proof prover="0"><result status="valid" time="0.04" steps="69"/></proof>
<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="0" timelimit="6"><result status="valid" time="0.24" steps="182"/></proof>
<proof prover="1" timelimit="6"><result status="valid" time="0.67" steps="380"/></proof>
</goal>
<goal name="WP_parameter find.26.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.25" steps="87"/></proof>
<proof prover="1"><result status="valid" time="0.25" steps="113"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter find.27" expl="27. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="87"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="87"/></proof>
</goal>
<goal name="WP_parameter find.28" expl="28. postcondition">
<proof prover="0"><result status="valid" time="0.19" steps="94"/></proof>
<proof prover="1"><result status="valid" time="0.19" steps="110"/></proof>
</goal>
<goal name="WP_parameter find.29" expl="29. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="32"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="WP_parameter find.30" expl="30. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter find.31" expl="31. assertion">
<proof prover="0"><result status="valid" time="0.04" steps="36"/></proof>
<proof prover="1"><result status="valid" time="0.04" steps="38"/></proof>
</goal>
<goal name="WP_parameter find.32" expl="32. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter find.33" expl="33. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="35"/></proof>
</goal>
<goal name="WP_parameter find.34" expl="34. postcondition">
<proof prover="0" timelimit="15"><result status="valid" time="0.03" steps="34"/></proof>
<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="0"><result status="valid" time="0.02" steps="20"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter find.36" expl="36. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter find.37" expl="37. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
</transf>
</goal>
......
examples/all_distinct/why3session.xml
View file @ 34c5aeb6
......@@ -2,46 +2,46 @@
<!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.95.2" timelimit="6" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="1" 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="0"><result status="valid" time="0.02" steps="2"/></proof>
<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="0"><result status="valid" time="0.01" steps="8"/></proof>
<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="0"><result status="valid" time="0.02" steps="8"/></proof>
<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="0"><result status="valid" time="0.02" steps="9"/></proof>
<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="0"><result status="valid" time="0.02" steps="7"/></proof>
<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="0"><result status="valid" time="0.02" steps="7"/></proof>
<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="0"><result status="valid" time="0.01" steps="9"/></proof>
<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="0"><result status="valid" time="0.01" steps="17"/></proof>
<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="0"><result status="valid" time="0.02" steps="10"/></proof>
<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="0"><result status="valid" time="0.02" steps="36"/></proof>
<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="0"><result status="valid" time="0.02" steps="33"/></proof>
<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="0"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
</transf>
</goal>
......
examples/avl/monoid/why3session.xml
View file @ 34c5aeb6
......@@ -2,21 +2,21 @@
<!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.95.2" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../monoid.mlw">
<theory name="Monoid" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="MonoidSum" sum="eabe70b6b30093b064a3f08ab415b7b3">
<goal name="WP_parameter sum_append" expl="VC for sum_append">
<proof prover="0"><result status="valid" time="0.03" steps="78"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="78"/></proof>
</goal>
</theory>
<theory name="MonoidSumDef" sum="91ea54c2bdb5e1284705678b5156c535">
<goal name="sum_def_nil">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="sum_def_cons">
<proof prover="0"><result status="valid" time="0.02" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
</theory>
<theory name="ComputableMonoid" sum="d41d8cd98f00b204e9800998ecf8427e">
......
examples/avl/preorder/why3session.xml
View file @ 34c5aeb6
......@@ -2,31 +2,31 @@
<!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.95.2" timelimit="3" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="1" memlimit="1000"/>
<file name="../preorder.mlw" expanded="true">
<theory name="Full" sum="41eddb6a5f9e7172479be99f6dc563ca" expanded="true">
<goal name="Eq.Refl" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="Eq.Trans" expanded="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="31"/></proof>
</goal>
<goal name="Eq.Symm" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="Lt.Trans" expanded="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="35"/></proof>
</goal>
<goal name="Lt.Asymm" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
</theory>
<theory name="TotalFull" sum="b7a34af67ae9cf9bf55e6d6a58a0f423" expanded="true">
<goal name="Lt.Total" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="lt_def2" expanded="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.02"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
</theory>
<theory name="Computable" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
......
examples/avl/ral/why3session.xml
View file @ 34c5aeb6
This diff is collapsed.
examples/avl/sorted/why3session.xml
View file @ 34c5aeb6
......@@ -2,33 +2,33 @@
<!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.95.2" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../sorted.mlw">
<theory name="Increasing" sum="33bff6ba91e99a4e930bd71eb88f6a0e">
<goal name="smaller_lower_bound">
<proof prover="0"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="bigger_upper_bound">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter increasing_precede" expl="VC for increasing_precede">
<transf name="split_goal_wp">
<goal name="WP_parameter increasing_precede.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="24"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="WP_parameter increasing_precede.2" expl="2. variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="20"/></proof>
</goal>
<goal name="WP_parameter increasing_precede.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.53" steps="425"/></proof>
<proof prover="1"><result status="valid" time="0.53" steps="381"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter increasing_midpoint" expl="VC for increasing_midpoint">
<proof prover="0"><result status="valid" time="0.26" steps="168"/></proof>
<proof prover="1"><result status="valid" time="0.26" steps="128"/></proof>
</goal>
<goal name="WP_parameter increasing_snoc" expl="VC for increasing_snoc">
<proof prover="0"><result status="valid" time="0.03" steps="47"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="25"/></proof>
</goal>
</theory>
</file>
......
examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_one_1.v
View file @ 34c5aeb6
(* This file is generated by Why3's Coq 8.4 driver *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
......@@ -202,21 +202,24 @@ Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).
Parameter bw_and: bv -> bv -> bv.
Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).
(n < size)%Z) -> ((nth (bw_and v1 v2) n) = (Init.Datatypes.andb (nth v1
n) (nth v2 n))).
Parameter bw_or: bv -> bv -> bv.
Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).
(n < size)%Z) -> ((nth (bw_or v1 v2) n) = (Init.Datatypes.orb (nth v1
n) (nth v2 n))).
Parameter bw_xor: bv -> bv -> bv.
Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).
(n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (Init.Datatypes.xorb (nth v1
n) (nth v2 n))).
Axiom Nth_bw_xor_v1true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2)
n) = (negb (nth v2 n))).
n) = (Init.Datatypes.negb (nth v2 n))).
Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v2
......@@ -224,7 +227,7 @@ Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
Axiom Nth_bw_xor_v2true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2)
n) = (negb (nth v1 n))).
n) = (Init.Datatypes.negb (nth v1 n))).
Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v1
......@@ -233,7 +236,7 @@ Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
Parameter bw_not: bv -> bv.
Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth (bw_not v) n) = (negb (nth v n))).
((nth (bw_not v) n) = (Init.Datatypes.negb (nth v n))).
Parameter lsr: bv -> Z -> bv.
......@@ -288,6 +291,7 @@ Axiom to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < size)%Z /\
k) = false)) -> ((to_nat_sub b j i) = 0%Z)).
Require Import Why3.
Ltac cvc := why3 "CVC3,2.4.1," timelimit 5; admit.
Open Scope Z_scope.
(* Why3 goal *)
......@@ -299,6 +303,6 @@ Theorem to_nat_of_one : forall (b:bv) (i:Z) (j:Z), ((j < size)%Z /\
intros b i j (Hj,(Hij,Hi)).
generalize Hij Hj.
pattern j; apply Zlt_lower_bound_ind with (z:=i); auto.
why3 "cvc3" timelimit 3.
Qed.
cvc.
Admitted.
examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_zero_1.v
View file @ 34c5aeb6
......@@ -287,8 +287,11 @@ Axiom to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), ((j < size)%Z /\
i 0%Z))).
Require Import Why3.
Ltac ae := why3 "Alt-Ergo,0.99.1," timelimit 5; admit.
Ltac cvc := why3 "CVC3,2.4.1," timelimit 5; admit.
Open Scope Z_scope.
(* Why3 goal *)
Theorem to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < size)%Z /\
(0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth b
......@@ -297,10 +300,10 @@ Theorem to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < size)%Z /\
(* intros b i j (h1,h2) h3. *)
intros b i j (Hj & Hi).
assert (h:(i>j)\/(i<=j)) by omega; destruct h.
why3 "Alt-Ergo,0.99.1," timelimit 2.
ae.
generalize Hj.
pattern j.
apply Zlt_lower_bound_ind with (z:=i); auto.
why3 "CVC3,2.4.1,".
Qed.
cvc.
Admitted.
examples/bitvectors/bitvector/bitvector_BitVector_to_nat_sub_footprint_1.v
View file @ 34c5aeb6
......@@ -149,15 +149,19 @@ Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).
Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z).
Axiom Div_double : forall (x:Z) (y:Z), (((0%Z < y)%Z /\ (y <= x)%Z) /\
(x < (2%Z * y)%Z)%Z) -> ((int.EuclideanDivision.div x y) = 1%Z).
Axiom Div_mult_inst : forall (x:Z) (z:Z), (0%Z < x)%Z ->
((int.EuclideanDivision.div ((x * 1%Z)%Z + z)%Z
x) = (1%Z + (int.EuclideanDivision.div z x))%Z).
Axiom Div_double : forall (x:Z) (y:Z), ((0%Z < y)%Z /\ ((y <= x)%Z /\
(x < (2%Z * y)%Z)%Z)) -> ((int.EuclideanDivision.div x y) = 1%Z).
Axiom Div_pow : forall (x:Z) (i:Z), (0%Z < i)%Z ->
((((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) ->
((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z)).
Axiom Div_double_neg : forall (x:Z) (y:Z), (((((-2%Z)%Z * y)%Z <= x)%Z /\
(x < (-y)%Z)%Z) /\ ((-y)%Z < 0%Z)%Z) -> ((int.EuclideanDivision.div x
Axiom Div_double_neg : forall (x:Z) (y:Z), ((((-2%Z)%Z * y)%Z <= x)%Z /\
((x < (-y)%Z)%Z /\ ((-y)%Z < 0%Z)%Z)) -> ((int.EuclideanDivision.div x
y) = (-2%Z)%Z).
Axiom Div_pow2 : forall (x:Z) (i:Z), (0%Z < i)%Z ->
......@@ -198,21 +202,24 @@ Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).
Parameter bw_and: bv -> bv -> bv.
Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).
(n < size)%Z) -> ((nth (bw_and v1 v2) n) = (Init.Datatypes.andb (nth v1
n) (nth v2 n))).
Parameter bw_or: bv -> bv -> bv.
Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).
(n < size)%Z) -> ((nth (bw_or v1 v2) n) = (Init.Datatypes.orb (nth v1
n) (nth v2 n))).
Parameter bw_xor: bv -> bv -> bv.
Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).
(n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (Init.Datatypes.xorb (nth v1
n) (nth v2 n))).
Axiom Nth_bw_xor_v1true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2)
n) = (negb (nth v2 n))).
n) = (Init.Datatypes.negb (nth v2 n))).
Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v2
......@@ -220,7 +227,7 @@ Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
Axiom Nth_bw_xor_v2true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2)
n) = (negb (nth v1 n))).
n) = (Init.Datatypes.negb (nth v1 n))).
Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v1
......@@ -229,7 +236,7 @@ Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
Parameter bw_not: bv -> bv.
Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth (bw_not v) n) = (negb (nth v n))).
((nth (bw_not v) n) = (Init.Datatypes.negb (nth v n))).
Parameter lsr: bv -> Z -> bv.
......@@ -263,19 +270,19 @@ Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
Parameter to_nat_sub: bv -> Z -> Z -> Z.
Axiom to_nat_sub_zero : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\
(i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = false) -> ((to_nat_sub b j
Axiom to_nat_sub_zero : forall (b:bv) (j:Z) (i:Z), ((0%Z <= i)%Z /\
((i <= j)%Z /\ (j < size)%Z)) -> (((nth b j) = false) -> ((to_nat_sub b j
i) = (to_nat_sub b (j - 1%Z)%Z i))).
Axiom to_nat_sub_one : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\
(i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = true) -> ((to_nat_sub b j
Axiom to_nat_sub_one : forall (b:bv) (j:Z) (i:Z), ((0%Z <= i)%Z /\