158 Chapter 3 Describing Syntax and Semantics
Because of the difficulty of proving loop termination, that requirement
is often ignored. If loop termination can be shown, the axiomatic description
of the loop is called total correctness. If the other conditions can be met but
termination is not guaranteed, it is called partial correctness.
In more complex loops, finding a suitable loop invariant, even for partial
correctness, requires a good deal of ingenuity. Because computing the pre-
condition for a while loop depends on finding a loop invariant, proving the
correctness of programs with while loops using axiomatic semantics can be
difficult.3.5.3.7 Program Proofs
This section provides validations for two simple programs. The first example
of a correctness proof is for a very short program, consisting of a sequence of
three assignment statements that interchange the values of two variables.{x = A AND y = B}
t = x;
x = y;
y = t;
{x = B AND y = A}Because the program consists entirely of assignment statements in a
sequence, the assignment axiom and the inference rule for sequences can be
used to prove its correctness. The first step is to use the assignment axiom on
the last statement and the postcondition for the whole program. This yields
the precondition{x = B AND t = A}Next, we use this new precondition as a postcondition on the middle state-
ment and compute its precondition, which is{y = B AND t = A}Next, we use this new assertion as the postcondition on the first statement
and apply the assignment axiom, which yields{y = B AND x = A}which is the same as the precondition on the program, except for the order of
operands on the AND operator. Because AND is a symmetric operator, our proof
is complete.
The following example is a proof of correctness of a pseudocode program
that computes the factorial function.