Predicate transformer semantics: Difference between revisions

Revision as of 20:27, 15 August 2005

Revision as of 18:49, 9 September 2005

Line 13:

This means that in order for the "post-condition" ''x > 10'' to be true after the assignment, the "pre-condition" ''y > 15'' must be true before the assignment. This is also the "weakest pre-condition", in that it is the "weakest" restriction on the value of ''y'' which makes ''x > 10'' true after the assignment.

Dijkstra also defined alternative ('''if''') and repetitive ('''do''') constructs as well as a composition operator (''';''') using ''wp''. The alternative and repetitive constructs used ''[[guarded commands]]'' to influence execution. Because of the rules he imposed on the definition of ''wp'', both constructs allow for non-deterministic execution if the ''guards[[guard (computing)|guard]]s'' in the commands are non disjoint.

Unlike many other semantic formalisms, predicate transformer semantics was not designed as an investigation into foundations of computation. Rather, it is intended to provide programmers with a methodology to develop their programs as "correct by construction" in a "calculational style". This style was advocated by Dijkstra and others, and also developed further in a [[Higher-order_logic|higher order logic]] setting by R.J Back in the [http://www.ecs.soton.ac.uk/~mjb/refcalc-tut/home.html Refinement Calculus].