by C. A. R. Hoare – 1980 ACM Turing Award

Professional practice in a mature engineering discipline is based on relevant scientific theories, usually expressed in the language of mathematics. A mathematical theory of programming aims to provide a similar basis for specification, design and implementation of computer programs. The theory can be presented in a variety of styles, including

1. Denotational, relating a program to a specification of its observable properties and behaviour.
2. Algebraic, providing equations and inequations comparison, transformation and optimisation of designs and programs.
3. Operational, describing individual steps of a possible mechanical implementation.

This paper presents a simple theory of sequential non-deterministic programming in each of these three styles; by deriving each presentation from its predecessor, mutual consistency is assured.

[論文] [其他訊息]