Unifying Theories of Programming: Difference between revisions

Revision as of 18:36, 7 July 2012

Revision as of 15:16, 22 September 2012

Line 1:

'''''Unifying Theories of Programming''''' (UTP) 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 [[Computer program|program]]s and [[computer system]]s.

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.<ref>[[C.A.R. Hoare]] and [[He Jifeng]], ''Unifying Theories of Programming'', [[Prentice Hall International Series in Computer Science]], 1998. ISBN 0-13-458761-8.</ref>

== 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]], [[Predicative programming|programs are predicates]] in the UTP, and there is no distinction between programs and specifications at the semantic level. In the words of [[C.A.R. Hoare|Hoare]]:

<blockquote>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.<ref>[[C.A.R. Hoare]], Programming: Sorcery or science? [[IEEE Software]], 1(2): 5–16, April 1984. ISSN 0740-7459. doi: 10.1109/MS.1984.234042.</ref></blockquote>

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 transformer semantics|predicate transformers]].

[[Program refinement]] is an important concept in the UTP. A program <math>P_1</math> is refined by <math>P_2</math> if and only if every observation that can be made of <math>P_2</math> is also an observation of <math>P_1</math>.

The definition of refinement is common across UTP theories:

<math>P_1 \sqsubseteq P_2 \quad\text{if and only if}\quad \left[ P_2 \Rightarrow P_1 \right]</math>

where <math>\left[ X \right]</math> denotes<ref>[[Edsger W. Dijkstra]] and [[Carel S. Scholten]]. Predicate calculus and program semantics. Texts and Monographs in Computer Science. Springer-Verlag New York, Inc., New York, NY, USA, 1990. ISBN 0-387-96957-8.</ref> 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 (<math>v</math>), modelling an observation of the program at the start of its execution; and

* primed variables (<math>v'</math>), 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:

<math>\mathbf{skip} \equiv v' = v</math>

* The assignment of value <math>E</math> to a variable <math>a</math> is modelled as setting <math>a'</math> to <math>E</math> and keeping all other variables (denoted by <math>u</math>) constant:

<math>a := E \equiv a' = E \land u' = u</math>

* The [[sequential composition]] of two programs is just [[http://en.wikipedia.org/wiki/Composition_of_relations|relational composition]] of intermediate state:

<math>P_1 ; P_2 \equiv \exists v_0 \bullet P_1 [ v_0 / v' ] \land P_2 [ v_0 / v ]</math>

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

<math>P_1 \sqcap P_2 \equiv P_1 \lor P_2</math>

* [[Conditional_(programming)|Conditional choice]] between programs is written using infix notation:

<math>P_1 \triangleleft C \triangleright P_2 \equiv ( C \land P_1 ) \lor ( \lnot C \land P_2 )</math>

* A semantics for [[recursion]] is given by the [[least fixed point]] <math>\mu \mathbf{F}</math> of a monotonic predicate transformer <math>\mathbf{F}</math>:

<math>\mu X \bullet \mathbf{F}(X) \equiv \sqcap \left\{ X \mid \mathbf{F}(X) \sqsubseteq X \right\}</math>

== References ==

{{reflist}}

== Further reading ==

* Jim Woodcock and Ana Cavalcanti. A tutorial introduction to designs in Unifying Theories of Programming. In Integrated Formal Methods, volume 2999 of Lecture Notes in Computer Science, pages 40–66. Springer Berlin / Heidelberg, 2004. ISBN 978-3-540-21377-2. doi: [http://dx.doi.org/10.1007/978-3-540-24756-2_4 10.1007/978-3-540-24756-2_4]

* Ana Cavalcanti and Jim Woodcock. A tutorial introduction to CSP in Unifying Theories of Programming. In Refinement Techniques in Software Engineering, volume 3167 of Lecture Notes in Computer Science, pages 220–268. Springer Berlin / Heidelberg, 2006. doi: [http://dx.doi.org/10.1007/11889229_6 10.1007/11889229_6].

[[Category:1998 books]]