Java Reference
In-Depth Information
We can combine the two like this to make postcondition R :
Post R :
v not in here
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:
inv P:
v not in here
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.
Finding the minimum value
We develop a function to return the index of a minimum value in an array seg-
/** = 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