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

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

    x = a;
    y = b;
    z = 0;

    inv( z+x*y==a*b );
    while( y!=0 ) 
        { 
        if ( y % 2 ==1 )
            {
            z = z+x;
            y = y-1;
            }
        x = 2*x;
        y = y/2;
        }
    return z; 
    }
post( result==a*b );