#pragma CIVL ACSL

$input int N;
$assume(N > 0);
$input int a[N];

int binary_search(long t[], int n, long v) {
  int l = 0, u = n-1;

  /*@ loop invariant 0 <= l && u <= n-1;
    @ loop invariant \forall integer k; 0 <= k < n && 
    @                                   (t[k] == v ==> l <= k && k <= u);
    @ loop assigns   l, u;   
    @*/
  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 
      return m;
  }
  return -1;
}

int main() {
  int v = 0;
  int ret = binary_search(a, N, v);
}