Theories of programming: Top-Down and Bottomup and Neeting in the Middle
C. A. R. Hoare6 
| (6) |
Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD |
Abstract
A theory of programming provides a scientific basis for programming practices that lead to predictable delivery of programs
of high quality. A topdown theory starts with a specification of the intended behaviour of a program; and a bottomup theory
starts with a description of how the program is executed. The aim of both theories is to prove theorems (often algebraic laws)
that will be helpful in the design, development, compilation, testing, optimisation and maintainance of all kinds of program.
The most mature theories are those that are presented both in bottomup and top-down fashion, where essentially the same laws
are valid in both presentations.
Acknowledgements The views put forward in this paper evolved during a long collaboration with He Jifeng on research into unifying theories
of programming. They contribute towards goals pursued by the partners in the EC Basic Research Project CON- CUR;and they have
been subjected to test in the EC Basic Research Project PROCOS. They are more fully expounded in the reference [Hoare, He],
which contains a list of 188 further references. Significant contributors to this work at Oxford include Carroll Morgan, Jeff
Sanders, Oege de Moor, Mike Spivey, Jeff Sanders, Annabelle McIver, Guy McCusker, and Luke Ong. Other crucial clarifications
and insights were obtained during a sabbatical visit to Cambridge in conversations with Robin Milner, Andy Pitts, Martin Hyland,
Philippa Gardner, Peter Sewell, Jamey Leifer, and many others. I am also grateful to Microsoft Research Limited for supporting
my visit to Cambridge, and to researchers at Microsoft who have devoted their time to my further education, including Luca
Cardelli, Andy Gordon, Cedric Fournet, Nick Benton and Simon Peyton Jones. The organisers of POPL 1999 in San Antonio invited
me to present my thoughts there, and the participants gave useful encouragement and feedback. Krzysztof Apt and John Reynolds
have suggested many improvements that have been made since an earlier draft of the paper, and more that could have been.
References secured to subscribers.