@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

@axiom I4: all x,y: int. x =< y ==> isqrt(x) =< isqrt(y)

@requires n >= 2

@ensures prime <=> all(k, 2:isqrt(n), mod(n,k) != 0)

@program 

// must not declare k
@var  i, n, isq : int
@var  prime : bool

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;}
}

i = 2;
prime = true;

@invariant 2 =< i && i=<isq+1 && 
           (prime <=> all(k, 2:i-1, mod(n,k) != 0))

while (i =< isq) {
      if (mod(n,i) == 0) {
	     prime = false; 
             break;
          }
      i = i+1;
}
@end
--