Unifying Theories of Programming: Difference between revisions

Revision as of 07:48, 10 August 2015

Revision as of 10:50, 14 February 2016

Line 6:

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>

In UTP parlance, a ''theory'' is a model of a particular programming paradigm. A UTP theory is composed of three ingredients:

Line 45:

<math>P_1 \sqcap P_2 \equiv P_1 \lor P_2</math>

* [[Conditional_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>