Unifying Theories of Programming: Difference between revisions

Revision as of 15:21, 10 November 2022

Revision as of 12:16, 8 December 2022

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 |author-link=C.A.R. Hoare |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]]:

<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>[[{{cite journal |last1=Hoare|first1=C.A.R. Hoare]], |title=Programming: Sorcery or science? |journal=[[IEEE Software]], |volume=1( |issue=2): |pages=5–16, |date=April 1984. {{ISSN|0740-7459}}. {{doi|=10.1109/MS.1984.234042|s2cid=375578 }}.</ref></blockquote>

In UTP parlance, a ''theory'' is a model of a particular programming paradigm. A UTP theory is composed of three ingredients:

Line 19:

<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>[[{{cite book |author1-link=Edsger W. Dijkstra]] and|first1=Edsger [[W. |last1=Dijkstra |author2-link=Carel S. Scholten]] |first2=Carel S. |last2=Scholten |title=Predicate calculus and program semantics. |series=Texts and Monographs in Computer Science. |publisher=Springer-Verlag New York, Inc., New York, NY, USA, |year=1990. {{ISBN|isbn=0-387-96957-8}}. </ref> the [[universal closure]] of all variables in the alphabet.

==Relations==

Line 57:

==Further reading==

*{{cite [[book |author1-link=Jim Woodcock]] and|first1=Jim |last1=Woodcock |first2=Ana |last2=Cavalcanti. |volume=2999 |series=[[Lecture Notes in Computer Science]], pages |chapter=A tutorial introduction to designs in Unifying Theories of Programming |chapter-url=https://kar.kent.ac.uk/14036/1/A_Tutorial_Introduction_to_Designs_in.pdf In ''|title=Integrated Formal Methods'', volume 2999 of [[Lecture Notes in Computer Science]], pages 40–66. [[Springer-Verlag|publisher=Springer]] Berlin / Heidelberg, |date=2004. {{ISBN|isbn=978-3-540-21377-2}}. {{|pages=40–66 |doi|=10.1007/978-3-540-24756-2_4}} {{CiteSeerX|10.1.1.99.2929}} [https://www.cs.york.ac.uk/ftpdir/pub/leo/utp/tutorials/utp-tutorial-designs-v2.pdf paper]

*{{cite book |first1=Ana |last1=Cavalcanti and |first2=Jim |last2=Woodcock. A tutorial introduction to CSP in Unifying Theories of Programming. In ''Refinement Techniques in Software Engineering'', |volume =3167 of |series=Lecture Notes in Computer Science, pages|chapter=A 220–268.tutorial Springerintroduction Berlinto /CSP Heidelberg,in 2006.Unifying {{doi|10.1007/11889229_6}}Theories of Programming {{CiteSeerX|10.1.1.97.3469}} [chapter-url=https://www.cs.york.ac.uk/ftpdir/pub/leo/utp/tutorials/utp-tutorial-CSP.pdf paper]|title=Refinement Techniques in Software Engineering |publisher=Springer |date=2006 |isbn= 978-3-540-46253-8|pages=220–268 |doi=10.1007/11889229_6}}

==External links==