Unifying Theories of Programming: Difference between revisions

Revision as of 15:16, 22 September 2012

Revision as of 06:38, 16 October 2012

Line 39:

<math>a := E \equiv a' = E \land u' = u</math>

* The [[sequential composition]] of two programs is just [[http://en.wikipedia.org/wiki/Composition_of_relationsComposition 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>