Getting a Program Right (5)

Yes, I know, this is dragging on. But that’s part of the idea: showing how hard it is to get a program right if you just judging by the seat of your pants. Maybe we can get it right this time?

This is the fifth article about a seemingly naïve question: how do we write a binary search program? The first article appeared here. The first three program attempts were wrong. The fourth article dismissed one more variant and introduced yet another:

 —  Program attempt #4.

from

i := 0 ; j := n + 1

until i = j loop

m := (i + j) // 2

if t [m] ≤ x then

i := m  + 1

else

j := m

end

end

if 1  ≤  i  and i ≤ n then Result := i end

Are we there yet? Is this one finally correct?

Sorry to disappoint, but no. Consider a two-element array t = [0 0], so n = 2, and a search value x = 1 (yes, same counter-example as last time, although here we could also use x = 0). The successive values of the variables and expressions are:

                                                m          i          j            i + j

After initialization:                           0        3           3

i ≠ j, so enter loop:               1           2       3          5            — First branch of "if"

i ≠ j, enter loop again:         2         3        3         6            — First branch again

i = j, exit loop                                   

The condition of the final "if" is true, so Result gets the value 3. This is quite wrong, since there is no element at position 3, and in any case x does not appear in t.

But we are so close! Something like this should work, should it not?

So patience, patience, let us tweak it just one trifle more, OK?

 —  Program attempt #5.

from

i := 0 ; j := n

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

Does it work now? Answer on Monday. (The search for the ultimate truth in life knows no weekends, but I have to wait for the friendly staff at ACM to make sure each article is properly registered and linked.)

 Post-publication note: the  announced sixth ("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).