Predicate transformer semantics: Difference between revisions

Revision as of 23:38, 26 January 2007

Revision as of 16:10, 4 February 2007

Line 1:

'''Predicate transformer semantics''' is an extension of [[Hoare_logicHoare 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 precondition]]" <math>wp(S, R)</math>. Here ''S'' denotes a list of ''commands'' and ''R'' denotes a predicate on the space, called the "[[postcondition]]". 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:

Line 22:

* [[Edsger W. Dijkstra]], "Guarded commands, nondeterminacy and formal derivation of programs". ''[[Communications of the ACM]]'', 18(8):453&ndash;457, August 1975. [http://doi.acm.org/10.1145/360933.360975]

* [[Leslie Lamport]], "''win'' and ''sin'': Predicate Transformers for Concurrency". ''[[Association for Computing Machinery|ACM]] Transactions on Programming Languages and Systems'', 12(3), July 1990. [http://research.microsoft.com/users/lamport/pubs/pubs.html#lamport-win]

* [[Ralph-Johan Back]] and Joakim von Wright, ''Refinement Calculus: A Systematic Introduction'', 1st edition, 1998. ISBN 0-387-98417-8.

* Edsger W. Dijkstra. ''A Discipline of Programming'' (A systematic introduction with examples). ISBN 0-613-92411-8.