/* algorithm for computing simultaneously the GCD and the LCM, by Sankaranarayanan */
int lcm (int a, int b)
pre( a>0 && b>0 );
{
int x,y,u,v;
x=a;
y=b;
u=b;
v=0;
inv( GCD(x,y) == GCD(a,b) && x*u + y*v == a*b );
while(x!=y)
{
inv( GCD(x,y) == GCD(a,b) && x*u + y*v == a*b );
while (x>y)
{
x=x-y;
v=v+u;
}
inv( GCD(x,y) == GCD(a,b) && x*u + y*v == a*b );
while (x<y)
{
y=y-x;
u=u+v;
}
}
return u+v;
}
post( result == LCM(a,b) );