@requires n >= 1

@ensures 
  (exists(k, 0:n-1, x = a[k]) <=> found)  &&
  (all(k, 0:n-1, x != a[k]) <=> not(found))

@program 
	   @var x, p, n : int
           @var found : bool
	   @var a: int[]

           p = 0;
	   found = false;

           @invariant p >= 0 && 
                      p =< n &&
                      (all(k, 0:p-1, x!=a[k]) <=> not(found))
           while (p < n) {
		if (x = a[p]) {
		    found = true;
		    break;
                }
		p = p + 1;
	   }
@end
--