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