Java Reference

In-Depth Information

h i j k

≤ v > v

P
is then initially truthified by assigning
h-1
to
i
and
k+1
to
j
. Then,

b[h..h-1]
and
b[k+1..k]
are empty segments.

The loop can terminate with
R
true only if
j=i+1
. Therefore, it should con-

tinue as long as
j
and
i+1
are different. And, we can now place some obvious

bounds on
i
and
j
in the invariant:

P: -1≤i<j≤k+1
and
b[h..i] ≤ v < b[j..k]

The repetend has to make progress by incrementing
i
or decrementing
j
. To

that end, let
e
be the average of
i
and
j
. Because
i<j+1
,
e
lies strictly between

i
and
j
. This means that setting either
j
or
i
to
e
will keep the second part of

invariant
P
true.

There are now two cases to consider:
b[e] < v
and
v < b[e]
. In the first case,

setting
i
to
e
keeps
P
true because
b[h..e] < v
. In the second case, setting
j
to

e
keeps
P
true because
v < b[e..k]
. This ends the development of the repetend

and thus of the loop. The complete function is in Fig. 8.7.

Discussion

For an array segment of size
2
n
for some
n≥0
, this binary search function

always makes
n+1
iterations, looking at n+1 array elements, no matter what the

contents of the array. For example, if the array size is
2
15
= 32768
, it will look

at only
16
elements!

It may seem that stopping as soon as the value
v
is found would make the

algorithm faster. However, this requires a second test in the body of the loop —

one has to test for
v < b[i]
and
v = b[i]
— so the loop body is less efficient.

/** =
the value
i
that satisfies
R: b[h..i] ≤ v < b[i+1..k]

Precondition:
b[h..k]
is sorted.
*/

public static int
binarySearch(
int
[] b,
int
h,
int
k,
int
v) {

int
i= h - 1;

int
j= k + 1;

//
inv
P: h-1≤i<j≤k+1 and b[h..i] ≤ v < b[j..k]

while
(j != i + 1) {

int
e= (i + j) / 2;

// { h-1≤i<e<j≤k+1 }

if
(b[e] <= v) { i= e; }

else
{ j= e; }

}

return
i;

}

Figure 8.7:

Function binarySearch

Search WWH ::

Custom Search