@requires n > 2
@ensures (prime <=> all(k, 2:n-1, n%k != 0))

@program 

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

i = 2;
prime = true;

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

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

@end
--