@requires n >= 0

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

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

           p = 0;
	   found = 0;

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