acm-header
Sign In

Communications of the ACM

BLOG@CACM

Getting a Program Right (4, Also Includes 3')


View as: Print Mobile App Share:
Bertrand Meyer

This is the fourth article about a seemingly naïve question: how do we write a binary search program? The first article appeared here.

The first two program attempts were wrong. The third article introduced a new variant reading as follows:

 --  Program attempt #3.

from

i := 1 ; j := n

until i = j loop

m := (i + j + 1) // 2

if t [m] ≤ x then

i := m  + 1

else

j := m

end

end

if ≤ i  and i n then Result := i end
     
       -- If not, Result remains 0.

The question was: is it right?

I know, you have every right to be upset at me, but the answer here too is no.

Consider a two-element array t = [0 0] (so n = 2, remember that our arrays are indexed from 1 by convention) and a search value x = 1. The successive values of the variables and expressions are:

                                                m          i          j            i + j + 1

After initialization:                            1        2           4

i ≠ j, so enter loop:               2           3        2          6                  -- First branch of "if" since t [2] < x

i ≠ j,  enter loop again:        3                                                 -- Out-of-bounds memory access!
                                                                                                        -- (trying to access non-existent t [3])

 

Oops!

Note that we could hope to get rid of the array overflow by initializing i to 0 rather than 1. This variant (version #3') is left as a bonus question to the patient reader. (Hint: it is also not correct. Find a counter-example.)

OK, this has to end at some point. What about the following version (#4): is it right?

 --  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

 Answer on Friday.

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

Sign In for Full Access
» Forgot Password? » Create an ACM Web Account