Unifying Theories of Programming
Unifying Theories of Programming (UTP) in computer science deals with program semantics. It shows how denotational semantics, operational semantics and algebraic semantics can be combined in a unified framework for the formal specification, design and implementation of programs and computer systems. The book of this title by C.A.R. Hoare and He Jifeng was published in the Prentice Hall International Series in Computer Science in 1998 and is now freely available on the web. Theories. The semantic foundation of the UTP is the first-order predicate calculus, augmented with fixed point constructs from second-order logic. Following  the tradition of Eric Hehner, programs are predicates in the UTP, and there is no distinction between programs and specifications at the semantic level. In the words of Hoare: A computer program is identified with the strongest predicate describing every relevant observation that can be made of the behaviour of a computer executing that program. In UTP parlance, a "theory" is a model of a particular programming paradigm. A UTP theory is composed of three ingredients: Program refinement is an important concept in the UTP. A program formula_1 is refined by formula_2 if and only if every observation that can  be made of formula_2 is also an observation of formula_1. The definition of refinement is common across UTP theories: formula_5 where formula_6 denotes the universal closure of all variables in the alphabet. Relations. The most basic UTP theory is the alphabetised predicate calculus, which has no alphabet restrictions or healthiness conditions. The theory of relations is slightly more specialised, since a relation's alphabet may consist of only: Some common language constructs can be defined in the theory of relations as follows: formula_9 formula_15 formula_16 formula_17 formula_18 formula_21