Predicate transformer semantics: Difference between revisions

Revision as of 23:25, 4 February 2007

Revision as of 23:26, 4 February 2007

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 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:

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