86
Formal Logic
A predicate R describes conditions that the output values are supposed to satisfy.
These conditions will often involve the input values as well, so R has the form
R(X, Y ) or R[X, P(X )]. In our square root case, if y is the single output value, then
y is supposed to be the square root of x, so R(x, y) would be “y
2
= x.” Program P
is correct if the implication
(4X )(Q(X ) S R[X, P(X )])
(1)
is valid. In other words, whenever Q is true about the input values, R should be
true about the input and output values. For the square root case, (1) is
(4x)(x > 0 S [P(x)]
2
= x )
The implication (1) is standard predicate wff notation, but the traditional program
correctness notation for (1) is
{Q}P{R}
(2)
{Q}P{R} is called a hoare triple, named for the British computer scientist
Anthony Hoare. Condition Q is called the precondition for program P, and condition R is the postcondition. In the Hoare notation, the universal quantifier does
not explicitly appear; it is understood.
Rather than simply having an initial predicate and a final predicate, a program
or program segment is broken down into individual statements s i , with predicates
inserted between statements as well as at the beginning and end. These predicates
are also called assertions because they assert what is supposed to be true about
the program variables at that point in the program. Thus we have
{Q}
s 0
{R 1 }
s 1
{R 2 }
(
s n−1
{R}
where Q, R 1 , R 2 , … , R n = R are assertions. The intermediate assertions are often
obtained by working backward from the output assertion R.
P is provably correct if each of the following implications holds:
{Q}s 0 {R l }
{R l }s l {R 2 }
{R 2 }s 2 {R 3 }
(
{R n−1 }s n−1 {R}
A proof of correctness for P consists of producing this sequence of valid
implications, that is, producing a proof sequence of predicate wffs. Some new
rules of inference can be used, based on the nature of the program statement s i .