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

assembly by a calculation based only on descriptions of the behaviour of its ma-
jor components. The collection of formulae used for these calculations eectively
constitutes a denotational semantics for the languages in which a system is speci-
ed, designed, and eventually implemented. The programming language used for
ultimate implementation is dened by simply selecting an implementable sub-
set of the mathematically dened notations for describing program behaviour.
The correctness of a program simply means that all possible observations of its
behaviour under execution are included in the range dened by its specica-
tion. The development of the theory starts from the denotational denitions and
continues by formalisation and proof of theorems that express the properties
of all programs written in the language. The goal is to assemble a collection
of mathematical laws (usually equations and inequations) that will be useful in
the top-down design of programs from their specications, and ensure that the
resulting code is correct by construction.
Investigation of a complex system from the bottom-up starts with an at-
tempt to discover a minimum collection of primitive components from which it
has been made, or in principle could have been. These are assembled into larger
components by primitive combinators, selected again from a minimal set. The no-
tations chosen to denote these primitives and combinators constitute the syntax
of a simple programming language. Since programs are intended for execution
by a machine, their operational meaning is dened by enumerating the kinds
of primitive step that will be taken by the machine in executing any program
that is presented to it. The theory may be further developed by investigation
of properties of programs that are preserved by all the possible execution steps;
they are necessarily preserved throughout execution of any program. The result-
ing classication of programs is presented as a set of axioms that can be used
in proofs that a program enjoys the relevant property. The properties are often
decidable, and the axioms can be used as a type system for the programming
language, with conformity checkable by its compiler. In favourable cases, the
type system allows unique or canonical types to be inferred from an untyped
program. Such inference can help in the understanding of legacy code, possibly
written without any comprehensible documentation describing its structure or
purpose (or worse, the original documentation often has not been kept up to
date with the later changes made to the code).
The benets of a top-down presentation of a theory are entirely complemen-
tary to those of a bottom-up presentation. The former is directly applicable to
discussion and reasoning about the design of a program before it has been writ-
ten, and the latter to the testing, debugging, and modication of code that has
already been written. In both cases, successful application of the theory takes
advantage of a collection of theorems proved for this purpose. The most useful
theorems are those which take the form of algebraic laws. The advantages of
both approaches can be condently combined, if the overlap of laws provided
by both of them is suciently broad. The laws are a specication of the com-
mon interface where the two approaches meet in the middle. I suggest that such
a convergence of laws developed by complementary approaches and applied to