Gcd function

Here is a static method for computing the greatests common divisor of two non-negative integers.

0pt class Gcd { 
 
    static int gcd(int x, int y) { 
        while (y > 0) { 
            int r = x % y; 
            x = y; 
            y = r; 
        } 
        return x; 
    } 
 
} 
  1. Give a direct definition of the predicate divides(x,y) expressing that x divides y
  2. Give a direct definition of the predicate isGcd(x,y,d) expressing that d is the gcd of x and y.
  3. Annotate the code with a behavior expressing that the result is the gcd of x and y.
  4. Prove the behavior. Hint: add some lemmas about isGcd, that you can leave unproved.
  5. Add another behavior expressing Bezout property: there exists a and b such that xa+yb=d.
  6. Instrument the code with ghost variables in order to prove that new behavior.
This document was translated from LATEX by HEVEA.