# Invariants For Binary Search, Part 1: A Simple Example

Once upon a time, when I was still in college, I had dinner at a restaurant with some people, one of whom specialized in sorting algorithms. He told me that when he taught introductory computer-science courses, he would often describe the binary-search algorithm to his students and then ask them to implement it. His experience was that essentially no one could do so correctly.

I took him up on the challenge, and discovered two things: First, I did not know how to solve the problem in a way that made me confident that he would not find an embarrassing flaw in my solution. Second — and fortunately — my fountain pen made such a mess of the restaurant's cocktail napkins that I could use that fact as an excuse to avoid solving it.

Now, decades later, I would like to revisit the problem in the light of the previous few weeks' comments about invariants.

We shall begin by describing the problem. There is an array, which we'll call `a`

. We care about the elements in the range `[begin, end)`

. In other words, the first element is `a[begin]`

and the last element is `a[end-1]`

; if there are no elements at all, `begin`

and `end`

are equal. Because array indices in C and C++ are unsigned, we shall assume that `begin`

and `end`

are unsigned.

The elements of `a`

are in increasing order, allowing for the possibility that some pairs of adjacent elements might be equal. We can restate this claim by saying that if `i`

and `j`

are indices of `a`

and `i<j`

, then `a[i]<=a[j]`

.

Given these constraints, the simplest form of binary search is one that determines whether `a`

contains an element equal to a given value `x`

. We can make the problem slightly richer by asking for the index of an element with value `x`

if one exists, and richer still by asking the code to tell us where the value `x`

would be placed in the array if it is not there. For now, we shall consider the simplest form: Our input is a value; our output is either yes or no depending on whether `x`

appears in `a`

.

Expressed in this way, this problem is similar to the one solved by the standard-library `binary_searc`

algorithm. The main difference is that instead of accepting an array and two indices, `binary_search`

accepts two random-access iterators. There are some subtle points about iterator arithmetic that we would like to discuss later; so for now we shall think in terms of integers and array indices. Continuing our simplification, we shall not try to write a complete C++ function; instead, we shall assume that the variables `begin`

, `end`

, and `x`

have already been set up for us.

Binary search works by using a pair of values to define a range. Roughly speaking, we pick a new index that is midway between the two indices we have, we compare `x`

with the element denoted by that index, and we use the result of that comparison to adjust the indices in a way that rules out approximately half of our range as a possible location to search for `x`

. We repeat this process, each time reducing the range by half, until either we find `x`

or we are confident that it is not there. This description suggests an invariant:

*If any element in the original range *`[begin, end)`

* is equal to *`x`

*,
then an element in the current range *`[begin, end)`

* is equal to *`x`

.

In other words, each time through the loop, we intend to bring `begin`

and `end`

closer together while ensuring that doing so does not exclude all of the elements that are equal to `x`

. If we get to the point where the range `[begin, end)`

is empty, we know that we are not going to be able to find `x`

; otherwise, we will have found it along the way.

We have to ensure two other conditions as well:

- Every time we attempt to access an array element, we must ensure that the element actually exists. We shall verify this condition whenever we compute an array index.
- We must never allow
`begin`

to become greater than`end`

, in order to ensure that`[begin, end)`

is always a valid range. Because of this requirement we shall use`begin != end`

as our loop condition, even though`begin < end`

might seem more natural.

With these preliminaries, we can imagine a loop that looks like this:

while (begin != end) { // Increase begin or decrease end while maintaining the invariant } // If we get here, x is not in the original array

This is a funny kind of loop, at least so far, because it does not tell us what happens if we *do* find an element that is equal to `x`

. In a way, we're doing two things at once: We're looking for `x`

, and at the same time, we're trying to maintain a loop invariant. If we find `x`

, we no longer care about the invariant. So we might imagine our code as a function body and add a little to it:

while (begin != end) { if (some kind of test involving x, begin, and end) return true; // we found x // Increase begin or decrease end while maintaining the invariant } return false; // If we get here, x is not in the original array

What is this test we're talking about? Remember the description of binary search: We compute an index that is approximately in the middle of our range and inspect the element there. Let's do so:

auto mid = (begin + end)/2;

Here, `begin`

, `end`

, and `mid`

are integers; we need to prove that `mid`

is in the range [begin, end). If we were dealing with real numbers, it would be obvious that `begin < mid < end`

. However, we must show that rounding will never take`mid`

outside of the range.

To do so, consider two cases: `(begin + end)`

is even or odd. If it is even, the division is exact, so the behavior is the same as it would be if `begin`

and `end`

were real numbers. If `(begin + end)`

is odd, then `mid`

must be `(begin + end) - 0.5`

. Because `end > begin, (begin + end) > (begin + begin)`

and therefore `(begin + end) >= (begin + begin + 1)`

. Therefore, before rounding `(begin + end) / 2 >= (begin + 0.5)`

, so `mid >= begin`

. A similar argument shows that `mid < end`

, and therefore that `mid`

is always the index of an element, provided that `begin < end`

. Our loop has grown:

while (begin != end) { auto mid = (begin + end) / 2; if (array[mid] == x) return true; // Increase begin or decrease end while maintaining the invariant } return false; // If we get here, x is not in the original array

All that remains is to adjust `begin`

or `end`

based on the comparison between `array[mid]`

and `x`

. If `array[mid] < x`

, then because the array is ordered, we know that the lowest possible index for an element equal to `x`

is `mid+1`

. We knew before that if `x`

was anywhere in the original array, it must be in `[begin, end)`

; we now know that it must be in `[mid+1, end)`

. Is this a valid range? Yes, because we knew at the beginning of the loop that `mid`

is the index of an element, which means that `mid < end`

, which, in turn, means that `mid+1 <= end`

.

What about the case where `array[mid] > x`

? In that case, we know that the largest possible index for an element `x`

, if it exists, is `mid-1`

. We express this knowledge by saying that if `x`

is in the array, its index is in the range `[begin, mid)`

, because such ranges exclude their right-hand endpoints.

We can include these decisions in the code as follows:

while (begin != end) { auto mid = (begin + end) / 2; if (array[mid] == x) return true; // Increase begin or decrease end while maintaining the invariant if (array[mid] < x) begin = mid + 1; else // array[mid] > x end = mid; } return false; // If we get here, x is not in the original array

There is much more to be said about this code. For example, it's not a complete C++ function, which makes it difficult to test. Moreover, the two comparisons of `array[mid]`

and `x`

each time through the loop seem ungainly and probably unnecessary. Finally, it should be clear that this code comes close to figuring out where in the array `x`

should go if it is not already there, and it seems a shame to throw this information away.

We shall address these issues starting next week. Meanwhile, please keep in mind the point of this example: We can use an invariant to help us reason about a piece of code that many programmers find hard to get right by any other means.