/* Wensley's algorithm for real division */
float division (float P, float Q, float E)
pre( Q > P && P >= 0 && E > 0
);
{
float a,b,d,y;
a=0;
b=Q/2;
d=1;
y=0;
inv( a == Q*y && b == Q*d/2
&& P/Q - d < y && y <= P/Q
);
while( d>= E)
{
if (P< a+b)
{
b=b/2;
d=d/2;
}
else
{
a=a+b;
y=y+d/2;
b=b/2;
d=d/2;
}
}
return y;
}
post( P/Q >= result && result > P/Q
- E );