@function isqrt: int -> int
@function isq: int,int -> int

@axiom A1: all k:int. all n:int. k*k > n ==> isq(k,n) = k-1
@axiom A2: all k:int. all n:int. k*k = n ==> isq(k,n) = k
@axiom A3: all k:int. all n:int. k*k < n ==> isq(k,n) = isq(k+1,n)

@axiom I1: isqrt(1) = 1
@axiom I2: all n:int. n > 1 ==> isqrt(n) = isq(2,n)

@requires isqrt(n) >= 2

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

@program 

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

i = 2;
prime = true;

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

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