{n:nat}
int bsearch(key: int, vec: <int> array(n)) {
  var: low: [i: int | 0 <= i <= n] int(i);
       high: [j: int | 0 <= j + 1 <= n] int(j);
       int mid, x;;

  low = 0; high = vec.size - 1;

  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;
}