{n:nat}
int bsearch(key: int, vec: <int> array(n)) {
  var: int low, mid, high, x;;

  low = 0; high = vec.size - 1;
  invariant:
    [i:int, j:int | 0 <= i <= n, 0 <= j+1 <= n] (low: int(i), high: int(j))
  while (low <= high) {
    mid = (low + high) / 2;
    x = vec.data[mid];
    if (key == x) { return mid; }
    else if (key < x) { high = mid - 1; }
         else { low = mid + 1; }
  }
  return -1;
}

int main () {
  var: int size, i; vec: <int> array;;

  size = 1000; vec = array {size = size; data = alloc(size, 0)};

  invariant: (i: nat)
  for (i=0; i < size; i=i+1) {
    vec.data[i] = i * i - 1;
  }

  return bsearch (80, vec);
}


/*
{n:nat}
int bsearch(key: int, size: int(n), vec[n]: int) {
  var: int low, mid, high, x;;

  low = 0; high = size - 1;
  invariant:
    [i:int, j:int | 0 <= i <= n, 0 <= j+1 <= n] (low: int(i), high: int(j))
  while (low <= high) {
    mid = (low + high) / 2;
    x = vec[mid];
    if (key == x) { return mid; }
    else if (key < x) { high = mid - 1; }
         else { low = mid + 1; }
  }
  return -1;
}

int main () {
  var: int size, i, vec[];;

  size = 1000; vec = alloc(size, 0);

  invariant: (i: nat)
  for (i=0; i < size; i=i+1) {
    vec[i] = i * i - 1;
  }

  return bsearch (80, size, vec);
}
*/