@function isqrt: int -> int

@axiom I1: isqrt(1) = 1
@axiom I2: all n,k:int. k*k = n ==> isqrt(n) = k
@axiom I3: all n,k:int. k*k < n && (k+1)*(k+1) > n ==> isqrt(n) = k

@requires n > 0                     
@ensures isq = isqrt(n)

@program 
@var  isq, n : int

isq = 1;  

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