A Theory of Programming: Denotational, Algebraic and Operational Semantics

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 for 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.