Commit 8e710b9a authored by MARCHE Claude's avatar MARCHE Claude

example gcd_bezout, with version using fast WP

parent ae5c5eef
......@@ -14,16 +14,17 @@ module GcdBezout
ensures { exists a b:int. a*x+b*y = result }
=
let x = ref x in let y = ref y in
'Pre:
label Pre in
let ghost a = ref 1 in let ghost b = ref 0 in
let ghost c = ref 0 in let ghost d = ref 1 in
while (!y > 0) do
invariant { !x >= 0 /\ !y >= 0 }
invariant { gcd !x !y = gcd (at !x 'Pre) (at !y 'Pre) }
invariant { !a * (at !x 'Pre) + !b * (at !y 'Pre) = !x }
invariant { !c * (at !x 'Pre) + !d * (at !y 'Pre) = !y }
invariant { gcd !x !y = gcd (!x at Pre) (!y at Pre) }
invariant { !a * (!x at Pre) + !b * (!y at Pre) = !x }
invariant { !c * (!x at Pre) + !d * (!y at 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;
......
......@@ -2,41 +2,53 @@
<!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" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="4000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../gcd_bezout.mlw" expanded="true">
<theory name="GcdBezout" sum="ee56a3971a32c0af67845daaf6066a93" expanded="true">
<goal name="WP_parameter gcd" expl="VC for gcd" expanded="true">
<theory name="GcdBezout" sum="7318637ab33e07e39a6842bed7a1f44b" expanded="true">
<goal name="VC 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="1"><result status="valid" time="0.01"/></proof>
<goal name="VC gcd.1" expl="1. loop invariant init">
<proof prover="2"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter gcd.2" expl="2. loop invariant init">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<goal name="VC gcd.2" expl="2. loop invariant init">
<proof prover="2"><result status="valid" time="0.02" steps="0"/></proof>
</goal>
<goal name="WP_parameter gcd.3" expl="3. loop invariant init" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<goal name="VC gcd.3" expl="3. loop invariant init">
<proof prover="2"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter gcd.4" expl="4. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.79"/></proof>
<goal name="VC gcd.4" expl="4. loop invariant init">
<proof prover="2"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="WP_parameter gcd.5" expl="5. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<goal name="VC gcd.5" expl="5. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter gcd.6" expl="6. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<goal name="VC gcd.6" expl="6. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="8"/></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="VC gcd.7" expl="7. assertion">
<proof prover="2"><result status="valid" time="0.03" steps="12"/></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="VC gcd.8" expl="8. loop invariant preservation">
<proof prover="2"><result status="valid" time="1.14" steps="41"/></proof>
</goal>
<goal name="WP_parameter gcd.9" expl="9. postcondition">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<goal name="VC gcd.9" expl="9. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.13" steps="16"/></proof>
</goal>
<goal name="WP_parameter gcd.10" expl="10. postcondition">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<goal name="VC gcd.10" expl="10. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.06" steps="15"/></proof>
</goal>
<goal name="VC gcd.11" expl="11. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.16" steps="15"/></proof>
</goal>
<goal name="VC gcd.12" expl="12. loop variant decrease" expanded="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC gcd.13" expl="13. postcondition">
<proof prover="2"><result status="valid" time="0.05" steps="25"/></proof>
</goal>
<goal name="VC gcd.14" expl="14. postcondition">
<proof prover="2"><result status="valid" time="0.03" steps="25"/></proof>
</goal>
</transf>
</goal>
......
<?xml version="1.0" encoding="UTF-8"?>
<!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.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../gcd_bezout.mlw" expanded="true">
<theory name="GcdBezout" sum="e56e39dcd05a8b28864b366f7744395c" expanded="true">
<goal name="VC gcd" expl="VC for gcd" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC gcd.1" expl="1. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="VC gcd.2" expl="2. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="0"/></proof>
</goal>
<goal name="VC gcd.3" expl="3. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="VC gcd.4" expl="4. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="VC gcd.5" expl="5. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC gcd.6" expl="6. precondition">
<proof prover="0"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
<goal name="VC gcd.7" expl="7. assertion">
<proof prover="0"><result status="valid" time="0.03" steps="12"/></proof>
</goal>
<goal name="VC gcd.8" expl="8. loop invariant preservation">
<proof prover="0"><result status="valid" time="1.19" steps="41"/></proof>
</goal>
<goal name="VC gcd.9" expl="9. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.16" steps="16"/></proof>
</goal>
<goal name="VC gcd.10" expl="10. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.16" steps="15"/></proof>
</goal>
<goal name="VC gcd.11" expl="11. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.22" steps="15"/></proof>
</goal>
<goal name="VC gcd.12" expl="12. loop variant decrease">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC gcd.13" expl="13. postcondition">
<proof prover="0"><result status="valid" time="0.12" steps="30"/></proof>
</goal>
<goal name="VC gcd.14" expl="14. postcondition">
<proof prover="0"><result status="valid" time="0.16" steps="30"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
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