Java Reference

In-Depth Information

is
P
true before and after the loop. It is
more general
than
Q
and
R
. Thus, in devel-

oping the invariant, we seek to generalize either
Q
or
R
.

{
Q
}

{
invariant:
P
}

{
bound function:
t
}

while
(B)

{
P && B
}
S
{
P
}

{
P && !B
}

{
R
}

Usually, but not always, generalizing
R
is most useful. Here are some ways to

generalize
R
.

Generalize R by replacing an expression by a fresh variable

We used this technique when writing a loop to process a range
m..n-1
of

integers, where it is assumed that
m
and
n
should not be changed. Suppose the

postcondition is:

R
: integers
m..n-1
have been processed

Then we replace
n
by a fresh variable
k
and get the invariant:

P
: integers
m..k-1
have been processed

The loop will start with
k=m
, since initially no integers have been processed, and

terminate with
k=n
. It usually helps (or is even formally necessary, usually to

prove termination) to place the conjunct
m≤k≤n
in the invariant:

P
:
m≤k≤n
and integers
m..k-1
have been processed

If we want to process the integers from highest to lowest, we replace
m
(instead

of
n
) by a fresh variable and use the invariant:

P
:
m≤k≤n
and integers
h..n-1
have been processed

This is the basis for all loops that process each integer in some range
m..n-1
,

including array algorithms like linear search, selection sort, and insertion sort.

Sometimes, we can determine what variable to use by attempting to initial-

ize variables so that the postcondition is true. An example is in binary search.

Initially, array segment
b[h..k]
is in ascending order, and we want to store an

integer in variable
i
so that:

R: b[h..i] ≤ x < b[i+1..k]

Setting
i
to
h-1
truthifies
b[h..i] ≤ x
; setting
i
to
k
truthifies
x < b[i+1..k]
.

We cannot do both at the same time, so we break the dependence of the formula

x < b[i+1..k]
on
i
by replacing expression
i+1
by a fresh variable
j
and end

up with this loop invariant:

Search WWH ::

Custom Search