Apply Loop Invariant in Binary Search

When reading the book “Accelerated C++” years ago, I was impressed by the effectiveness of loop invariant in ensuring bug-free of many functions implemented in the book. That reading opens me another door to formulate and solve some of the error-prone programming problems. The idea of loop invariant is a very simple, and it exists in each for or while loop we wrote. But many programmers may underestimate its power in solving complex problems. Recently, I discovered a series of blog posts in Dr.Dobb’s by the author of the book “Accelerated C++”, Andrew Koenig. Among these posts, I especially interested in his article series discussing how to use loop invariant to derive a concise binary search routine, proof its correctness, and test the binary search program. This post is to summarize the core ideas of Andrew’s binary search articles.

Part 1 A simple example

Binary search 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.

Two assertions:

array index begin, mid, end is always valid.
[begin, end) is always be a valid range.

First version binary search

 1while (begin != end) {
 2    auto mid = (begin + end) / 2;
 3    if (array[mid] == x)
 4        return ture;
 5
 6    if (array[mid] < x)
 7        start = mid + 1;
 8    else // array[mid] > x
 9        end = mid;
10
11    return false;
12}

Part 2 Refining The Specifications

Ordering of the array

C++ allows user to supply the comparison function.
the sequence being searched must not be out of order.

Goal to achieve

Given a sequence A[0, ..., n - 1] ordered according <, and a target value x.

If any element in A equal to x, it return the smallest index of such an element.

If no element in A equal to x, it return the smallest index j to the element greater than x.

NB: “has no value equal to x” indicates x < A[i] and A[i] < x are both false.

Possible return value of this specification

return an index of an element in A, the index points to an element that equal to x, or points to an element that greater than x. We can also express it as “the index points to a element that no less than x”. This is the definitioni from C++ STL lower_bound API.
return a non index, must be one pass the end. In this case, every element must be < x.

Part 3 Improving Our Abstractions

A = [3, 6, 7, 11, 12, 12, 12, 15, 17, 18, 23], A.length() = 11. If the sequence have n elements, there are n + 1 possible search results. The result is in the range [0, n].

Ordering abstraction

vless(x, k) is true if

k is the position of an element of the sequence that is not (strictly) less than x, or
k is equal to n (i.e., k is the off-the-end position). Otherwsie, vless(x, k) is false.

Binary search problem reduced as

With the function vless(x, k), k in the range [0, n]. vless(x, n) is true.
All of the false results of vless(x, k) come before all of the true results.
Find the lowest value of k such that vless(x, k) is true.

For example:

1        k, i =  0  1  2   3   4   5   6   7   8   9  10  n = 11
2           A = [3, 6, 7, 11, 12, 12, 12, 15, 17, 18, 23]
3 vless(0, k) = [T  T  T   T   T   T   T   T   T   T   T  T]
4vless(12, k) = [F  F  F   F   T   T   T   T   T   T   T  T]
5vless(24, k) = [F  F  F   F   F   F   F   F   F   F   F  T]

Part 4 Using The Improved Abstractions

Second version binary search

With the help of function vless(x, k)

 1size_t binary_search(T x, const T& array, size_t n)
 2{
 3    size_t begin = 0, end = n;
 4    while (begin != end) {
 5        size_t mid = (begin + end) / 2
 6        if (vless(x, mid)) { // true if mid == n, or x <= array[mid]
 7            end = mid;
 8        } else {
 9            begin = mid + 1;
10        }
11    }
12
13    return begin;
14}

Part 5 Getting Down to Details

We can replace the function call vless(x, mid) in above code with the following condition, if (mid == n || !(array[mid] < x)), the reason we prefer using < instead of <= is that we set out to define a binary search algorithm that is implemented entirely in terms of < operation. Because mid can never equal n, we change the condition to if (x < array[mid]) and switch the if and else statements.

 1size_t binary_search(T x, const T& array, size_t n)
 2{
 3    size_t begin = 0, end = n;
 4    while (begin != end) {
 5        size_t mid = (begin + end) / 2
 6        if (array[mid] < x) { // true if mid == n, or x <= array[mid]
 7            begin = mid + 1;
 8        } else {
 9            end = mid;
10        }
11    }
12
13    return begin;
14}

Part 6 How On Earth Do You Test It?

Test criteria

It return the same result as a linear search;
It accesses only legitimate array elements; and
It approximately bisects the available elements each time through the inner loop.

Linear search

We can write the linear_search function that behaves the same as the binary_search with the vless(x, k) function.

1size_t linear_search(T x, const T& array, size_t n)
2{
3    size_t k = 0;
4    while (!vless(x, k))
5        ++k;
6
7    return k;
8}

Transform the while loop from while (!vless(x, k)) to while (!(k == n) || !(array[k] < x)) to while (k != n && array[k] < x)

1size_t linear_search(T x, const T& array, size_t n)
2{
3    size_t k = 0;
4    while (k != n && array[k] < x)
5        ++k;
6
7    return k;
8}

Part 7 Choosing Test Cases

Test criteria

Binary search expects the input sequence is ordered, but doesn’t verify the ordering. Verifying the ordering takes O(n).
The order relation itself must be well behaved.
Not good enough to return correct results. It must not execute any undefined operations.
The binary search algorithm must run in O(logn).

Performance bugs are bugs.

Observation

The actual value of the array elements don’t matter! All that matters is the relative ordering of the array elements. After all, the only time we ever look at an element is in the condition of a single if statement: if (array[mid] < x).
In other words: If the array has one or more elements, the first element could have any value at all. Each subsequent element is either greater than its predecessor or equal to it; no element can ever be less than its predecessor.
For array of length n. we can construct a list of 2^{n-1} distinct arrays that is exhaustive for testing purposes.

Relevant values to test

Any value less than the first element of the array
Any value greater than the last element of the array
A value equal to each of the array elements
A value between any two adjacent array elements

Above observations suggest that we can construct test cases by using odd integers and searching for all integers, even and odd, starting with zero and ending one past the last element, inclusive.

Example test cases

Use x = 0, 1, 2, 3, and 4 to test.

Part 8 What Does It Mean To Say “It Works?”

Test cases

Suppose the input array have length of k, and n distinct elements. We should be able to check this array by searching only for values of x in the range [0, 2n]. For example, array = [1, 3], we can test it by searching for 0, 1, 2, 3, and 4, and no other values.

This loop can facilitate our test.

1# define NDEBUG 0
2for (unsigned x = 0; x <= 2 * n; ++x)
3  assert(binary_search(x, array, k) == linear_search(x, array, k));

We can add some more sanity checks:

Result must be in the range [0, k], k is the number of element in the array.
If the result r refers to an element that is not the first element. Then array[r - 1] < x must hold.

1for (unsigned x = 0; x <= 2 * n; ++x) {
2    auto r = binary_search(x, array, k);
3    assert(r >= 0 && r <= k);
4    if (r != k) {
5        assert(!(x < array[r]));
6        if (r > 0) assert(array[r - 1] < x);
7    }
8    assert(r == linear_search(x, array, k));
9}

Part 9 What Do We Need to Test?

Some claims about test

Verifying that a program’s output is correct is not enough to test it thoroughly.
Example: to test expresion i + j + k, where i, j, and k all have type int.
1. different overflow behaviors,
2. different C++ implementations,
3. different platforms.
Array indices out of bounds can be even a more serious problem: It is entirely possible for a program to appear to produce correct results, but to have a side effect of disrupting memory used by an unrelated program.
Test the invariant in the loop: mid is in the range [begin, end). and array indexes are valid.

 1size_t binary_search(T x, const T& array, size_t n)
 2{
 3    size_t begin = 0, end = n;
 4    while (begin != end) {
 5        assert(begin < end && begin < n && end <= n);
 6        size_t mid = begin + (end - begin) / 2
 7        assert(begin <= mid && mid < end);
 8        if (array[mid] < x) {
 9            begin = mid + 1;
10        } else {
11            end = mid;
12        }
13    }
14
15    return begin;
16}

Part 10 Putting It All Together

Using the strategy discussed in Part 7 to generating test cases. To generate the test arrays with length of n, we leverage the bit mask trick. Basically, each element of $[0, 1, ..., 2^{n-1} - 1]$ corresponds to a test case. The bit representation of the current element determine the current test case uniquely. Notice n is in the range [0, 32] if the element is 32-bit integer.

 1/* bits now equal to 2^{n-1} when n != 0*/
 2unsigned long bits = (n == 0) ? 1UL : 1UL << (n - 1);
 3
 4/* The outer loop enumerate the bit representation of such a case */
 5do {
 6    --bits;
 7    unsigned i = 1;
 8    for (unsigned j = 0; j != n; ++j) {
 9        array[j] = i;
10        if (bits & (1UL << j))
11            i += 2;
12    }
13
14    for (unsigned x = 0; x <= i + 1; ++x) {
15        assert(binary_search(x, array, n) == linear_search(x, array, n));
16    }
17} while (bits != 0);

The do while loop could be written using for loop:

 1for (bits--; bits >= 0; --bits) {
 2    unsigned i = 1;
 3    for (unsigned j = 0; j != n; ++j) {
 4        array[j] = i;
 5        if (bits & (1UL << j))
 6            i += 2;
 7    }
 8
 9    for (unsigned x = 0; x <= i + 1; ++x) {
10        assert(binary_search(x, array, n) == linear_search(x, array, n));
11    }
12}