/* binary division algorithm, by Kaldewaij */
int division (int A, int B)
pre( A >= 0 && B > 0 );
{
int q,r,b;
q=0;
r=A;
b=B;
inv( exists ( int k; k >= 0 && b ==
2^k*B ) && q == 0 &&
r == A && A >= 0 && B > 0 );
while(r>=b)
{
b=2*b;
}
inv( A == q*b + r && r >= 0
&& exists ( int k; k >= 0 && b == 2^k*B )
&& B > 0 && b > r );
while(b!=B)
{
q=2*q;
b=b/2;
if (r>=b)
{
q=q+1;
r=r-b;
}
}
assert(q==A/B);
return r;
}
post( result == A % B);