/* 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 );