Communications of the ACM
Getting a Program Right (2)
This is the second article about a seemingly naïve question: how do we write a binary search program? More accurately, how do we write a binary search program that is right?
If you have not read the first article, please do so first (you can find it here.), as this one really does not make much sense otherwise.
We are looking for an element x in a sorted array t. The first candidate program attempt was:
-- Program attempt #1.
from
i := 1 ; j := n -- Result initialized to 0.
until i = j loop
m := (i + j) // 2 -- Integer division
if t [m] ≤ x then i := m else j := m end
end
if x = t [i] then Result := i end
And the question was: is it correct? If so it should yield the correct answer. (An answer is correct if either Result is the index in t of an element equal to x, or Result = 0 and x does not appear in t.)
This program is not correct. To prove that it is not correct it suffices of a single example (test case) for which the program does not "yield the correct answer". Assume x = 1 and the array t has two elements both equal to zero (n = 2, remember that arrays are indexed from 1):
t = [0 0]
The successive values of the variables and expressions are:
m i j i + j + 1
After initialization: 1 2 3
i ≠ j, so enter loop: 1 1 2 6 -- First branch of "if" since t [1] ≤ x
-- so i gets assigned the value of m
But then neither of the values of i and j has changed, so the loop will repeat its body identically (taking the first branch) forever. It is not even that the program yields an incorrect answer: it does not yield an answer at all!
Note (in reference to the famous Dijkstra quote mentioned in the first article), that while it is common to pit tests against proofs, a test can actually be a proof: a test that fails is a proof that the program is incorrect. As valid as the most complex mathematical proof. It may not be the kind of proof we like most (our customers tend to prefer a guarantee that the program is correct), but it is a proof all right.
We are now ready for the second attempt:
-- Program attempt #2.
from
i := 1 ; j := n
until i = j or Result > 0 loop
m := (i + j) // 2 -- Integer division
if t [m] ≤ x then
i := m + 1
elseif t [m] = x then
Result := m
else -- In this case t [m] > x
j := m - 1
end
end
Unlike the previous one this version always changes i or j, so we may hope it does not loop forever. It has a nice symmetry between i and j.
Same question as before: does this program meet its goal?
Answer on Monday.
Post-publication note: the announced third ("Monday") article was published here.
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