@axiom I: all i, j: int. all a : int farray. 
                     i =< j ==> a[i] =< a[j]

@requires n >= 1 &&  all(i, 0:n-1, a[i] =< a[i+1])

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

@program 

  @var lo, hi, x, p, n : int
  @var a: int[]

  lo = 0-1;
  hi = n;

  @invariant  
             // must not have a @var declaration for i and j

	     all(i, 0:n-1, a[i] =< a[i+1]) &&
             all(k, 0:lo, a[k] < x)  &&
	     all(k, hi:n-1, a[k] > x) &&
             lo+1 >= 0 && 
             lo+1 =< hi &&
             hi =< n
	     
  while (lo+1 < hi) {
	p = (lo+hi)/2;   // integer division; drop fraction
	if (a[p] == x) 
	   break;
        else if (a[p] < x) 
	   	lo = p;
	     else 
	   	hi = p;
  }

@end
--