132
Proofs, Induction, and Number Theory
Between the time j and i have the values j k and i k and the time they have the values
j k+1 and i k+1 , one iteration of the loop takes place. In that iteration, j is changed by
adding y to the previous value, and i is changed by adding 1. Thus,
j k+1 = j k + y
(3)
i k+1 = i k + 1
(4)
Then
j k+1 = j k + y
(by (3))
= i k * y + y (by the inductive hypothesis)
= (i k + 1)y
= i k+1 * y
(by (4))
We have proved that Q is a loop invariant.
The loop rule of inference allows us to infer that after the loop statement is
exited, the condition Q ` B′ holds, which in this case becomes
j = i * y ` i = x
Therefore at this point the statement
j = x * y
is true, which is exactly what the function is intended to compute.
Example 26 illustrates that loop invariants say something stronger about the
program than we actually want to show; what we want to show is the special case
of the loop invariant on termination of the loop. Finding the appropriate loop invariant requires working backward from the desired conclusion, as in Example 25.
We did not, in fact, prove that the loop in this example actually does terminate. What we proved was partial correctness—the program produces the
correct answer, given that execution does terminate. Because x is a nonnegative
integer and i is an integer that starts at 0 and is then incremented by 1 at each pass
through the loop, we know that eventually i = x will become true.
PrACTiCe 10 Show that the following function returns the value x + y for nonnegative integers x and y
by proving the loop invariant Q: j = x + i and evaluating Q when the loop terminates.
Sum (nonnegative integer x; nonnegative integer y)
Local variables:
integers i, j
i = 0
j = x
while i ≠ y do
j = j + 1
i = i + 1
end while
// j now has the value x + y
return j
end function Sum
■
Proofs, Induction, and Number Theory
Between the time j and i have the values j k and i k and the time they have the values
j k+1 and i k+1 , one iteration of the loop takes place. In that iteration, j is changed by
adding y to the previous value, and i is changed by adding 1. Thus,
j k+1 = j k + y
(3)
i k+1 = i k + 1
(4)
Then
j k+1 = j k + y
(by (3))
= i k * y + y (by the inductive hypothesis)
= (i k + 1)y
= i k+1 * y
(by (4))
We have proved that Q is a loop invariant.
The loop rule of inference allows us to infer that after the loop statement is
exited, the condition Q ` B′ holds, which in this case becomes
j = i * y ` i = x
Therefore at this point the statement
j = x * y
is true, which is exactly what the function is intended to compute.
Example 26 illustrates that loop invariants say something stronger about the
program than we actually want to show; what we want to show is the special case
of the loop invariant on termination of the loop. Finding the appropriate loop invariant requires working backward from the desired conclusion, as in Example 25.
We did not, in fact, prove that the loop in this example actually does terminate. What we proved was partial correctness—the program produces the
correct answer, given that execution does terminate. Because x is a nonnegative
integer and i is an integer that starts at 0 and is then incremented by 1 at each pass
through the loop, we know that eventually i = x will become true.
PrACTiCe 10 Show that the following function returns the value x + y for nonnegative integers x and y
by proving the loop invariant Q: j = x + i and evaluating Q when the loop terminates.
Sum (nonnegative integer x; nonnegative integer y)
Local variables:
integers i, j
i = 0
j = x
while i ≠ y do
j = j + 1
i = i + 1
end while
// j now has the value x + y
return j
end function Sum
■