Content deleted Content added
m dab link |
Rescuing 1 sources and tagging 1 as dead.) #IABot (v2.0.9.5 |
||
| (18 intermediate revisions by 11 users not shown) | |||
Line 1:
{{short description|Formal semantics and 1998 book}}
'''''Unifying Theories of Programming''''' (UTP) 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.▼
{{use dmy dates|date=June 2025}}
{{use British English|date=June 2025}}
{{italic title}}
{{Infobox book
| 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 has been 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|isbn=978-0-13-458761-5|pages=320|url=http://unifyingtheories.org/|accessdate=7 October 2016|archive-date=7 October 2016|archive-url=https://web.archive.org/web/20161007215026/http://unifyingtheories.org/|url-status=bot: unknown}}</ref>
== Theories ==▼
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>
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>▼
▲The semantic foundation of the UTP is the [[first-order predicate calculus]], augmented with fixed
▲<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>
In UTP parlance, a ''theory'' is a model of a particular programming paradigm. A UTP theory is composed of three ingredients:
Line 20 ⟶ 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>
== 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 47 ⟶ 97:
<math>P_1 \sqcap P_2 \equiv P_1 \lor P_2</math>
* [[
<math>P_1 \triangleleft C \triangleright P_2 \equiv ( C \land P_1 ) \lor ( \lnot C \land P_2 )</math>
Line 55 ⟶ 105:
<math>\mu X \bullet \mathbf{F}(X) \equiv \sqcap \left\{ X \mid \mathbf{F}(X) \sqsubseteq X \right\}</math>
==
{{reflist}}
==
*{{cite book |author1-link=Jim Woodcock |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 |title=Integrated Formal Methods |publisher=Springer |date=2004 |isbn=978-3-540-21377-2 |pages=40–66 |doi=10.1007/978-3-540-24756-2_4}}
*{{cite book |first1=Ana |last1=Cavalcanti |first2=Jim |last2=Woodcock |volume=3167 |series=Lecture Notes in Computer Science |chapter=A tutorial introduction to CSP in Unifying Theories of Programming |chapter-url=https://www.cs.york.ac.uk/ftpdir/pub/leo/utp/tutorials/utp-tutorial-CSP.pdf |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:1998 books]]
[[Category:Computer science books]]
[[Category:Formal methods publications]]
[[Category:Programming language semantics]]
[[Category:Prentice Hall books]]
▲[[hr:Unifying Theories of Programming]]
| |||