Unifying Theories of Programming: Difference between revisions

Revision as of 22:39, 17 September 2014

Revision as of 17:10, 7 November 2014

Line 1:

'''''Unifying Theories of Programming''''' ('''UTP''') in [[computer science]] deals with [[program semantics]]. It shows how [[denotational semantics]], [[operational semantics]] and [[algebraic semantics (computer science)|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 and is now freely available on the web.<ref>{{cite book|last1=Hoare|first1=C. A. R.|last2=Jifeng|first2=He|title=Unifying Theories of Programming|date=April 1, 1998|publisher=Prentice Hall College Division|isbn=978-0-13-458761-5|pages=320|url=http://www.unifyingtheories.org/|accessdate=17 September 2014}}</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]]:

Line 22 ⟶ 21:

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:

Line 55 ⟶ 53:

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

== References ==

{{reflist}}

== Further reading ==

* Ana[[Jim CavalcantiWoodcock]] and JimAna WoodcockCavalcanti. A tutorial introduction to CSPdesigns in Unifying Theories of Programming. In Refinement''Integrated TechniquesFormal in Software EngineeringMethods'', volume 31672999 of [[Lecture Notes in Computer Science]], pages 220–26840–66. [[Springer-Verlag|Springer]] Berlin / Heidelberg, 20062004. doi:ISBN [http://dx978-3-540-21377-2.doi.org/10.1007/11889229_6 {{DOI|10.1007/11889229_6].978-3-540-24756-2_4}}

* JimAna WoodcockCavalcanti and AnaJim CavalcantiWoodcock. A tutorial introduction to designsCSP in Unifying Theories of Programming. In Integrated''Refinement FormalTechniques Methodsin Software Engineering'', volume 29993167 of Lecture Notes in Computer Science, pages 40–66220–268. Springer Berlin / Heidelberg, 20042006. ISBN 978-3-540-21377-2. doi: [http://dx.doi.org/{{DOI|10.1007/978-3-540-24756-2_411889229_6 10.1007/978-3-540-24756-2_4]11889229_6}}

* 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].

==External links==

* [http://www.unifyingtheories.org/ UTP book website]

[[Category:1998 books]]