## § Correctness of binary search

#### § Closed-closed intervals

// search in interval [l, r] for value val
int binsearch(int l, int r, int val, int *xs) {
if (l == r) { return l; }
int mid = (l+r)/2;
if (xs[mid] <= val) {
return binsearch(l, mid, val, xs);
} else {
return binsearch(mid+1, r, val, xs);
}
}

We have (l <= mid < r) since floor division of the form (l+r)/2 will pull values "downward". The length of the interval [l, mid] is smaller than the interval [l, r] as mid < r. The length of the interval [mid+1, r] is smaller than the interval [l, r] as l < mid+1. We are monotonically decreasing on the quantity "length of interval", and terminate the recursion when the length is zero.

#### § Closed-open intervals

// search in interval [l, r) for value val
int binsearch(int l, int r, int val, int *xs) {
// [l, l+1) = { l }
if (r == l + 1) { return l; }
int mid = (l+r)/2;
if (xs[mid] <= val) {
return binsearch(l, mid, val, xs);
} else {
return binsearch(mid, r, val, xs);
}
}

We have (l <= mid < r) since floor division of the form (l+r)/2 will pull values "downward". Furthermore, if r = l + 1 we end the recursion. Thus, we are guaranteed that we will have that r >= l + 2. Hence, mid = (l+r)/2 >= (l + l + 2)/2 >= l + 1. Thus, we have that: l is to the left of mid=l+1 is to the left of r>=l+2. So the intervals [l, mid) and [mid, r) will be smaller, as we cleanly "separate" out l, mid, and r.