A proof that a program is correct (always produces the correct output for every possible input) consists of two parts:
- Show that the correct answer is obtained if the program terminates. This part of the proof establishes the partial correctness of the program.
- Show that the program always terminates.
Two propositions are used to specify a program produces the correct output:
- Initial Assertion - Gives properties that the input values must have.
- Final Assertion - Gives the properties that the output of the program should have, if the program did what was intended.
The appropriate and final assertions must be provided when a program is checked.
A program, or program segment, S is said to be partially correct with respect to the initial assertion p and the final assertion q if whenever p is true for the input values of S and S terminates, then q is true for the output values of S. The notation p{S}q indicates that the program, or program segment, S is partially correct with respect to the initial assertion p and the final assertion q.
The composition rule, which can be stated as
∴p{S1}qq{S2}rp{S1;S2}r
It is stating that a program S is split into subprograms S1 and S2. S=S1;S2 indicates S is made up of S1 followed by S2.
Suppose that the correctness of S1 with respect to the initial assertion p and final assertion q, and the correctness of S2 with respect to the initial assertion q and the final assertion r, have been established. It follows that if p is true and S1 is executed and terminates, then q is true; and if q is true, and S2 executes and terminates, then r is true.
Thus, if p is true and S=S1;S2 is executed and terminates, then r is true.
∴(p∧ condition ){S}q(p∧¬ condition )→qp{ if condition then S}q
For the program segment
if condition then
S
where S is a block of statements. Then S is executed iff condition is true.
To verify this particular program segment is correct with respect to the initial assertion p and final assertion q, two things must be shown:
- When p is true and condition is also true, then q is true after S terminates.
- When p is true and condition is false, then q is true (because S does not execute).
∴(p∧ condition ){S1}q(p∧¬ condition ){S2}qp{ if condition then S1elseS2}q
if condition then
S1
else
S2
To verify this particular program segment is correct with respect to the initial assertion p and final assertion q, two things must be shown:
- When p is true and condition is true, then q is true after S1 terminates.
- When p is true and condition is false, then q is true after S2 terminates.