Font Arena

Pin the slots you have settled, then choose the one to fight for and the faces that fight. A slot left unpinned stays on the browser’s generic family.

  • Title
    The article title
  • Lead
    The intro paragraph
  • Headings
    Section headings
  • Body text
    Paragraphs and lists
  • Accents
    Links and bold
  • Code
    Inline code and the code block
Slot under test

Choose the slot to fight for. The other five stay as they are pinned.

Export

The stack on screen, to paste into a project.

The binary search bug that outlived its proof

Jon Bentley published a binary search in 1986 together with an argument for why it could not fail. The argument was sound. The code was broken anyway — not in the logic, which held, but in the one assumption the logic never mentioned.

That this is a hard routine to write was Bentley’s own finding. Given two hours and a language of their choosing, only about ten percent of the professional programmers he taught produced a correct one — for a routine whose idea fits in a sentence: halve the interval until the target is cornered.

The idea is easy and the boundaries are not. Three things have to agree at once:

  • the bounds — whether the window is closed at both ends or half-open — held to the same convention in every branch;
  • the termination test, which decides whether a window of one element is examined or stepped over;
  • the midpoint, whose rounding decides which half a tie falls into, and whether the window is guaranteed to shrink at all.

Get one of the three wrong and the loop still answers correctly for almost every input you would think to try. It fails on the empty array, or on the last element, or not at all until the array is far larger than the ones you tested with.

A proof, and the libraries that trusted it

So Bentley did the responsible thing. The version in Programming Pearls is derived from the loop invariant and carries an argument that the loop terminates and cannot miss an element that is present. The argument is correct. It is also the version behind java.util.Arrays.binarySearch: Joshua Bloch, who wrote the JDK’s, has said he worked from the book — and inherited its flaw, which then sat in the standard library for some nine years, running on every machine that ran Java.

Where the machine disagrees with the arithmetic

The line at fault computes the midpoint of the window: int mid = (low + high) / 2; Over the integers, that is the midpoint, unconditionally. Over int it is the midpoint only while the sum stays under 2,147,483,647. Hand the routine an array of 1,073,741,824 elements or more — a size that was science fiction in 1986 and is an afternoon’s allocation now — and low + high wraps to a negative number, the division carries the sign down with it, and the search indexes the array at a negative offset. Java throws; C reads whatever happens to be there.

In 2006 Bloch published a post under the headline “Nearly All Binary Searches and Mergesorts are Broken”. The cause is an integer overflow in a single line, and the fix for it is three characters wide:

// Bloch's fix: a midpoint that cannot overflow.
static int binarySearch(int[] a, int key) {
    int low = 0, high = a.length - 1;

    while (low <= high) {
        int mid = (low + high) >>> 1;   // not (low + high) / 2
        int midVal = a[mid];

        if (midVal < key) low = mid + 1;
        else if (midVal > key) high = mid - 1;
        else return mid;
    }
    return -(low + 1);   // where it would have been
}

>>> is the unsigned right shift: it moves every bit down one place and feeds a zero into the vacated top bit, so the wrapped sum is read back as the large positive number it really is rather than as a negative one. The sum still overflows. The midpoint no longer does.

The assumption nobody wrote down

The proof was never wrong. It was a proof about the integers, and the code was running on int, which is not the integers but a fixed-width approximation that agrees with them right up until it doesn’t. The gap was not in the code, the tests or the argument. It was in a sentence nobody thought to write: assume the sum of two valid indices is itself representable.

That assumption held for twenty years because for twenty years it was true — no machine within reach had a billion-element array in it. Nothing about the code changed. The world underneath it did, and a defect that had been there since the first printing finally had room to happen.

The moral is not that proofs are worthless. It is that a proof holds over the model it was written against, and the machine is not that model — so the boundaries worth testing are precisely the ones the argument quietly rules out.