Hoare C.A.R., Jifeng H. Unifying theories of programming

New York: Prentice-Hall, 1998. — 311 p.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 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:
an alphabet, which is a set of variable names denoting the attributes of the paradigm that can be observed by an external entity;
a signature, which is the set of programming language constructs intrinsic to the paradigm;
and a collection of healthiness conditions, which define the space of programs that fit within the paradigm. These healthiness conditions are typically expressed as monotonic idempotent predicate transformers.