Predicate transformer semantics

Predicate transformer semantics is a reformulation of Floyd–Hoare logic. While Hoare logic was originally presented as a deductive system, predicate transformer semantics (either by weakest-preconditions or by strongest-postconditions see below) give an effective algorithm to reduce the problem verifying a Hoare triple to the problem of proving a first-order formula.

Predicate transformer semantics has been 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 preconditions (see below).

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. As an example, we give below to equivalent definition of the assignment statement (in these formulas, ${\displaystyle R[x\leftarrow E]}$  is a copy of R where fresh occurrences of x are replaced by E):

• version 1:

 ${\displaystyle wp(x:=E,R)\ =\ \forall y,y=E\Rightarrow R[y\leftarrow x]\ }$  where y is a fresh variable. 

• version 2:

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

The first version avoids a potential duplication of E in R, whereas the second version is simpler when there is at most a single occurrence of x in E. The first version reveals also a deep duality between weakest-precondition and strongest-postcondition (see below).

An example of a valid calculation of wp (using version 2) for assignments with integer valued variable x 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,x=E[x\leftarrow y]\wedge R[x\leftarrow y]}$  where ${\displaystyle y}$  is fresh.

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

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

Others

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

Applications

• 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 "calculation 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.

• Computations of weakest-preconditions are used to check assertions in programs using a theorem-prover (like SMT-solvers or proof assistants): see Frama-C or ESC/Java2.

• In the meta-theory of Hoare logic, weakest-preconditions are a key notion in the proof of relative completness.

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]