Every Programmer Should Know Some Formal Proof

I believe every programmer should know some formal proof techniques. It helps with reasoning, and even more importantly, it helps you write correct implementations.

In recent interviews, I found that nearly half of the candidates could not correctly complete a binary search (or, more precisely, one of its variants). Some of these candidates had 3–5 years of work experience, while others were excellent recent graduates in computer science. I was surprised that none of them could give a complete, careful, and comprehensive explanation of the binary search algorithm together with a correct implementation. Although some candidates were able to write the correct algorithm, follow-up questions revealed that they had not fully thought through the boundary cases; they had simply happened to get it right. This made me sigh: every programmer should know some mathematical induction.

The problem is described as follows: given a monotonically nondecreasing array, perform a binary search in it to find the position of the first element greater than or equal to a given number (std::lower_bound). This constraint is fairly broad. For example, it does not restrict the number of comparisons in each recursive step, does not require using only less-than-or-equal-to operators, does not consider what to return when the element is not found (when the target position overflows the right boundary), and so on.

For convenience in the discussion that follows, I will explain the meaning of some notation here:

The given target element is denoted as t.
The given array is denoted as arr, and its length is n.
arr[k] is the value at position k in the array.
The contiguous subinterval \([b, e)\) of the array contains the values arr[b], arr[b + 1], …, arr[e - 1]. The position of its middle element is \(m = b + \lfloor (e - b) / 2 \rfloor\).

The method of binary search is to examine the magnitude relationship between the middle element of the target interval and the target element, use that as the basis for dividing the target interval into two parts, and then continue the same steps in one of those parts until the target interval is small enough that the position of the element being searched for can be determined simply. Then use this simple method to determine the final position of the desired element.

Generally speaking, candidates consider three cases:

arr[m] < t: continue searching in the right interval (excluding the middle element), \([m + 1, e)\).
arr[m] = t: continue searching in the left interval (including the middle element), \([b, m + 1)\).
arr[m] > t: continue searching in the left interval (including the middle element), \([b, m + 1)\). The reason for including the middle element is that the given array may contain no element equal to the target element.

If these three cases are considered without any gaps, they can guarantee that the element being searched for is always in the new interval. Denote this property as Safety Property 1.

Most candidates can do this step correctly. However, every candidate I have seen failed to consider one thing: is the new interval smaller than the original interval? In fact, we need to guarantee that the new search interval is always smaller than the original search interval, so that the algorithm can keep making progress. Denote this property as Liveness Property 1.

Together, Safety Property 1 and Liveness Property 1 correspond to the induction step in mathematical induction.

Let \(e = m + 1\). Solving this gives \(e = b + 1\) or \(e = b + 2\), which means the search interval has 1 element or 2 elements. Obviously, \(b = m + 1\) can never hold. Only from this can we determine that when the search interval shrinks to an empty interval or contains only no more than 2 elements, special handling is required. By special handling, I mean handling cases that violate Liveness Property 1. At this point, simply check the elements in the interval one by one. If the element being searched for does not exist, returning either -1 or e is a reasonable choice. This operation guarantees that when the search interval has only 1 or 2 elements, the position of the element being searched for can be returned. Denote this property as Safety Property 2. This property corresponds to the base step in mathematical induction.

There is no need to carry out a formal proof. As long as you think according to the structure of the proof, you can have strong confidence in the program you write.