Unifying Theories of Programming: Difference between revisions

Revision as of 07:48, 10 August 2015

Latest revision as of 08:48, 30 July 2025

(13 intermediate revisions by 8 users not shown)

Line 1:

{{short description|Formal semantics and 1998 book}}

{{use dmy dates|date=June 2025}}

{{use British English|date=June 2025}}

{{italic title}}

{{Infobox book

| italic title = Unifying Theories of Programming

| name = Unifying Theories of Programming

| image =

| image_size =

| border =

| alt =

| caption =

| author = [[C. A. R. Hoare]]<br/>[[He Jifeng]]

| audio_read_by =

| title_orig =

| orig_lang_code =

| title_working =

| translator =

| illustrator =

| cover_artist =

| country = [[United Kingdom]]

| language = [[English language|English]]

| series = Series in Computer Science

| release_number =

| subject =

| genre = Scientific non-fiction

| set_in =

| publisher = [[Prentice Hall]]

| publisher2 =

| pub_date = 1998

| english_pub_date =

| published =

| media_type =

| pages = xix+298

| awards =

| isbn = 0-13-458761-8

| isbn_note =

| oclc =

| dewey = 005.1/01

| congress = QA76.6. .H5735 1998

| preceded_by = <!-- for books in a series -->

| followed_by = <!-- for books in a series -->

| native_wikisource =

| wikisource =

| notes =

| exclude_cover =

| website = [https://web.archive.org/web/20161007215026/http://unifyingtheories.org/ unifyingtheories.org]

| module =

}}

'''''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]]<ref>{{cite book| chapter=Hoare and He's Unifying Theories of Programming | first=Jim | last=Woodcock | author-link=Jim Woodcock | title=Theories of Programming: The Life and Works of Tony Hoare | date=October 2021 | pages=285–316 | doi=10.1145/3477355.3477369 | publisher=[[Association for Computing Machinery]] | editor-first1=Cliff B. | editor-last1=Jones | editor-link1=Cliff Jones (computer scientist) | editor-first2=Jayadev | editor-last2=Misra | editor-link2=Jayadev Misra }}</ref> was published in the [[Prentice Hall International Series in Computer Science]] in 1998 and ishas nowbeen made freely available on the web.<ref>{{cite book|author-link1=C.A.R. Hoare|last1=Hoare|first1=C. A. R.|last2=Jifeng|first2=He|author-link2=He Jifeng|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=177 SeptemberOctober 2016|archive-date=7 October 2016|archive-url=https://web.archive.org/web/20161007215026/http://unifyingtheories.org/|url-status=bot: 2014unknown}}</ref>

A UTP Symposium series was started in 2006.<ref>{{cite book| editor-first1=Steve | editor-last1=Dunne | editor-first2=Bill | editor-last2=Stoddart | title=Unifying Theories of Programming: First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5–7, 2006 | date=2006 | publisher=[[Springer Science+Business Media|Springer]] | series=[[Lecture Notes in Computer Science]] | url=https://link.springer.com/content/pdf/10.1007/11768173.pdf | doi=10.1007/11768173 }}</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 ⟶ 71:

<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 45 ⟶ 97:

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

* [[Conditional_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>

Line 57 ⟶ 109:

==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. {{DOI|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_6Theories 10.1007/11889229_6}}of {{citeseerx|10.1.1.97.3469}}Programming [|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 }}{{Dead link|date=July 2025 |bot=InternetArchiveBot |fix-attempted=yes }}

==External links==

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

* [https://web.archive.org/web/20161007215026/http://unifyingtheories.org/ UTP book] on [[Archive.org]]

* [https://openlibrary.org/books/OL351206M/Unifying_theories_of_programming UTP book] in the [[Internet Archive]] Open Library

[[Category:1998 non-fiction books]]

[[Category:Computer science books]]

[[Category:Formal methods publications]]

[[Category:Programming language semantics]]

[[Category:Prentice Hall books]]