Content deleted Content added
m cat |
Rescuing 1 sources and tagging 1 as dead.) #IABot (v2.0.9.5 |
||
| (37 intermediate revisions by 25 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 =
}}
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>
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. |title=Programming: Sorcery or science? |journal=[[IEEE Software]] |volume=1 |issue=2 |pages=5–16 |date=April 1984 |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:
* 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>{{cite book |author1-link=Edsger W. Dijkstra |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 |year=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 [[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==
*{{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:Computer science books]]
[[Category:Formal methods publications]]
[[Category:Programming language semantics]]
[[Category:Prentice Hall books]]
| |||