Section 2.3 More on Proof of Correctness
129
S e c t i o n 2 . 3 More on Proof of CorreCTness
In Section 1.6, we explained the use of a formal logic system to prove mathematically the correctness of a program. Assertions or predicates involving the program
variables are inserted at the beginning, at the end, and at intermediate points between
the program statements. Then proving the correctness of any particular program
statement s i involves proving that the implication represented by the Hoare triple
{Q} s i {R}
(1)
is true.Here Q and R are assertions known, respectively, as the precondition and
postcondition for the statement. The program is provably correct if all such implications for the statements in the program are true.
In Chapter 1, we discussed rules of inference that give conditions under
which implication (1) is true when s i is an assignment statement and when s i is a
conditional statement. Now we will use a rule of inference that gives conditions
under which implication (1) is true when s i is a loop statement. We have deferred
consideration of loop statements until now because mathematical induction is
used in applying this rule of inference.
loop rule
Suppose that s i is a loop statement in the form
while condition B do
P
end while
where B is a condition that is either true or false and P is a program segment.
When this statement is executed, condition B is evaluated. If B is true, program
segment P is executed and then B is evaluated again. If B is still true, program
segment P is executed again, then B is evaluated again, and so forth. If condition
B ever evaluates to false, the loop terminates.
The form of implication (1) that can be used when s i is a loop statement
imposes (like the assignment rule did) a relationship between the precondition and
the postcondition. The precondition Q holds before the loop is entered; strangely
enough, one requirement is that Q must continue to hold after the loop terminates
(which means that we should look for a Q that we want to be true when the loop
terminates). In addition, B′—the condition for loop termination—must be true
then as well. Thus (1) will have the form
{Q} s i {Q ` B′}
(2)
eXAMPLe 25
Consider the following pseudocode function, which is supposed to return the value
x * y for nonnegative integers x and y.
129
S e c t i o n 2 . 3 More on Proof of CorreCTness
In Section 1.6, we explained the use of a formal logic system to prove mathematically the correctness of a program. Assertions or predicates involving the program
variables are inserted at the beginning, at the end, and at intermediate points between
the program statements. Then proving the correctness of any particular program
statement s i involves proving that the implication represented by the Hoare triple
{Q} s i {R}
(1)
is true.Here Q and R are assertions known, respectively, as the precondition and
postcondition for the statement. The program is provably correct if all such implications for the statements in the program are true.
In Chapter 1, we discussed rules of inference that give conditions under
which implication (1) is true when s i is an assignment statement and when s i is a
conditional statement. Now we will use a rule of inference that gives conditions
under which implication (1) is true when s i is a loop statement. We have deferred
consideration of loop statements until now because mathematical induction is
used in applying this rule of inference.
loop rule
Suppose that s i is a loop statement in the form
while condition B do
P
end while
where B is a condition that is either true or false and P is a program segment.
When this statement is executed, condition B is evaluated. If B is true, program
segment P is executed and then B is evaluated again. If B is still true, program
segment P is executed again, then B is evaluated again, and so forth. If condition
B ever evaluates to false, the loop terminates.
The form of implication (1) that can be used when s i is a loop statement
imposes (like the assignment rule did) a relationship between the precondition and
the postcondition. The precondition Q holds before the loop is entered; strangely
enough, one requirement is that Q must continue to hold after the loop terminates
(which means that we should look for a Q that we want to be true when the loop
terminates). In addition, B′—the condition for loop termination—must be true
then as well. Thus (1) will have the form
{Q} s i {Q ` B′}
(2)
eXAMPLe 25
Consider the following pseudocode function, which is supposed to return the value
x * y for nonnegative integers x and y.