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

While the trace is empty, an event can be refused by just if it can be

refused by both of them. When the trace is non-empty, the subsequent behaviour
is determined by either

P + Q

, whichever is consistent with the rst event in
the trace. If both are, the result is non-deterministic. As in the case of the condi-
tional, the algebraic properties of this simple denition can be simply veried by
truth tables. External choice is commutative, idempotent and associative, with
unit 0 ; and it is mutually distributive with non-deterministic union. The corre-
sponding operator ￿ in CSP has the same properties, but its denition has been
made a little more complicated, to take account of the risk of divergence of one
of its two operands. The top-down approach to both theories helps to elucidate
exactly how two very similar theories may in some ways be subtly dierent.
The aim of the top-down method of system development is to deliver pro-
grams that are correct. Assurance of correctness is obtained not just by testing
or debugging the code, but by the quality of the reasoning that has gone into its
construction. This top-down philosophy of correctness by construction is based
on the premise that every specication and every design and every program can
be interpreted as a description of some subset of a mathematically dened space
of observations. But the converse is certainly not true. Not every subset of the
observation space is expressible as a program. For example, the empty predicate
false represents a specication that no physical object could ever implement: if
it did, the object described would be irretrievably unobservable.
The question therefore arises, what are the additional characteristics of those
subsets of observations that are in fact denable in the restricted notations of
a particular programming language? The answer would help us to distinguish
the feasible specications that can be implemented by program from the in-
feasible ones that cannot. The distinguishing characteristics of implementable
specications have been called healthiness conditions [Dijkstra]. They act like
conservation laws or symmetry principles in physics, which enable the scientist
quickly to dismiss impossible experiments and implausible theories; and simi-
larly they can protect the engineer from many a wild-goose chase. As in the
natural sciences, healthiness conditions can be justied by appeal to the real-
world meaning of the variables in the alphabet. Analysis of termination gives a
good example.
A characteristic feature of a program in any programming language is that
if its rst part fails to terminate, any fragment of program which is written
to be executed afterwards will never be started, and the whole program will
also fail to terminate. In our top-down theory, the non-terminating program is
represented by the predicate true ; so the relevant healthiness condition can be
neatly expressed as an algebraic law, stating that true is a left zero for sequential
composition

P or Q

true ; P = true , for all programs P

This law is certainly not true for all predicates P ; for example, when P is false,

we have

true ; false = false