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