('a){n:nat}
int bsearch(key: 'a, vec[n]: 'a, comparison: ('a, 'a) -> int) {
  var: int low, mid, high;
       int i; 'a x;;

  low = 0; high = arraysize(vec) - 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];
    i = comparison(x, key);
    if (i == 0) { return mid; }
    else if (i > 0) { high = mid - 1; }
         else { low = mid + 1; }
  }
  return -1;
}