Java Reference

In-Depth Information

We can combine the two like this to make postcondition
R
:

Post
R
:

h

i

k

v
not in here

b

and (
i=k
or
b[i] = v)

To find the loop invariant, we investigate postcondition
R.
It is easy to ini-

tialize
i
so that
b[h..i-1]
does not contain
v
: just set
i
to
h
, since then

b[h..i-1]
is empty and
v
is not in it. And, like the schema you have seen, that

array segment can grow. The second part of
R
, “either
i=k
or
b[i] = v
”, is real-

ly what we are trying to accomplish and may not be true with
i=h
. So, we take

just the first part of
R
as the invariant:

h

i

k

inv
P:

v
not in here

b

How does it start?
As discussed in the previous paragraph, we set
i
to
h.

When is the loop done?
When we have the piece of the postcondition that

we eliminated: when either
i=k
or
b[i] = v
. So the loop must continue as long

as this condition is false. Using De Morgan's law:

not
(A || B) = (
not
A&&
not
B)

we see that the loop condition can be written in Java as:
i != k && b[i] != v
.

How does the repetend make progress?
Increment
i
.

How does the repetend keep the invariant true?
We get lucky: from the loop

condition, we see that the increment happens only when
b[i] != v
, so no other

work needs to be done.

See Fig. 8.5 for the complete method.

8.5.2

Finding the minimum value

We develop a function to return the index of a minimum value in an array seg-

ment:

Activity

8-5.3

/** =
index of first occurrence of
v
in
b[h..k - 1]
(=
k
if
v
is not in
b[h..k - 1]
)
*/

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

int
i= h;

//
inv
P: h ≤ i ≤ k
and
v
is not in
b[h..i - 1]}

while
(i != k && v != b[i])

{ i= i + 1; }

return
i;

}

Figure 8.5:

Function
linearSearch

Search WWH ::

Custom Search