13.2. Reasoning AboutWhilePrograms 395
13.2.4 Logic of Programs
A typical program specification describes the kind of inputs and environments the
program should handle, and then describes what should result from an execution.
The specification of the inputs or initial environment is called thepreconditionfor
program execution, and the prescription of what the result of execution should be
is called thepostcondition. So ifPis a logical formula expressing the precondition
for a program,C, and likewiseQexpresses the postcondition, the specification
requires that
IfPholds whenCis started, thenQwill hold if and whenChalts.We’ll express this requirement as a formula
PfCgQcalled apartial correctness assertion.
For example, ifEis thewhileprogram above for the Euclidean algorithm, then
the partial correctness ofEcan be expressed as
.a;b 2 NAND a¤ 0 /fEg.xDgcd.a;b//: (13.4)More precisely, notice that just as the value of an expression in an environment
is an integer, the value of a logical formula in an environment is a truth value. For
example, if.x/D 4 , and.y/D 2 , then by (13.3),ŒŒx^2 Cy 3 ççD 11 , so
ŒŒ 9 z:z> 4ANDx^2 Cy 3 DzççDT;
ŒŒ 9 z:z> 13ANDx^2 Cy 3 DzççDF:Definition 13.2.7.For logical formulasPandQ, andwhileprogram,C, the partial
correctness assertion
PfCgQ
is true proving that for all environments,rho, ifŒŒPççis true, andhC; i !
hDone; ^0 ifor some^0 , thenŒŒQçç^0 is true.
In the 1970’s, Prof. Tony Hoare (now Sir Anthony) at Univ. Dublin formulated
a set of inference rules for proving partial correctness formulas. These rules are
known asHoare Logic.
The first rule captures the fact that strengthening the preconditions and weaken-
ing the postconditions makes a partial correctness specification easier to satisfy:
P IMPLIES R; RfCgS; S IMPLIES Q
PfCgQ