@requires n > 2

@ensures (prime = 1 <=> all(k, 2:n-1, not(mod(n,k)= 0)))

@program 

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

i = 2;
prime = 1;

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

while (i < n) {
      if (mod(n,i) = 0) {
	     prime = 0;
             break;
          }
      i = i+1;
}

@end
--