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