/* algorithm for computing simultaneously the GCD and the LCM, by Dijkstra */

int lcm (int a, int b)
pre(  a > 0   &&   b > 0  ); 
    {
    int x,y,u,v;

    x=a;
    y=b;
    u=b;
    v=a;

    inv(   GCD(x,y) == GCD(a,b)   &&   x>0   &&   y>0   &&   x*u + y*v == 2*a*b  );
    while(x!=y) 
        { 
        if (x>y)
            {
            x=x-y;
            v=v+u;
            }
        else 
            {
            y=y-x;
            u=u+v;
            }
        }


    return (u+v)/2;
    }
post(   result == LCM(a,b)   );