Commit 574642cf authored by Martin Clochard's avatar Martin Clochard

update proof sessions

parent 65c0633c
......@@ -9,7 +9,6 @@ esterel.mlw
ewd673.mlw
fibonacci.mlw
find.mlw
finite_tarski.mlw
gcd.mlw
hackers-delight.mlw
hashtbl_impl.mlw
......
......@@ -2,18 +2,50 @@
<!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"/>
<file name="../finite_tarski.mlw" expanded="true">
<theory name="Tarski" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../finite_tarski.mlw">
<theory name="Tarski" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Tarski_rec" sum="ce480e189cfd29d29e9e2e61ceebe833" expanded="true">
<goal name="WP_parameter least_fix_point" expl="VC for least_fix_point" expanded="true">
<proof prover="0"><result status="valid" time="0.15"/></proof>
<theory name="Tarski_rec" sum="be2611fed1bae1fd8d47c34cd2783601">
<goal name="VC least_fix_point" expl="VC for least_fix_point">
<proof prover="2"><result status="valid" time="0.10" steps="462"/></proof>
</goal>
</theory>
<theory name="Tarski_while" sum="dfcdd727fd1b802f81fc5c84ff819eda" expanded="true">
<goal name="WP_parameter least_fix_point" expl="VC for least_fix_point" expanded="true">
<proof prover="0"><result status="valid" time="0.19"/></proof>
<theory name="Tarski_while" sum="c808f92413ae599648f05a5a183d93eb">
<goal name="VC least_fix_point" expl="VC for least_fix_point">
<transf name="split_goal_wp">
<goal name="VC least_fix_point.1" expl="1. loop invariant init">
<proof prover="2"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="VC least_fix_point.2" expl="2. loop invariant init">
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC least_fix_point.3" expl="3. loop invariant init">
<proof prover="2"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="VC least_fix_point.4" expl="4. loop invariant init">
<proof prover="2"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="VC least_fix_point.5" expl="5. loop variant decrease">
<proof prover="2"><result status="valid" time="0.04" steps="77"/></proof>
</goal>
<goal name="VC least_fix_point.6" expl="6. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02" steps="54"/></proof>
</goal>
<goal name="VC least_fix_point.7" expl="7. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02" steps="67"/></proof>
</goal>
<goal name="VC least_fix_point.8" expl="8. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="VC least_fix_point.9" expl="9. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="VC least_fix_point.10" expl="10. postcondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
......
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