130
Proofs, Induction, and Number Theory
Assertion Q must be true before the loop is entered. If implication (2) is to
hold, Q must remain true after the loop terminates. Because it may not be known
exactly when the loop will terminate, Q must remain true after each iteration
through the loop, which will include the final iteration. Q represents a predicate,
or relation, among the values of the program variables. If this relation holds among
the values of the program variables before a loop iteration executes and holds
among the values after the iteration executes, then the relation among these variables is unaffected by the action of the loop iteration, even though the values
themselves may be changed. Such a relation is called a loop invariant.
Product (nonnegative integer x; nonnegative integer y)
Local variables:
integers i, j
i = 0
j = 0
while i ∙ x do
j = j + y
i = i + 1
end while
//j now has the value x * y
return j
end function Product
This function contains a loop; the condition B for continued loop execution is
i ∙ x. The condition B′ for loop termination is therefore i = x. When the loop
terminates, it is claimed in the comment that j has the value x * y. Thus, on loop
termination, we want
Q ` B′ = Q ` ( i = x )
and we also want
j = x * y
To have both
Q ` (i = x) and j = x * y
Q must be the assertion
j = i * y
(Notice that Q is a predicate, that is, it states a relationship between variables in
the program. It is never part of an equation such as Q = j.) To match the form of
(2), the assertion j = i * y would have to be true before the loop statement. This is
indeed the case because right before the loop statement, i = j = 0.
It would seem that for this example we have a candidate assertion Q for implication (2), but we do not yet have the rule of inference that allows us to say when
(2) is a true implication. (Remember that we discovered our Q by “wishful thinking” about the correct operation of the function code.)
Proofs, Induction, and Number Theory
Assertion Q must be true before the loop is entered. If implication (2) is to
hold, Q must remain true after the loop terminates. Because it may not be known
exactly when the loop will terminate, Q must remain true after each iteration
through the loop, which will include the final iteration. Q represents a predicate,
or relation, among the values of the program variables. If this relation holds among
the values of the program variables before a loop iteration executes and holds
among the values after the iteration executes, then the relation among these variables is unaffected by the action of the loop iteration, even though the values
themselves may be changed. Such a relation is called a loop invariant.
Product (nonnegative integer x; nonnegative integer y)
Local variables:
integers i, j
i = 0
j = 0
while i ∙ x do
j = j + y
i = i + 1
end while
//j now has the value x * y
return j
end function Product
This function contains a loop; the condition B for continued loop execution is
i ∙ x. The condition B′ for loop termination is therefore i = x. When the loop
terminates, it is claimed in the comment that j has the value x * y. Thus, on loop
termination, we want
Q ` B′ = Q ` ( i = x )
and we also want
j = x * y
To have both
Q ` (i = x) and j = x * y
Q must be the assertion
j = i * y
(Notice that Q is a predicate, that is, it states a relationship between variables in
the program. It is never part of an equation such as Q = j.) To match the form of
(2), the assertion j = i * y would have to be true before the loop statement. This is
indeed the case because right before the loop statement, i = j = 0.
It would seem that for this example we have a candidate assertion Q for implication (2), but we do not yet have the rule of inference that allows us to say when
(2) is a true implication. (Remember that we discovered our Q by “wishful thinking” about the correct operation of the function code.)