Predicate transformer semantics is an extension of 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 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) on the state space of a program.

The canonical predicate transformer of sequential imperative programming is the so-called weakest precondition wp(S, R). 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:

: wp(x := E, R) = R_E^x

This gives a predicate that is a copy of R with the value of x replaced by E .

An example of a valid calculation of wp for assignments with integer valued variables x and y is:

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

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 guard (computing)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 setting by Ralph-Johan Back in the 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.

= References =