Commit bd4383b4 authored by MARCHE Claude's avatar MARCHE Claude

example gcd_bezout: additional assert to help provers

parent 588edddb
......@@ -24,10 +24,11 @@ module GcdBezout
invariant { !c * (at !x 'Pre) + !d * (at !y 'Pre) = !y }
variant { !y }
let r = mod !x !y in let ghost q = div !x !y in
assert { r = !x - q * !y };
x := !y; y := r;
let ghost ta = !a in let ghost tb = !b in
a := !c; b := !d;
c := ta - !c * q; d := tb - !d * q
c := ta - !c * q; d := tb - !d * q;
done;
!x
......
......@@ -3,40 +3,45 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" memlimit="4000"/>
<prover id="3" name="Z3" version="4.4.1" timelimit="5" memlimit="4000"/>
<file name="../gcd_bezout.mlw" expanded="true">
<theory name="GcdBezout" sum="910432b1fed52122625d8689525e888a" expanded="true">
<theory name="GcdBezout" sum="64a68ff39d46e88e6208437a2eae11a6" expanded="true">
<goal name="WP_parameter gcd" expl="VC for gcd" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter gcd.1" expl="1. loop invariant init" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="2"/></proof>
<goal name="WP_parameter gcd.1" expl="1. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter gcd.2" expl="2. loop invariant init">
<proof prover="2"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="WP_parameter gcd.3" expl="3. loop invariant init" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="2"/></proof>
<goal name="WP_parameter gcd.3" expl="3. loop invariant init">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="WP_parameter gcd.4" expl="4. loop invariant preservation">
<proof prover="2"><result status="valid" time="1.39" steps="37"/></proof>
<goal name="WP_parameter gcd.4" expl="4. assertion">
<proof prover="1"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter gcd.5" expl="5. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.34" steps="19"/></proof>
<proof prover="1"><result status="valid" time="0.51" steps="41"/></proof>
</goal>
<goal name="WP_parameter gcd.6" expl="6. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.17" steps="14"/></proof>
<proof prover="1"><result status="valid" time="0.40" steps="16"/></proof>
</goal>
<goal name="WP_parameter gcd.7" expl="7. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<goal name="WP_parameter gcd.7" expl="7. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.31" steps="15"/></proof>
</goal>
<goal name="WP_parameter gcd.8" expl="8. loop variant decrease" expanded="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<goal name="WP_parameter gcd.8" expl="8. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.16" steps="15"/></proof>
</goal>
<goal name="WP_parameter gcd.9" expl="9. postcondition">
<proof prover="2"><result status="valid" time="0.17" steps="25"/></proof>
<goal name="WP_parameter gcd.9" expl="9. loop variant decrease">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter gcd.10" expl="10. postcondition">
<proof prover="2"><result status="valid" time="0.06" steps="25"/></proof>
<proof prover="1"><result status="valid" time="0.04" steps="25"/></proof>
</goal>
<goal name="WP_parameter gcd.11" expl="11. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="8"/></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