Commit 45e79180 authored by MARCHE Claude's avatar MARCHE Claude

example: linked list rev, updated session on moloch

parent c686623e
......@@ -2,36 +2,36 @@
<!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" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="10" memlimit="1000"/>
<prover id="6" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="10" steplimit="1" memlimit="1000"/>
<prover id="6" name="Z3" version="4.4.0" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../linked_list_rev.mlw" expanded="true">
<theory name="Disjoint" sum="9c582db93bf8e816b74d113c3748231e">
<theory name="Disjoint" sum="d9538770c8f60c61e92f6baffbf62d5d">
<goal name="WP_parameter mem_decomp" expl="VC for mem_decomp">
<proof prover="3"><result status="valid" time="0.02" steps="48"/></proof>
</goal>
</theory>
<theory name="InPlaceRev" sum="a7297b137cc5c020b4e5c498e6a72165" expanded="true">
<theory name="InPlaceRev" sum="79182a5e3856c7f8aff3c51d7a23476f" expanded="true">
<goal name="WP_parameter list_seg_frame_ext" expl="VC for list_seg_frame_ext">
<proof prover="3"><result status="valid" time="0.16" steps="242"/></proof>
<proof prover="3"><result status="valid" time="0.16" steps="236"/></proof>
</goal>
<goal name="WP_parameter list_seg_functional" expl="VC for list_seg_functional">
<proof prover="3"><result status="valid" time="0.10" steps="357"/></proof>
<proof prover="3"><result status="valid" time="0.10" steps="278"/></proof>
</goal>
<goal name="WP_parameter list_seg_sublistl" expl="VC for list_seg_sublistl">
<proof prover="0"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="WP_parameter list_seg_no_repet" expl="VC for list_seg_no_repet">
<proof prover="3"><result status="valid" time="0.36" steps="245"/></proof>
<proof prover="3"><result status="valid" time="0.05" steps="179"/></proof>
</goal>
<goal name="WP_parameter list_seg_append" expl="VC for list_seg_append">
<proof prover="3"><result status="valid" time="0.23" steps="721"/></proof>
<proof prover="3"><result status="valid" time="0.23" steps="615"/></proof>
</goal>
<goal name="WP_parameter app" expl="VC for app">
<transf name="split_goal_wp">
<goal name="WP_parameter app.1" expl="1. postcondition">
<proof prover="3"><result status="valid" time="0.03" steps="30"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="24"/></proof>
</goal>
<goal name="WP_parameter app.2" expl="2. loop invariant init">
<proof prover="3"><result status="valid" time="0.01" steps="4"/></proof>
......@@ -52,7 +52,7 @@
<proof prover="3"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter app.8" expl="8. unreachable point">
<proof prover="3"><result status="valid" time="0.06" steps="91"/></proof>
<proof prover="3"><result status="valid" time="0.06" steps="76"/></proof>
</goal>
<goal name="WP_parameter app.9" expl="9. precondition">
<proof prover="3"><result status="valid" time="0.01" steps="13"/></proof>
......@@ -64,13 +64,13 @@
<proof prover="5" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter app.12" expl="12. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.08" steps="148"/></proof>
<proof prover="3"><result status="valid" time="0.08" steps="137"/></proof>
</goal>
<goal name="WP_parameter app.13" expl="13. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.06" steps="143"/></proof>
<proof prover="3"><result status="valid" time="0.06" steps="180"/></proof>
</goal>
<goal name="WP_parameter app.14" expl="14. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.32" steps="694"/></proof>
<proof prover="3"><result status="valid" time="0.32" steps="670"/></proof>
</goal>
<goal name="WP_parameter app.15" expl="15. loop variant decrease">
<proof prover="3"><result status="valid" time="0.03" steps="46"/></proof>
......@@ -79,13 +79,13 @@
<proof prover="3"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter app.17" expl="17. assertion">
<proof prover="3"><result status="valid" time="0.16" steps="91"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="31"/></proof>
</goal>
<goal name="WP_parameter app.18" expl="18. assertion">
<proof prover="3"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="WP_parameter app.19" expl="19. assertion">
<proof prover="3"><result status="valid" time="0.32" steps="312"/></proof>
<proof prover="3"><result status="valid" time="0.32" steps="283"/></proof>
</goal>
<goal name="WP_parameter app.20" expl="20. postcondition">
<proof prover="0"><result status="valid" time="0.23"/></proof>
......@@ -107,19 +107,19 @@
<proof prover="3"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter in_place_reverse.5" expl="5. assertion">
<proof prover="3"><result status="valid" time="0.09" steps="153"/></proof>
<proof prover="3"><result status="valid" time="0.09" steps="46"/></proof>
</goal>
<goal name="WP_parameter in_place_reverse.6" expl="6. unreachable point">
<proof prover="3"><result status="valid" time="0.05" steps="165"/></proof>
<proof prover="3"><result status="valid" time="0.05" steps="140"/></proof>
</goal>
<goal name="WP_parameter in_place_reverse.7" expl="7. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.30" steps="591"/></proof>
<proof prover="3"><result status="valid" time="0.30" steps="526"/></proof>
</goal>
<goal name="WP_parameter in_place_reverse.8" expl="8. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.11" steps="240"/></proof>
<proof prover="3"><result status="valid" time="0.11" steps="215"/></proof>
</goal>
<goal name="WP_parameter in_place_reverse.9" expl="9. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.56" steps="431"/></proof>
<proof prover="3"><result status="valid" time="0.56" steps="405"/></proof>
</goal>
<goal name="WP_parameter in_place_reverse.10" expl="10. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
......@@ -128,12 +128,12 @@
<proof prover="3"><result status="valid" time="0.02" steps="58"/></proof>
</goal>
<goal name="WP_parameter in_place_reverse.12" expl="12. postcondition">
<proof prover="3"><result status="valid" time="0.06" steps="163"/></proof>
<proof prover="3"><result status="valid" time="0.06" steps="139"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="InPlaceRevSeq" sum="30a608b3a69381c1200472269902ac18" expanded="true">
<theory name="InPlaceRevSeq" sum="41f050ae287b51370da0688bf7f2e2df" expanded="true">
<goal name="WP_parameter mem_decomp" expl="VC for mem_decomp">
<transf name="split_goal_wp">
<goal name="WP_parameter mem_decomp.1" expl="1. postcondition">
......@@ -146,7 +146,7 @@
<proof prover="3" timelimit="60"><result status="valid" time="0.04" steps="15"/></proof>
</goal>
<goal name="WP_parameter mem_decomp.4" expl="4. precondition">
<proof prover="6" timelimit="60"><result status="valid" time="12.20"/></proof>
<proof prover="6" timelimit="60"><result status="valid" time="15.92"/></proof>
</goal>
<goal name="WP_parameter mem_decomp.5" expl="5. postcondition">
<proof prover="3" timelimit="60"><result status="valid" time="0.02" steps="8"/></proof>
......@@ -232,7 +232,7 @@
<proof prover="3" timelimit="10"><result status="valid" time="0.03" steps="2"/></proof>
</goal>
<goal name="WP_parameter list_seg_prefix.2" expl="2. precondition">
<proof prover="3" timelimit="10"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="3" timelimit="10"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter list_seg_prefix.3" expl="3. variant decrease">
<proof prover="3" timelimit="10"><result status="valid" time="0.06" steps="22"/></proof>
......@@ -241,10 +241,10 @@
<proof prover="3" timelimit="10"><result status="valid" time="0.05" steps="60"/></proof>
</goal>
<goal name="WP_parameter list_seg_prefix.5" expl="5. postcondition">
<proof prover="5"><result status="valid" time="2.03"/></proof>
<proof prover="5"><result status="valid" time="1.56"/></proof>
</goal>
<goal name="WP_parameter list_seg_prefix.6" expl="6. postcondition">
<proof prover="3" timelimit="10"><result status="valid" time="2.51" steps="1137"/></proof>
<proof prover="3" timelimit="10"><result status="valid" time="0.98" steps="724"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......@@ -270,7 +270,7 @@
<proof prover="3" timelimit="25"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter list_seg_sublistl.7" expl="7. postcondition">
<proof prover="3" timelimit="25"><result status="valid" time="0.36" steps="529"/></proof>
<proof prover="3" timelimit="25"><result status="valid" time="0.36" steps="543"/></proof>
</goal>
</transf>
</goal>
......@@ -368,7 +368,7 @@
<proof prover="3" timelimit="10"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter app.11" expl="11. loop invariant preservation">
<proof prover="5"><result status="valid" time="2.53"/></proof>
<proof prover="5"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="WP_parameter app.12" expl="12. loop invariant preservation">
<proof prover="3" timelimit="10"><result status="valid" time="0.02" steps="16"/></proof>
......@@ -383,7 +383,7 @@
<proof prover="3" timelimit="10"><result status="valid" time="0.09" steps="123"/></proof>
</goal>
<goal name="WP_parameter app.13.1.1.2" expl="2. VC for app">
<proof prover="5"><result status="valid" time="0.63"/></proof>
<proof prover="5"><result status="valid" time="0.16"/></proof>
</goal>
</transf>
</goal>
......@@ -392,7 +392,7 @@
</transf>
</goal>
<goal name="WP_parameter app.14" expl="14. loop invariant preservation">
<proof prover="5"><result status="valid" time="9.61"/></proof>
<proof prover="5"><result status="valid" time="2.52"/></proof>
</goal>
<goal name="WP_parameter app.15" expl="15. loop variant decrease">
<proof prover="3" timelimit="10"><result status="valid" time="0.85" steps="346"/></proof>
......@@ -403,7 +403,7 @@
<proof prover="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter app.17" expl="17. assertion">
<proof prover="3" timelimit="10"><result status="valid" time="0.09" steps="109"/></proof>
<proof prover="3" timelimit="10"><result status="valid" time="0.09" steps="107"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter app.18" expl="18. assertion">
......@@ -414,7 +414,7 @@
<proof prover="5"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter app.20" expl="20. postcondition">
<proof prover="5"><result status="valid" time="0.47"/></proof>
<proof prover="5"><result status="valid" time="0.72"/></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