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

Successful termination is one of the most important properties of a program
to predict, so we need a special variable (called ! ) which is true just if and

when termination occurs. The corresponding initial variable

ok

ok

indicates that

the program has started. Of course a false value of ! will never be conclusively

observed; but that doesn't matter, because the intention of the theorist and the
programmer alike is to ensure it that !

ok

is necessarily true, and to prove it. Such
a proof would be vacuous if the possibility of its falsity were not modelled in
the theory. In general, for serious proof of total correctness of programs, it is
essential to model realistically all the ways in which a program can go wrong,
even if not directly observable. In fact, the progress of science is marked by
acceptance of such unobservable abstractions as force and mass and friction as
though they were directly measurable quantities. As Einstein pointed out, it is
the theory itself which determines what is observable.
In the interactive programming paradigm, the most important observable
component of program behaviour is an interaction between the system and its
environment. Each kind of interaction has a distinct name. For example, in the
process algebra CCS[Milner] the event name coin may stand for the insertion of a
pound coin in the slot of a vending machine, and the event name choc may stand
for the selection and extraction of a chocolate bar by the user. The CSP[Roscoe]
variant of process algebra allows the user to record a trace of the sequence in
which such events have occurred while the machine is running; so

ok

h coin, choc,

coin is a value of trace observed in the middle of the second transaction of the

machine; the empty trace

i

is the value when the machine is rst delivered. We
also model the possibility of deadlock (hang-up) by recording the set of events
currently oered by the machine's environment, but which it refuses to accept.
For example, initially the machine refuses

hi

because it has not been paid
(or perhaps because it has run out of chocolates). A deadlocked machine is one
that refuses all the events oered by its environment.
Practical programming of useful systems will involve a combination of in-
teractive and imperative programming features; and the relevant alphabet must
include both internal variable names and external event names. The special vari-
able !

f choc g

should be reinterpreted as successful stabilisation, or avoidance of livelock
(divergence). A new special variable !

ok

is needed to distinguish those stable
states in which the program is waiting for an interaction with its environment
from those in which it has successfully terminated. An important achievement in
the theory of programming has been to formalise separate models for sequential
and for interactive programs, and then to combine them with only a minimum
of extra complexity.
A top-down theory of programming is highly conducive to a top-down method-
ology for program design and development. The identiers chosen to denote the
relevant observations of the ultimate program are rst used to describe the in-
tended and permitted behaviour of a program, long before the detailed program-
ming begins. For example, a program can be specied not to decrease the value
of

wait

x by the statement