Dr. Dobb's is part of the Informa Tech Division of Informa PLC

This site is operated by a business or businesses owned by Informa PLC and all copyright resides with them. Informa PLC's registered office is 5 Howick Place, London SW1P 1WG. Registered in England and Wales. Number 8860726.

Channels ▼

Andrew Koenig

Dr. Dobb's Bloggers

Invariants For Binary Search, Part 1: A Simple Example

October 16, 2014

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:

  1. 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.
  2. 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 takemid 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.

Related Reading

More Insights

Currently we allow the following HTML tags in comments:

Single tags

These tags can be used alone and don't need an ending tag.

<br> Defines a single line break

<hr> Defines a horizontal line

Matching tags

These require an ending tag - e.g. <i>italic text</i>

<a> Defines an anchor

<b> Defines bold text

<big> Defines big text

<blockquote> Defines a long quotation

<caption> Defines a table caption

<cite> Defines a citation

<code> Defines computer code text

<em> Defines emphasized text

<fieldset> Defines a border around elements in a form

<h1> This is heading 1

<h2> This is heading 2

<h3> This is heading 3

<h4> This is heading 4

<h5> This is heading 5

<h6> This is heading 6

<i> Defines italic text

<p> Defines a paragraph

<pre> Defines preformatted text

<q> Defines a short quotation

<samp> Defines sample computer code text

<small> Defines small text

<span> Defines a section in a document

<s> Defines strikethrough text

<strike> Defines strikethrough text

<strong> Defines strong text

<sub> Defines subscripted text

<sup> Defines superscripted text

<u> Defines underlined text

Dr. Dobb's encourages readers to engage in spirited, healthy debate, including taking us to task. However, Dr. Dobb's moderates all comments posted to our site, and reserves the right to modify or remove any content that it determines to be derogatory, offensive, inflammatory, vulgar, irrelevant/off-topic, racist or obvious marketing or spam. Dr. Dobb's further reserves the right to disable the profile of any commenter participating in said activities.

Disqus Tips To upload an avatar photo, first complete your Disqus profile. | View the list of supported HTML tags you can use to style comments. | Please read our commenting policy.