Predicate transformer semantics: Difference between revisions

Revision as of 18:50, 6 October 2005

Revision as of 18:55, 6 October 2005

Line 1:

'''Predicate transformer semantics''' is an extension of [[Hoare_logic|Floyd-Hoare Logic]] invented by [[Dijkstra]] and extended and refined by other researchers. It was first introduced in Dijkstra's paper "Guarded commands, nondeterminacy and formal derivation of programs". It is a method for defining the semantics of an [[Imperative_programming|imperative programming]] language by assigning to each ''command'' in the language a corresponding ''predicate transformer''. A ''[[predicate transformer]]'' is a [[total function]] mapping between two ''[[assertion (computing)|predicates]]'' on the state space of a program.

The canonical ''predicate transformer'' of sequential imperative programming is the so-called "[[weakest pre-conditionprecondition]]" <math>wp(S, R)</math>. Here ''S'' denotes a list of ''commands'' and ''R'' denotes a predicate on the space, called the "[[post-conditionpostcondition]]". The result of applying this function gives the "weakest pre-condition" for ''S'' terminating with ''R'' true. An example is the following definition of the assignment statement:

:<math> wp(x := E, R) = R_E^x </math>

Line 15:

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 ''[[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 [[Ralph-JohnJohan Back|R.-J. Back]] in the [http://www.ecs.soton.ac.uk/~mjb/refcalc-tut/home.html [Refinement Calculus]].

Although the most common and most widely discussed because of their relevance to sequential programming, "weakest pre-conditions" are not the only ''predicate transformers''. For example, [[Leslie Lamport]] has suggested ''win'' and ''sin'' as ''predicate transformers'' for [[concurrent programming]].