{n:nat}
int bsearch(key: float, vec[n]: float, size: int(n)) {
  var: int low, mid, high;
       float 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;
}