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