Unifying Theories of Programming explained

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.^[1]

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.^[2]

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.

Program refinement is an important concept in the UTP. A program

P _{1} is refined by P _{2} if and only if every observation that can be made of P _{2} is also an observation of P _{1} .The definition of refinement is common across UTP theories:P _{1} \sqsubseteq P _{2} ifandonlyif \left[ P _{2} ⇒ P _{1} \right]

where

\left[ X \right] denotes^[3] 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:

• undecorated variables (

v ), modelling an observation of the program at the start of its execution; and

• primed variables (

v' ), modelling an observation of the program at a later stage of its execution.

Some common language constructs can be defined in the theory of relations as follows:

• The skip statement, which does not alter the program state in any way, is modelled as the relational identity:

skip \equiv v' = v

• The assignment of value

E to a variable a is modelled as setting a' to E and keeping all other variables (denoted by u ) constant:a : = E \equiv a' = E \land u' = u

• The sequential composition of two programs is just relational composition of intermediate state:

P _{1} ; P _{2} \equiv \exists v _{0} \bullet P _{1} [ v _{0} / v' ] \land P _{2} [ v _{0} / v ]

• Non-deterministic choice between programs is their greatest lower bound:

P _{1} \sqcap P _{2} \equiv P _{1} \lor P _{2}

• Conditional choice between programs is written using infix notation:

P _{1} \triangleleft C \triangleright P _{2} \equiv ( C \land P _{1} ) \lor ( ln ot C \land P _{2} ) \mu F of a monotonic predicate transformer F :\mu X \bullet F (X) \equiv \sqcap \left\{ X \mid F (X) \sqsubseteq X \right\}

Further reading

• Book: Jim Woodcock . Jim . Woodcock . Ana . Cavalcanti . 2999 . Lecture Notes in Computer Science, pages . A tutorial introduction to designs in Unifying Theories of Programming . https://kar.kent.ac.uk/14036/1/A_Tutorial_Introduction_to_Designs_in.pdf . Integrated Formal Methods . Springer . 2004 . 978-3-540-21377-2 . 40–66 . 10.1007/978-3-540-24756-2_4.
• Book: Ana . Cavalcanti . Jim . Woodcock . 3167 . Lecture Notes in Computer Science . A tutorial introduction to CSP in Unifying Theories of Programming . https://www.cs.york.ac.uk/ftpdir/pub/leo/utp/tutorials/utp-tutorial-CSP.pdf . Refinement Techniques in Software Engineering . Springer . 2006 . 978-3-540-46253-8. 220–268 . 10.1007/11889229_6.

External links

• UTP book website
• UTP book on Archive.org

Notes and References

1. Book: C.A.R. Hoare . Hoare. C. A. R.. Jifeng. He. Unifying Theories of Programming. April 1, 1998. Prentice Hall . 978-0-13-458761-5. 320. 17 September 2014.
2. Hoare. C.A.R. . Programming: Sorcery or science? . . 1 . 2 . 5–16 . April 1984 . 10.1109/MS.1984.234042. 375578 .
3. Book: Edsger W. Dijkstra . Edsger W. . Dijkstra . Carel S. Scholten . Carel S. . Scholten . Predicate calculus and program semantics . Texts and Monographs in Computer Science . Springer . 1990 . 0-387-96957-8.