@requires n > 1

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

@program 

  @var i, n, isqrt : int
  i = 1;

  @invariant n >= (i-1)*(i-1) && 
           1 =< i
  while (i*i < n) {
      i = i + 1;
  }
  if (i*i > n)
      isqrt = i-1;
  else 
      isqrt = i;
@end
--