/* extended Euclid's algorithm */

int gcd (int x, int y)
pre(  x > 0  &&  y > 0   ); 
    {
    int a,b,p,q,r,s;

    a=x;
    b=y;
    p=1;
    q=0;
    r=0;
    s=1;

    inv(    GCD(a,b) == GCD(x,y)    &&    a == y*r + x*p    &&    b == x*q + y*s    );
    while(a!=b) 
        { 

        if (a>b) {a = a-b; p = p-q; r=r-s;}

        else {b = b-a; q = q-p; s = s-r;}

        }

    assert(   GCD(x,y) == y*r + x*p   );

    return a;
    }
post(   result==GCD(x,y)   );