@requires n > 1

@ensures (isqrt*isqrt =< n ==> 
		(isqrt+1)*(isqrt+1) - n > n - isqrt*isqrt)
         &&
         (isqrt*isqrt > n ==> 
		n - (isqrt-1)*(isqrt-1) > isqrt*isqrt - n)

@program 

   @var hi, lo, n, isqrt : int

   hi = 1;

   @invariant n >= (hi-1)*(hi-1) && 
           1 =< hi

   while (hi*hi < n) {
        hi = hi + 1;
   }

   lo = hi-1;
   if (n-lo*lo < hi*hi-n) 
      isqrt = lo;
   else 
      isqrt = hi;

@end
--