Unifying Theories of Programming: Difference between revisions

Revision as of 15:10, 5 December 2016

Revision as of 23:06, 3 July 2017

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>[[Edsger W. Dijkstra]] and [[Carel S. Scholten]]. Predicate calculus and program semantics. Texts and Monographs in Computer Science. Springer-Verlag New York, Inc., New York, NY, USA, 1990. {{ISBN |0-387-96957-8}}.</ref> the [[universal closure]] of all variables in the alphabet.

==Relations==

Line 57:

==Further reading==

* [[Jim Woodcock]] and Ana Cavalcanti. A tutorial introduction to designs in Unifying Theories of Programming. In ''Integrated Formal Methods'', volume 2999 of [[Lecture Notes in Computer Science]], pages 40–66. [[Springer-Verlag|Springer]] Berlin / Heidelberg, 2004. {{ISBN |978-3-540-21377-2}}. {{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]

* Ana Cavalcanti and Jim Woodcock. A tutorial introduction to CSP in Unifying Theories of Programming. In ''Refinement Techniques in Software Engineering'', volume 3167 of Lecture Notes in Computer Science, pages 220–268. Springer Berlin / Heidelberg, 2006. {{DOI|10.1007/11889229_6}} {{citeseerx|10.1.1.97.3469}} [https://www.cs.york.ac.uk/ftpdir/pub/leo/utp/tutorials/utp-tutorial-CSP.pdf paper]