/* algorithm for computing the product of two natural numbers */

int prod (int x,int y)
pre( x >= 0 && y >= 0 ); 
    {
    int a,b,p,q;

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

    inv( q+abp==xy );
    while( a!=0 && b!=0 ) 
        { 
        if ( a % 2 ==0 && b% 2 ==0 )
            {
            a =a/2;
            b = b/2;
            p = 4p;
            }
        else if ( a % 2 ==1 && b% 2 ==0 )
            {
            a =a-1;
            q = q+bp;
            }
        else if ( a % 2 ==0 && b% 2 ==1 )
            {
            b =b-1;
            q = q+ap;
            }
        else
            {
            a =a-1;
            b =b-1;
            q = q+(a+b-1)p;
            }
        }
    return z; 
    }
post( result==xy );