Predicate transformer semantics

Predicate transformer semantics is an extension of Floyd–Hoare logic introduced by Dijkstra in its seminal 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 predicates on the state space of a program. Actually, in Guarded commands, Dijkstra uses only one kind of predicate transformers: the well-known weakest precondition (see below).

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 an " algebraic style". This style was advocated by Dijkstra and others, and also developed further in a higher order logic setting by R.-J. Back in the Refinement Calculus. It has been mechanized in B-Method.

Examples of predicate transformers

Weakest precondition

The canonical predicate transformer of sequential imperative programming is the so-called "weakest precondition" ${\displaystyle 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" on the initial state for S terminating with R satisfied on the final state. An example is the following definition of the assignment statement:

${\displaystyle wp(x:=E,R)\ =\ R[x\leftarrow E]}$ 

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:

${\displaystyle wp(x:=x-5,x>10)\ =\ (x-5>10)\ =\ (x>15)}$ 

This means that in order for the "post-condition" x > 10 to be true after the assignment, the "pre-condition" x > 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 x which makes x > 10 true after the assignment.

Weakest liberal precondition

An important variant of the weakest precondition is the weakest liberal precondition ${\displaystyle wlp(S,R)}$ , which yields the weakest condition under which S either does not terminate or establishes R. It therefore differs from wp in not guaranteeing termination.

Strongest postcondition

Given S a statement (or in other words, a list of commands) and R a precondition (a predicate on the initial state), then ${\displaystyle sp(S,R)}$  is the strongest-postcondition: it implies any postcondition satisfied by the final state of the execution of S, for any initial state statisfying R. For example, on assignment we have:

${\displaystyle sp(x:=E,R)\ =\ \exists y,R[x\leftarrow y]\wedge x=E[x\leftarrow y]}$ 

The logical variable ${\displaystyle y}$  above represents the initial value of variable ${\displaystyle x}$ . Hence,

${\displaystyle sp(x:=x-5,x>15)\ =\ \exists y,y>15\wedge x=y-5\ =\ x>10}$ 

Others

Leslie Lamport has suggested win and sin as predicate transformers for concurrent programming.

Links with Guarded commands

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.

See also

• Axiomatic semantics — includes predicate transformer semantics
• Formal semantics of programming languages — an overview
• Hoare logic — the best-known axiomatic semantics
• Refinement calculus, an extension of Hoare logic exploiting the lattice structure of predicate transformers (for "refinement" order).
• Dynamic logic, where predicate transformers appear as modalities (in the sense of Modal logic).

References

• Ralph-Johan Back and Joakim von Wright, Refinement Calculus: A Systematic Introduction, 1st edition, 1998. ISBN 0-387-98417-8.
• Marcello M. Bonsangue and Joost N. Kok, The weakest precondition calculus: Recursion and duality, Formal Aspects of Computing, 6(6):788–800, November 1994. DOI 10.1007/BF01213603.
• Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of program. Communications of the ACM, 18(8):453–457, August 1975. [1]
• Edsger W. Dijkstra. A Discipline of Programming. ISBN 0-613-92411-8. — A systematic introduction to a version of the guarded command language with many worked examples
• Edsger W. Dijkstra and Carel S. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag 1990 ISBN 0-387-96957-8 — A more abstract, formal and definitive treatment
• David Gries. The Science of Programming. Springer-Verlag 1981 ISBN 0-387-96480-0
• Leslie Lamport, "win and sin: Predicate Transformers for Concurrency". ACM Transactions on Programming Languages and Systems, 12(3), July 1990. [2]