/* algorithm for finding the closest integer to the square root, from www.pedrofreire.com/crea2_en.htm?*/
int sqrt ( float a )
pre( a > 0 );
{
float x;
int r;
x=a/2;
r=0;
inv( a == 2*x + r^2 - r && x>0 );
while( x>r )
{
x=x-r;
r=r+1;
}
return r;
}
post( result^2 + result >= a && result^2 - result < a );