/* 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( b!=0 )
{
int c,quot;
c=a;
quot=0;
inv( GCD(a,b)==GCD(x,y) && a==y*r+x*p && b==x*q+y*s && a==quot*b+c );
while( c>=b )
{
int d,dd;
d=1;
dd=b;
inv( GCD(a,b)==GCD(x,y) && a==y*r+x*p && b==x*q+y*s && a==quot*b+c && dd==b*d );
while ( c>= 2*dd )
{
d = 2*d;
dd = 2*dd;
}
c=c-dd;
quot=quot+d;
}
a=b;
b=c;
{
int temp;
temp=p;
p=q;
q=temp-q*quot;
temp=r;
r=s;
s=temp-s*quot;
}
assert( GCD(x,y)==y*r+x*p );
return a;
}
post( result==GCD(x,y) );