Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
c07f1a25
Commit
c07f1a25
authored
Mar 04, 2013
by
Jean-Christophe Filliâtre
Browse files
gcd_bezout: this is ghost code
parent
43b684d0
Changes
1
Hide whitespace changes
Inline
Side-by-side
examples/gcd_bezout.mlw
View file @
c07f1a25
...
...
@@ -12,19 +12,20 @@ module GcdBezout
requires { x >= 0 /\ y >= 0 }
ensures { result = gcd x y }
ensures { exists a b:int. a*x+b*y = result }
= let x = ref x in let y = ref y in
=
let x = ref x in let y = ref y in
'Pre:
let a = ref 1 in let b = ref 0 in
let c = ref 0 in let d = ref 1 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 }
variant { !y }
let r = mod !x !y in let q = div !x !y in
let r = mod !x !y in let
ghost
q = div !x !y in
x := !y; y := r;
let ta = !a in let tb = !b in
let
ghost
ta = !a in let
ghost
tb = !b in
a := !c; b := !d;
c := ta - !c * q; d := tb - !d * q
done;
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment