Communications of the ACM
Getting a Program Right (6)
This is the sixth article about a seemingly naïve question: how do we write a binary search program? The first article appeared here. The first four program attempts were wrong. The fifth article, the latest one, introduced yet another:
-- Program attempt #5.
from
i := 1 ; j := n + 1
until i ≥ j or Result > 0 loop
m := (i + j) // 2
if t [m] < x then
i := m + 1
elseif t [m] > x then
j := m
else
Result := m
end
end
And the question was the same as before: is it right, is it wrong?
Well, I know you are growing more upset at me with each article, but the answer is still that this program is wrong. But the way it is wrong is somewhat specific; and it applies, in fact, to all previous variants as well.
This particular wrongness (fancy word for "bug") has a history. As I pointed out in the first article, there is a long tradition of using binary search to illustrate software correctness issues. A number of versions were published and proved correct, including one in the justly admired Programming Pearls series by Jon Bentley. Then in 2006 Joshua Bloch, then at Google, published a now legendary blog article [2] which showed that all these versions suffered from a major flaw: to obtain m, the approximate mid-point between i and j, they compute
(i + j) // 2
which, working on computer integers rather than mathematical integers, might overflow! This in a situation in which both i and j, and hence m as well, are well within the range of the computer's representable integers, 2-n to 2n (give or take 1) where n is typically 31 or, these days, 63, so that there is no conceptual justification for the overflow.
In the specification that I have used for this article, i starts at 1, so the problem will only arise for an array that occupies half of the memory or more, which is a rather extreme case (but still should be handled properly). In the general case, it is often useful to use arrays with arbitrary bounds (as in Eiffel), so we can have even a small array, with high indices, for which the computation will produce an overflow and bad results.
The Bloch gotcha is a stark reminder that in considering the correctness of programs we must include all relevant aspects and consider programs as they are executed on a real computer, not as we wish they were executed in an ideal model world.
(Note that Jon Bentley alluded to this requirement in his original article: while he did not explicitly mention integer overflow, he felt it necessary to complement his proof by the comment that that "As laborious as our proof of binary search was, it is still unfinished by some standards. How would you prove that the program is free of runtime errors (such as division by zero, word overflow, or array indices out of bounds)?". Prescient words!)
It is easy to correct the potential arithmetic overflow bug: instead of (i + j) // 2, Bloch suggested we compute the average as
i + (j - i) // 2
which is the same from a mathematician's viewpoint, and indeed will compute the same value if both variants compute one, but will not overflow if both i and j are within range.
So we are ready for version 6, which is the same as version 5 save for that single change:
-- Program attempt #6.
from
i := 1 ; j := n + 1
until i ≥ j or Result > 0 loop
m := i + (j - i) // 2
if t [m] < x then
i := m + 1
elseif t [m] > x then
j := m
else
Result := m
end
end
Now is probably the right time to recall the words by which Donald Knuth introduces binary search in the original 1973 tome on Sorting and Searching of his seminal book series The Art of Computer Programming:
Although the basic idea of binary search is comparatively straightforward, the details can be somewhat tricky, and many good programmers have done it wrong the first few times they tried.
Do you need more convincing? Be careful what you answer, I have more variants up my sleeve and can come up with many more almost-right-but-actually-wrong program attempts if you nudge me. But OK, even the best things have an end. This article series does not end yet, but the examples do. To the naturally following next question in this running quiz, "is version 6 right or wrong", I can provide the answer: it is, to the best of my knowledge, a correct program. Yes! [3].
But the quiz continues. Since answers to the previous questions were all that the programs were not correct, it sufficed in each case to find one case for which the program did not behave as expected. Our next question (to be answered here on Wednesday) will be of a different nature: can you find an argument why version #6 is correct?
Post-publication note: the announced sixth ("Wednesday") article was published here. I fixed the same copy-paste error as in version #5.
References
[1] (In particular) Jon Bentley: Programming Pearls -- Writing Correct Programs, in Communications of the ACM, vol. 26, no. 12, December 1983, pages 1040-1045, available here.
[2] Joshua Bloch: Extra, Extra - Read All About It: Nearly All Binary Searches and Mergesorts are Broken, blog post, on the Google AI Blog, 2 June 2006, available here.
[3] A caveat: the program is correct barring any typos or copy-paste errors -- I am starting from rigorously verified programs (see the next posts), but the blogging system's UI and text processing facilities are not the best possible for entering precise technical text such as code. However carefully I check, I cannot rule out a clerical mistake, which of course would be corrected as soon as it is identified.
Bertrand Meyer is chief technology officer of Eiffel Software (Goleta, CA), professor and provost at the Schaffhausen Institute of Technology (Switzerland), and head of the software engineering lab at Innopolis University (Russia).
No entries found