/* algorithm computing the floor of the square root of a natural
number */
int sqrt (int n)
pre( n >= 0 );
{
int a,su,t;
a=0;
su=1;
t=1;
inv( a ^2 <= n &&
t == 2*a + 1 && su == ( a + 1 ) ^2
);
while ( su <= n )
{
a=a+1;
t=t+2;
su=su+t;
}
return a;
}
post( result ^2 <= n && (
result + 1 ) ^2 > n );