Gcd function
Here is a static method for computing the greatests common divisor of
two nonnegative integers.
0pt
class Gcd {
static int gcd(int x, int y) {
while (y > 0) {
int r = x % y;
x = y;
y = r;
}
return x;
}
}

Give a direct definition of the predicate divides(x,y)
expressing that x divides y
 Give a direct definition of the predicate isGcd(x,y,d)
expressing that d is the gcd of x and y.
 Annotate the code with a behavior expressing that the result is
the gcd of x and y.
 Prove the behavior. Hint: add some lemmas about isGcd, that
you can leave unproved.
 Add another behavior expressing Bezout property: there
exists a and b such that xa+yb=d.
 Instrument the code with ghost variables in order to prove that
new behavior.
This document was translated from L^{A}T_{E}X by
H^{E}V^{E}A.