Unified Theories of Programming

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. The paper presents simple theories of sequential non deterministic programming in each of these three styles; by deriving each presentation from its predecessor in a cyclic fashion, mutual consistency is assured.