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