Predicate transformer semantics: Difference between revisions

Revision as of 19:20, 1 February 2005

Revision as of 19:28, 1 February 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|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-condition" <math>wp(S, R)</math>. Here ''S'' denotes a list of ''commands'' and ''R'' denotes a predicate on the space, called the "post-condition". 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 asignment statment:

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

Line 11:

:<math>wp(x := y - 5, x > 10) = (y - 5 > 10) = (y > 15) </math>

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'' in the commands are non disjoint.