Theories of Programming: Top-Down and Bottom-Up and Meeting in the Middle - Correct System Design: Recent Insights and Advances - page 13

This just means that the healthiness condition is succeeding in its primary pur-
pose of showing that unimplementable predicates like false can never be ex-
pressed as a program.
The majority of simple algebraic laws that are applicable to programs can
be proved once-for-all as mathematical theorems about sets of observations; and
they can be applied equally to designs and even to specications. But healthiness
conditions, as we have seen, are just not true for arbitrary sets: they cannot be
proved and they must not be applied to specications. Their scope is mainly
conned to reasoning about programs, including program transformation and
optimisation. It is therefore an obligation on a programming theorist to prove
that each healthiness condition holds at least for all programs expressible in the
restricted notations of the programming language, and perhaps to certain design
notations as well.
The method of proof is essentially inductive on the syntax of the language. All
the primitive components of a program must be proved to satisfy the healthiness
condition; furthermore, all the operators of the language (including recursion)
must be proved to preserve the health of their operands. Here is a proof that
union and sequential composition preserve the healthiness condition that they
respect non-termination
true ;(

P_Q f g

) rel. composition distributes through disjunction

=( true ; P ) _ ( true ; Q ) f by induction hypothesis, P and Q are healthy g

= true _ true f_ is idempotent g

= true
For sequential composition
true ;(

P ; Q ) f composition is associative g

=( true ; P ); Q f by inductive hypothesis, P is healthy g

= true ; Q f by inductive hypothesis, Q is healthy g

= true

Algebraic laws are so useful in reasoning about programs, and in transform-
ing them for purposes of optimisation, that we want to have as many laws as
possible, provided of course that they are valid. How can we know that a list of
proven laws is complete in some appropriate sense? One possible sense of com-
pleteness is given by a normal form theorem, which shows that every program
in the language can be reduced (or rather expanded) to a normal form (not
necessarily expressible in the programming language). A normal form should be
designed so that the identity of meaning of non-identical normal forms is quite
easy to decide, for example, merely by rearranging their sub-terms. Furthermore,
if two normal forms are unequal, it should always be possible to nd an obser-
vation described by one of them but not the other. Unfortunately, there may
be no nite set of algebraic laws that exactly characterises all true facts about
the programming language. For example, even the simple relational calculus has
no complete nite axiomatisation. One interpretation of the Church-Turing hy-