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

possible upon it. But this understanding is exactly what the security analysis
seeks to develop; it cannot be postulated in advance.
A great deal of research eort has been expended on designing proof tech-
niques that are simpler to apply and more ecient to mechanise than proof by
non-contradiction. Many of these methods use a variation of the technique of
bisimulation [Milner]. A bisimulation is a postulated equivalence between pro-
grams that is respected by the individual steps of the operational semantics of
the language, i.e., if two programs belong to the same equivalence class before
the step, they belong to the same equivalence class afterwards. For particular
calculi and for particular kinds of bisimulation, theorists have proved that the
postulation of the bisimulation as an equality will not lead to a contradiction.
Then that kind of bisimulation may safely be used to prove equality of arbi-
trary programs in the language. For a well-explored calculus, there may be a
whole range of bisimulations of varying strength, some suitable for mechanisa-
tion, and some suitable for quick disproof. They are all approximations to the
truly intended notion of equality, which is dened by the more elusive concept
of contextual equivalence.
As described above, much of the eort in a bottom-up theory goes into the
determination of when two programs are equal. This is absolutely no problem in
a top-down theory, where normal mathematical equality of sets of observations
is used throughout. Conversely, much of the eort of a top-down theory goes into
determination of which subsets of observations correspond to implementations.
This is absolutely no problem in a bottom-up theory, where programs are always
by denition computable. In each case the theorist approaches the target by a
series of approximations. In the happy circumstance that they are working on
the same language and the same theory, top-down and bottom-up will eventually
meet in the middle.
4 Meeting in the Middle
A brief summary of the merits and deciencies of top-down and bottom-up
presentations show that they are entirely complementary.
{ A top-down presentation of a theory of programming gives excellent support
for top-down development of programs, with justiable condence that they
are correct by construction. By starting with observable system properties
and behaviour, it permits and encourages the advance specication of a sys-
tem yet to be implemented, and the careful design of the interfaces between
its major components. It provides concepts, notations and theorems that
can be used throughout the design and implementation of software systems
of any size and complexity. On the other hand, an abstract denotational
semantics gives no help at all in the debugging of incorrect programs. It is
therefore useless in the analysis of legacy systems, many of which have been
written and frequently changed without regard to general design principles,
clarity of structure, or correctness of code.