# How can induction be used to prove binary search is correct?

I'm having trouble understanding how to find an invariant to check if it's preserved, and generally how induction is used in proving the correctness of algorithms (binary search primarily, but others as well).

-

This is my interpretation of how to answer the question (perhaps there are others).

In binary search, we search a sorted list $L$ for an element $x$. The invariant that is preserved by binary search is the truth value of the statement "$x$ is in $L$".

In each iteration, we compare $x$ with a middle element $m$ of the list $L$.

1. If $L$ is empty, then "$x$ is in $L$" is false.
2. If $x=m$, then "$x$ is in $L$" is true.
3. If $x<m$ then we perform binary search on a new sorted list formed by the elements in $L$ that are less than $m$.
4. If $x>m$ then we perform binary search on a new sorted list formed by the elements in $L$ that are greater than $m$.

So to prove binary search is correct, we need to check that the truth value of "$x$ is in $L$" is preserved by 3. to 4. above. (1. and 2. form the base cases; there are actually infinitely many of them, but they're true by definition.)

We should also note that 3. and 4. both reduce the size of $L$ (which is why induction applies).

-

An invariant is a predicate that is provably true at certain places in your algorithm, and is meaningful for what the algorithm is meant to accomplish.

In this case, it must be true before each iteration of the loop (or, equivalently, just prior to each recursive function call, if that's your thing). And it must also be true after the loop terminates. (More technically, you must prove that it is true before the first iteration, and if it true before any iteration then it will still be true after that iteration.)

The part that really drives the selection of an invariant is an understanding of what it is that the algorithm is meant to accomplish. For example, in a binary search of an ordered array we want to get the index of a particular item, or a signal that the item is not in the array. So we have an array $A$ and a value $v$ that is being sought. So our final goal is to find a number $i$ so that $$A[i] = v$$ when the algorithm terminates.

There are a couple of reasons why this doesn't work as a loop invariant. First, it ignores the condition for when the value isn't in the array. This could be handled by a separate case, if we wanted to. But the other problem with this is that it is not true at the beginning of every iteration. It is only true at the very end. So that won't work.

So what is true at every iteration? The key feature of a binary search is that we have an ever-narrowing range of values in the array which could contain the answer. This range is bounded by a high value $h$ and a low value $l$. For example, $$A[l] \le v \le A[h]$$ contains the key piece of what is always true in a binary search. But that isn't really enough to prove that the algorithm is correct. We also have to make sure that it will terminate at some point. So for each iteration $t$ we also have $$h_{t} - l_{t} < h_{t-1} - l_{t-1}$$ meaning that the subrange under consideration gets smaller at each iteration. From this you can show by induction that the loop will terminate.

Each of these conditions should be easy to prove from your code (with the initial conditions $A[x] < A[j] \iff x < j, l = 0, h = |A| - 1$ etc.). Then you can easily prove at the end (when $h = l$) that $A[h] = v \iff v \in A$ or whatever.

-