/*@ lemma mean_1 : \forall integer x, integer y; x <= y ==> x <= (x+y)/2 <= y; */

/*@ requires
  @   n >= 0 && \valid_range(t,0,n-1) &&
  @   \forall int k1, int k2; 0 <= k1 <= k2 <= n-1 ==> t[k1] <= t[k2];
  @ ensures
  @   (\result >= 0 && t[\result] == v) ||
  @   (\result == -1 && \forall int k; 0 <= k < n ==> t[k] != v);
  @*/
int binary_search(int* t, int n, int v) {
  int l = 0, u = n-1, p = -1;
  /*@ loop invariant
    @   0 <= l && u <= n-1 && -1 <= p <= n-1
    @   && (p == -1 ==> \forall int k; 0 <= k < n ==> t[k] == v ==> l <= k <= u)
    @   && (p >= 0 ==> t[p]==v);
    @ loop variant u-l;
    @*/
  while (l <= u ) {
    int m = (l + u) / 2;
    //@ assert l <= m <= u;
    if (t[m] < v)
      l = m + 1;
    else if (t[m] > v)
      u = m - 1;
    else {
      p = m; break;
    }
  }
  return p;
}

/* 
Local Variables:
compile-command: "PPCHOME=../.. LC_ALL=C make binary_search"
End:
*/