How can we prove by induction that binary search is correct?

Question

I'm having a hard time understanding how induction, coupled with some invariant, can be used to prove the correctness of algorithms. Namely, how is the invariant found, and when is the inductive hypothesis used- particularly for binary search? I haven't been able to find an intuitive response yet, so I was hoping someone could shed some light on the topic here.

Answer 1

Let's assume that binary search is defined like this:

def binary_search(a,b,e,x):
  n = e-b
  if n==0: return None
  m = b + int(n/2)
  if x<a[m]: return binary_search(a,b,m,x)
  if x>a[m]: return binary_search(a,m+1,e,x)
  return m

Where

• a is the array of values -- assumed sorted
• [b,e) is the range from b to e, including b but not including e, which we are searching through.
• x is the value we are searching for

The goal of the function is to return i where a[i]==x if there is such a value of i, otherwise return None.

binary_search works for a range of size zero:

• Proof: If the range contains no elements, then n==0 and the function returns None, which is correct.

Assuming binary_search works for a range of elements of any size from 0 to n, then binary search works for a range of elements of size n+1.

• Proof:

  Because the array is sorted, if x < a[m], then x < a[k] for all k > m. This means we only need to search the range [b,m). The range [b,m) is necessarily smaller than the range [b,e), and we've assumed that binary search works for all ranges of size smaller than n+1, so it will work for [b,m).

  If x > a[m], then similar logic applies.

  If x==a[m], then the function will return m, which is correct.