Unifying Theories of Programming

<h2 id="theories">Theories</h2>
The semantic foundation of the UTP is the <a href="/facts/First-order_predicate_calculus/lcISqWIg">first-order predicate calculus</a>, augmented with fixed point constructs from second-order logic. Following the tradition of <a href="/facts/Eric_Hehner/EnUm5Qef">Eric Hehner</a>, <a href="/facts/Predicative_programming/y6LeAYGe">programs are predicates</a> in the UTP, and there is no distinction between programs and specifications at the semantic level. In the words of <a href="/facts/C.A.R._Hoare/vBeb3cmn">Hoare</a>:

<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.<a class="footnote-ref" id="fnref:2" href="#fn:2">2</a></blockquote>
In UTP parlance, a theory is a model of a particular programming paradigm. A UTP theory is composed of three ingredients:

<ul><li>an alphabet, which is a set of variable names denoting the attributes of the paradigm that can be observed by an external entity;</li>
<li>a signature, which is the set of programming language constructs intrinsic to the paradigm; and</li>
<li>a collection of healthiness conditions, which define the space of programs that fit within the paradigm. These healthiness conditions are typically expressed as <a href="/facts/Monotonic/MjQK0YL2">monotonic</a> <a href="/facts/Idempotent/khbSpexv">idempotent</a> <a href="/facts/Predicate_transformer_semantics/bxK9TNh7">predicate transformers</a>.</li></ul>
<a href="/facts/Program_refinement/ehdFJQ9T">Program refinement</a> is an important concept in the UTP. A program 
 
 
 
 
 P
 
 1
 
 
 
 
 {\displaystyle P_{1}}
 
 is refined by 
 
 
 
 
 P
 
 2
 
 
 
 
 {\displaystyle P_{2}}
 
 if and only if every observation that can be made of 
 
 
 
 
 P
 
 2
 
 
 
 
 {\displaystyle P_{2}}
 
 is also an observation of 
 
 
 
 
 P
 
 1
 
 
 
 
 {\displaystyle P_{1}}
 
.
The definition of refinement is common across UTP theories:

 
 
 
 
 P
 
 1
 
 
 ⊑
 
 P
 
 2
 
 
 
 
 if and only if
 
 
 
 [
 
 
 P
 
 2
 
 
 ⇒
 
 P
 
 1
 
 
 
 ]
 
 
 
 {\displaystyle P_{1}\sqsubseteq P_{2}\quad {\text{if and only if}}\quad \left[P_{2}\Rightarrow P_{1}\right]}

where 
 
 
 
 
 [
 X
 ]
 
 
 
 {\displaystyle \left[X\right]}
 
 denotes<a class="footnote-ref" id="fnref:3" href="#fn:3">3</a> the <a href="/facts/Universal_closure/agNmvJKN">universal closure</a> of all variables in the alphabet.

<h2 id="relations">Relations</h2>
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:

<ul><li>undecorated variables (
 
 
 
 v
 
 
 {\displaystyle v}
 
), modelling an observation of the program at the start of its execution; and</li>
<li>primed variables (
 
 
 
 
 v
 ′
 
 
 
 {\displaystyle v'}
 
), modelling an observation of the program at a later stage of its execution.</li></ul>
Some common language constructs can be defined in the theory of relations as follows:

<ul><li>The skip statement, which does not alter the program state in any way, is modelled as the relational identity:</li></ul>

 
 
 
 
 s
 k
 i
 p
 
 ≡
 
 v
 ′
 
 =
 v
 
 
 {\displaystyle \mathbf {skip} \equiv v'=v}

<ul><li>The assignment of value 
 
 
 
 E
 
 
 {\displaystyle E}
 
 to a variable 
 
 
 
 a
 
 
 {\displaystyle a}
 
 is modelled as setting 
 
 
 
 
 a
 ′
 
 
 
 {\displaystyle a'}
 
 to 
 
 
 
 E
 
 
 {\displaystyle E}
 
 and keeping all other variables (denoted by 
 
 
 
 u
 
 
 {\displaystyle u}
 
) constant:</li></ul>

 
 
 
 a
 :=
 E
 ≡
 
 a
 ′
 
 =
 E
 ∧
 
 u
 ′
 
 =
 u
 
 
 {\displaystyle a:=E\equiv a'=E\land u'=u}

<ul><li>The <a href="/facts/Sequential_composition/RmAEJ2tN">sequential composition</a> of two programs is just <a href="/facts/Composition_of_relations/tD8joBlo">relational composition</a> of intermediate state:</li></ul>

 
 
 
 
 P
 
 1
 
 
 ;
 
 P
 
 2
 
 
 ≡
 ∃
 
 v
 
 0
 
 
 ∙
 
 P
 
 1
 
 
 [
 
 v
 
 0
 
 
 
 /
 
 
 v
 ′
 
 ]
 ∧
 
 P
 
 2
 
 
 [
 
 v
 
 0
 
 
 
 /
 
 v
 ]
 
 
 {\displaystyle P_{1};P_{2}\equiv \exists v_{0}\bullet P_{1}[v_{0}/v']\land P_{2}[v_{0}/v]}

<ul><li>Non-deterministic choice between programs is their greatest lower bound:</li></ul>

 
 
 
 
 P
 
 1
 
 
 ⊓
 
 P
 
 2
 
 
 ≡
 
 P
 
 1
 
 
 ∨
 
 P
 
 2
 
 
 
 
 {\displaystyle P_{1}\sqcap P_{2}\equiv P_{1}\lor P_{2}}

<ul><li><a href="/facts/Conditional_(programming)/8gDQTqUD">Conditional choice</a> between programs is written using infix notation:</li></ul>

 
 
 
 
 P
 
 1
 
 
 ◃
 C
 ▹
 
 P
 
 2
 
 
 ≡
 (
 C
 ∧
 
 P
 
 1
 
 
 )
 ∨
 (
 ¬
 C
 ∧
 
 P
 
 2
 
 
 )
 
 
 {\displaystyle P_{1}\triangleleft C\triangleright P_{2}\equiv (C\land P_{1})\lor (\lnot C\land P_{2})}

<ul><li>A semantics for <a href="/facts/Recursion/CxSKxJoW">recursion</a> is given by the <a href="/facts/Least_fixed_point/JbcBLqTN">least fixed point</a> 
 
 
 
 μ
 
 F
 
 
 
 {\displaystyle \mu \mathbf {F} }
 
 of a monotonic predicate transformer 
 
 
 
 
 F
 
 
 
 {\displaystyle \mathbf {F} }
 
:</li></ul>

 
 
 
 μ
 X
 ∙
 
 F
 
 (
 X
 )
 ≡
 ⊓
 
 {
 
 X
 ∣
 
 F
 
 (
 X
 )
 ⊑
 X
 
 }
 
 
 
 {\displaystyle \mu X\bullet \mathbf {F} (X)\equiv \sqcap \left\{X\mid \mathbf {F} (X)\sqsubseteq X\right\}}

<h2 id="further-reading">Further reading</h2>
<ul><li><a href="/facts/Jim_Woodcock/mkHY39YP">Woodcock, Jim</a>; Cavalcanti, Ana (2004). <a href="https://kar.kent.ac.uk/14036/1/A_Tutorial_Introduction_to_Designs_in.pdf">"A tutorial introduction to designs in Unifying Theories of Programming"</a> (PDF). Integrated Formal Methods. <a href="/facts/Lecture_Notes_in_Computer_Science/1UeA77BC">Lecture Notes in Computer Science</a>, pages. Vol. 2999. Springer. pp. 40–66. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2F978-3-540-24756-2_4">10.1007/978-3-540-24756-2_4</a>. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-3-540-21377-2.</li>
<li>Cavalcanti, Ana; Woodcock, Jim (2006). <a href="https://www.cs.york.ac.uk/ftpdir/pub/leo/utp/tutorials/utp-tutorial-CSP.pdf">"A tutorial introduction to CSP in Unifying Theories of Programming"</a> (PDF). Refinement Techniques in Software Engineering. Lecture Notes in Computer Science. Vol. 3167. Springer. pp. 220–268. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2F11889229_6">10.1007/11889229_6</a>. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-3-540-46253-8.</li></ul>
<h2 id="external-links">External links</h2>
<ul><li><a href="http://www.unifyingtheories.org/">UTP book website</a></li>
<li><a href="https://web.archive.org/web/20161007215026/http://unifyingtheories.org/">UTP book</a> on <a href="/facts/Archive.org/PHStU8Lo">Archive.org</a></li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1">Hoare, C. A. R.; Jifeng, He (April 1, 1998). Unifying Theories of Programming. Prentice Hall. p. 320. ISBN 978-0-13-458761-5. Retrieved 17 September 2014. <a href="978-0-13-458761-5" target="_blank">978-0-13-458761-5</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></li>
<li id="fn:2">Hoare, C.A.R. (April 1984). "Programming: Sorcery or science?". IEEE Software. 1 (2): 5–16. doi:10.1109/MS.1984.234042. S2CID 375578. <a href="/wiki/IEEE_Software" target="_blank">/wiki/IEEE_Software</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></li>
<li id="fn:3">Dijkstra, Edsger W.; Scholten, Carel S. (1990). Predicate calculus and program semantics. Texts and Monographs in Computer Science. Springer. ISBN 0-387-96957-8.
 <a href="0-387-96957-8" target="_blank">0-387-96957-8</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></li>
</ol>

Unifying Theories of Programming open-in-new

Unifying Theories of Programming