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