Java Reference
In-Depth Information
How does it keep the invariant true?
If the new value at
b[i]
is smaller than
m
, store
m
in
i
.
See Fig. 8.6 for the complete method. The loop could have been developed
by refining a suitable loop schema. Try this yourself!
8.5.3
Binary search
The linear search algorithm of Sec. 8.4.1 may have to look at all the elements of
the array segment that it is searching. If the array segment is in ascending order,
far fewer elements may have to be looked at because the search can stop as soon
as an element larger than
v
is detected. So, we now investigate an algorithm to
search a sorted array.
We develop an algorithm to satisfy this specification:
Activity
8-5.8
/** =
index
i
such that
R: b[h..i] ≤ v < b[i+1..k]
Precondition:
b[h..k]
is in non-descending order
*/
public static int
binarySearch(
int
[] b,
int
h,
int
k,
int
v)
We determine what
R
means, using the fact that
b
is in ascending order. If
v
occurs in
b
, the postcondition indicates that the index of the rightmost occurrence
of
v
is to be calculated. For example, if
v
is
6
, the index of the rightmost
6
is to
be calculated.
Second, if
v
is not in
b
, for example,
v=3
, then the index of the position
after which
v
could be inserted should be calculated. As another example of this,
if
v
is less than the first element, the value
h-1
should be returned because
b[h..h-1] < v < b[h..k]
.
How will this function be used?
Examples when
d={1
,
3
,
3
,
5
,
7
,
8}
:
call
result
binarySearch(d
,
0
,
2
,
3)
2
binarySearch(d
,
0
,
2
,
4)
2
binarySearch(d
,
4
,
6
,
8)
5
binarySearch(d
,
4
,
6
,
2)
4
binarySearch(d
,
4
,
4
,
2)
4
The heart of this function is a loop to find the index
i
of
v
, which we now
develop. To find the loop invariant, note that it is easy to truthify the first part of
postcondition
R
by setting
i
to
h-1
, and it is easy to truthify the second part of
assertion
R
by setting
i
to
k
. But, obviously, we cannot do both! We break this
dependence of both parts on
i
by replacing expression
i+1
by a fresh variable
j
, giving us the invariant:
P: b[h..i] ≤ v < b[j..k]
If it helps, write the invariant as a diagram:
Search WWH ::
Custom Search