gcd_bezout: slightly nicer code

parent 7c50ae7b
......@@ -8,28 +8,27 @@ module GcdBezout
use number.Gcd
use ref.Ref
let gcd (x:int) (y:int)
let gcd (x y: int) : (result: int, ghost a: int, ghost b: int)
requires { x >= 0 /\ y >= 0 }
ensures { result = gcd x y }
ensures { exists a b:int. a*x+b*y = result }
ensures { a*x + b*y = result }
=
let x = ref x in let y = ref y in
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
while !y > 0 do
invariant { !x >= 0 /\ !y >= 0 }
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 }
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;
done;
!x
!x, !a, !b
end
......@@ -3,7 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.5" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../gcd_bezout.mlw" proved="true">
<theory name="GcdBezout" proved="true">
<goal name="VC gcd" expl="VC for gcd" proved="true">
......@@ -26,28 +26,26 @@
<goal name="VC gcd.5" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="VC gcd.6" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
<goal name="VC gcd.6" expl="loop variant decrease" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC gcd.7" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<goal name="VC gcd.7" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.18" steps="38"/></proof>
</goal>
<goal name="VC gcd.8" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.18" steps="42"/></proof>
<proof prover="0"><undone/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC gcd.9" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.09" steps="19"/></proof>
<proof prover="0"><result status="valid" time="0.09" steps="18"/></proof>
</goal>
<goal name="VC gcd.10" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.09" steps="19"/></proof>
<proof prover="0"><result status="valid" time="1.51" steps="64"/></proof>
</goal>
<goal name="VC gcd.11" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.09" steps="20"/></proof>
</goal>
<goal name="VC gcd.12" expl="postcondition" proved="true">
<goal name="VC gcd.11" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="VC gcd.13" expl="postcondition" proved="true">
<goal name="VC gcd.12" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></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