Section 2.3 More on Proof of Correctness
131
The loop rule of inference allows the truth of (2) to be inferred from an implication stating that Q is a loop invariant. Again, for Q to be a loop invariant it
must be the case that if Q is true and condition B is true, so that another loop iteration is executed, then Q remains true after that iteration, which can be expressed
by the Hoare triple {Q ` B} P {Q}. The rule is formally stated in Table 2.4.
To use this rule of inference, we must find a useful loop invariant Q—one that
asserts what we want and expect to have happen—and then prove the implication
5Q ` B6 P 5Q6
Here is where induction comes into play. We denote by Q(n) the statement that
a proposed loop invariant Q is true after n iterations of the loop. Because we do
not necessarily know how many iterations the loop may execute (that is, how long
condition B remains true), we want to show that Q(n) is true for all n ≥ 0. (The
value of n = 0 corresponds to the assertion upon entering the loop, after zero loop
iterations.)
eXAMPLe 26
Consider again the pseudocode function of Example 25. In that example, we
guessed that Q is the relation
j = i * y
To use the loop rule of inference, we must prove that Q is a loop invariant.
The quantities x and y remain unchanged throughout the function, but values
of i and j change within the loop. We let i n and j n denote the values of i and j,
respectively, after n iterations of the loop. Then Q(n) is the statement j n = i n * y.
We prove by induction that Q(n) holds for all n ≥ 0. Q(0) is the statement
j 0 = i 0 * y
which, as we noted in Example 25, is true, because after zero iterations of the loop,
when we first get to the loop statement, both i and j have been assigned the value
0. (Formally, the assignment rule could be used to prove that these conditions on i
and j hold at this point.)
Assume Q(k): j k = i k * y
Show Q(k + 1): j k+1 = i k+1 * y
tAbLe 2.4
From
can Derive
name of Rule
Restrictions on use
{Q ` B} P {Q}
{Q} s i {Q ` B′} loop
s i has the form
while condition B do
P
end while
131
The loop rule of inference allows the truth of (2) to be inferred from an implication stating that Q is a loop invariant. Again, for Q to be a loop invariant it
must be the case that if Q is true and condition B is true, so that another loop iteration is executed, then Q remains true after that iteration, which can be expressed
by the Hoare triple {Q ` B} P {Q}. The rule is formally stated in Table 2.4.
To use this rule of inference, we must find a useful loop invariant Q—one that
asserts what we want and expect to have happen—and then prove the implication
5Q ` B6 P 5Q6
Here is where induction comes into play. We denote by Q(n) the statement that
a proposed loop invariant Q is true after n iterations of the loop. Because we do
not necessarily know how many iterations the loop may execute (that is, how long
condition B remains true), we want to show that Q(n) is true for all n ≥ 0. (The
value of n = 0 corresponds to the assertion upon entering the loop, after zero loop
iterations.)
eXAMPLe 26
Consider again the pseudocode function of Example 25. In that example, we
guessed that Q is the relation
j = i * y
To use the loop rule of inference, we must prove that Q is a loop invariant.
The quantities x and y remain unchanged throughout the function, but values
of i and j change within the loop. We let i n and j n denote the values of i and j,
respectively, after n iterations of the loop. Then Q(n) is the statement j n = i n * y.
We prove by induction that Q(n) holds for all n ≥ 0. Q(0) is the statement
j 0 = i 0 * y
which, as we noted in Example 25, is true, because after zero iterations of the loop,
when we first get to the loop statement, both i and j have been assigned the value
0. (Formally, the assignment rule could be used to prove that these conditions on i
and j hold at this point.)
Assume Q(k): j k = i k * y
Show Q(k + 1): j k+1 = i k+1 * y
tAbLe 2.4
From
can Derive
name of Rule
Restrictions on use
{Q ` B} P {Q}
{Q} s i {Q ` B′} loop
s i has the form
while condition B do
P
end while