updated proof sessions

parent 1405ceaf
......@@ -6,8 +6,6 @@ bignum.mlw
bitcount.mlw
bitvector_examples.mlw
bitwalker.mlw
bresenham.mlw
bubble_sort.mlw
coincidence_count_list.mlw
conjugate.mlw
counting_sort.mlw
......@@ -31,7 +29,6 @@ foveoos11_challenge2.mlw
foveoos11_challenge3.mlw
gcd_bezout.mlw
gcd.mlw
generate_all_trees.mlw
hackers-delight.mlw
hashtbl_impl.mlw
ieee_float.mlw
......
......@@ -3,45 +3,14 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="4" name="Alt-Ergo" version="0.95.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="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bresenham.mlw" expanded="true">
<theory name="M" sum="3d5e82bb9f3ea61d2077393703418500" expanded="true">
<theory name="M" sum="8b33a83689687388b3fcf0a38496e94d" expanded="true">
<goal name="closest" expanded="true">
<proof prover="0" edited="bresenham_M_closest_1.v"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="WP_parameter bresenham" expl="VC for bresenham" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter bresenham.1" expl="1. loop invariant init" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter bresenham.2" expl="2. loop invariant init" expanded="true">
<proof prover="5"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter bresenham.3" expl="3. assertion" expanded="true">
<proof prover="4"><result status="valid" time="1.67" steps="132"/></proof>
<proof prover="5" timelimit="30"><result status="valid" time="1.18" steps="129"/></proof>
</goal>
<goal name="WP_parameter bresenham.4" expl="4. loop invariant preservation" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter bresenham.5" expl="5. loop invariant preservation" expanded="true">
<proof prover="5"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="WP_parameter bresenham.6" expl="6. loop invariant preservation" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter bresenham.7" expl="7. loop invariant preservation" expanded="true">
<proof prover="5"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
</transf>
<goal name="VC bresenham" expl="VC for bresenham" expanded="true">
<proof prover="2"><result status="valid" time="0.12" steps="69"/></proof>
</goal>
</theory>
</file>
......
......@@ -14,7 +14,7 @@ module BubbleSort
let bubble_sort (a: array int)
ensures { permut_all (old a) a }
ensures { sorted a }
= for i = length a - 1 downto 1 do
= "vc:liberal_for" for i = length a - 1 downto 1 do
invariant { permut_all (old a) a }
invariant { sorted_sub a i (length a) }
invariant { forall k1 k2: int.
......
This diff is collapsed.
......@@ -3,7 +3,6 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="3" name="CVC4" version="1.4" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="0.95.2" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="9" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
......@@ -23,103 +22,101 @@
</goal>
<goal name="VC combine" expl="VC for combine" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC combine.1" expl="1. variant decrease">
<goal name="VC combine.1" expl="1. variant decrease" expanded="true">
<proof prover="9"><result status="valid" time="0.01" steps="36"/></proof>
</goal>
<goal name="VC combine.2" expl="2. precondition">
<goal name="VC combine.2" expl="2. precondition" expanded="true">
<proof prover="9"><result status="valid" time="0.02" steps="131"/></proof>
</goal>
<goal name="VC combine.3" expl="3. postcondition">
<goal name="VC combine.3" expl="3. postcondition" expanded="true">
<proof prover="9"><result status="valid" time="0.28" steps="1380"/></proof>
</goal>
<goal name="VC combine.4" expl="4. postcondition">
<proof prover="3"><undone/></proof>
<goal name="VC combine.4" expl="4. postcondition" expanded="true">
<proof prover="9"><result status="valid" time="1.38" steps="5482"/></proof>
</goal>
<goal name="VC combine.5" expl="5. variant decrease">
<goal name="VC combine.5" expl="5. variant decrease" expanded="true">
<proof prover="9"><result status="valid" time="0.01" steps="30"/></proof>
</goal>
<goal name="VC combine.6" expl="6. precondition">
<goal name="VC combine.6" expl="6. precondition" expanded="true">
<proof prover="9"><result status="valid" time="0.02" steps="102"/></proof>
</goal>
<goal name="VC combine.7" expl="7. precondition">
<goal name="VC combine.7" expl="7. precondition" expanded="true">
<proof prover="9"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC combine.8" expl="8. postcondition">
<goal name="VC combine.8" expl="8. postcondition" expanded="true">
<proof prover="9"><result status="valid" time="0.14" steps="886"/></proof>
</goal>
<goal name="VC combine.9" expl="9. postcondition">
<proof prover="3"><undone/></proof>
<goal name="VC combine.9" expl="9. postcondition" expanded="true">
<proof prover="9"><result status="valid" time="2.42" steps="10937"/></proof>
</goal>
<goal name="VC combine.10" expl="10. precondition">
<goal name="VC combine.10" expl="10. precondition" expanded="true">
<proof prover="9"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="VC combine.11" expl="11. postcondition">
<goal name="VC combine.11" expl="11. postcondition" expanded="true">
<proof prover="9"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="VC combine.12" expl="12. postcondition">
<goal name="VC combine.12" expl="12. postcondition" expanded="true">
<proof prover="9"><result status="valid" time="0.01" steps="83"/></proof>
</goal>
</transf>
</goal>
<goal name="VC all_trees" expl="VC for all_trees" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC all_trees.1" expl="1. array creation size">
<goal name="VC all_trees.1" expl="1. array creation size" expanded="true">
<proof prover="9"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="VC all_trees.2" expl="2. index in array bounds">
<goal name="VC all_trees.2" expl="2. index in array bounds" expanded="true">
<proof prover="9"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC all_trees.3" expl="3. loop bounds">
<goal name="VC all_trees.3" expl="3. loop bounds" expanded="true">
<proof prover="9"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC all_trees.4" expl="4. loop invariant init">
<goal name="VC all_trees.4" expl="4. loop invariant init" expanded="true">
<proof prover="9"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC all_trees.5" expl="5. index in array bounds">
<goal name="VC all_trees.5" expl="5. index in array bounds" expanded="true">
<proof prover="9"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="VC all_trees.6" expl="6. loop bounds">
<goal name="VC all_trees.6" expl="6. loop bounds" expanded="true">
<proof prover="9"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="VC all_trees.7" expl="7. loop invariant init">
<goal name="VC all_trees.7" expl="7. loop invariant init" expanded="true">
<proof prover="9"><result status="valid" time="0.02" steps="175"/></proof>
</goal>
<goal name="VC all_trees.8" expl="8. loop invariant init">
<goal name="VC all_trees.8" expl="8. loop invariant init" expanded="true">
<proof prover="9"><result status="valid" time="0.00" steps="16"/></proof>
</goal>
<goal name="VC all_trees.9" expl="9. loop invariant init">
<goal name="VC all_trees.9" expl="9. loop invariant init" expanded="true">
<proof prover="9"><result status="valid" time="0.01" steps="63"/></proof>
</goal>
<goal name="VC all_trees.10" expl="10. index in array bounds">
<goal name="VC all_trees.10" expl="10. index in array bounds" expanded="true">
<proof prover="9"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="VC all_trees.11" expl="11. index in array bounds">
<goal name="VC all_trees.11" expl="11. index in array bounds" expanded="true">
<proof prover="9"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="VC all_trees.12" expl="12. index in array bounds">
<goal name="VC all_trees.12" expl="12. index in array bounds" expanded="true">
<proof prover="9"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="VC all_trees.13" expl="13. precondition">
<goal name="VC all_trees.13" expl="13. precondition" expanded="true">
<proof prover="9"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="VC all_trees.14" expl="14. index in array bounds">
<goal name="VC all_trees.14" expl="14. index in array bounds" expanded="true">
<proof prover="9"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="VC all_trees.15" expl="15. loop invariant preservation">
<goal name="VC all_trees.15" expl="15. loop invariant preservation" expanded="true">
<proof prover="9"><result status="valid" time="0.04" steps="158"/></proof>
</goal>
<goal name="VC all_trees.16" expl="16. loop invariant preservation">
<goal name="VC all_trees.16" expl="16. loop invariant preservation" expanded="true">
<proof prover="9"><result status="valid" time="0.05" steps="231"/></proof>
</goal>
<goal name="VC all_trees.17" expl="17. loop invariant preservation">
<goal name="VC all_trees.17" expl="17. loop invariant preservation" expanded="true">
<proof prover="9"><result status="valid" time="0.65" steps="2328"/></proof>
</goal>
<goal name="VC all_trees.18" expl="18. loop invariant preservation">
<goal name="VC all_trees.18" expl="18. loop invariant preservation" expanded="true">
<proof prover="9"><result status="valid" time="0.02" steps="177"/></proof>
</goal>
<goal name="VC all_trees.19" expl="19. postcondition">
<goal name="VC all_trees.19" expl="19. postcondition" expanded="true">
<proof prover="9"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
</transf>
......
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