Predicate transformer semantics

Predicate transformer semantics have been introduced by Dijkstra in its seminal paper "Guarded commands, nondeterminacy and formal derivation of programs". They define the semantics of an imperative programming language by assigning to each statement in this language a corresponding predicate transformer: a total function mapping between two predicates on the state space of the statement. Actually, in Guarded commands, Dijkstra uses only one kind of predicate transformers: the well-known weakest preconditions (see below).

Predicate transformer semantics are a reformulation of Floyd–Hoare logic. Whereas 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 of verifying a Hoare triple to the problem of proving a first-order formula. Technically, predicate transformer semantics perform a kind of Symbolic execution of statements into predicates (execution runs backward in the case of weakest-preconditions, and runs forward in the case of strongest-postconditions).

Weakest preconditions

Definition

Given S a statement, the weakest-precondition of S is a function mapping any postcondition R (R denotes thus a predicate on the space of states) to a precondition. Actually, the result of this function, denoted ${\displaystyle wp(S,R)}$ , is the "weakest" precondition on the initial state ensuring that execution of S terminates in a final state satisfying R. More formally, a given Hoare triple ${\displaystyle \{P\}S\{Q\}}$  is provable in Hoare logic for total correctness iff the first-order predicate below is universally valid (e.g. for all possible values of the space of states):

${\displaystyle P\Rightarrow wp(S,Q)}$ 

Formally, weakest-preconditions are defined recursively over the abstract syntax of statements. Actually, weakest-precondition semantics is a Continuation-passing style semantics of state transformers where the predicate in argument is a continuation.

Skip

${\displaystyle wp({\textbf {skip}},R)\ =\ R}$ 

Abort

 ${\displaystyle wp({\textbf {abort}},R)\ =\ {\textbf {false}}}$ 

Assignment

We give below two equivalent weakest-preconditions for 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 (representing the final value of variable x). 

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

Sequence

 ${\displaystyle wp(S_{1};S_{2},R)\ =\ wp(S_{1},wp(S_{2},R))}$ 

As example:

${\displaystyle wp(x:=x-5;x:=x*2\ ,\ x>20)\ =\ wp(x:=x-5,wp(x:=x*2,x>20))\ =\ wp(x:=x-5,x*2>20)\ =\ (x-5)*2>20}$ 

Conditional

 ${\displaystyle wp({\textbf {if}}\ E\ {\textbf {then}}\ S_{1}\ {\textbf {else}}\ S_{2}\ {\textbf {endif}},R)\ =\ (E\Rightarrow wp(S_{1},R))\wedge (\neg E\Rightarrow wp(S_{2},R))}$  

As example:

${\displaystyle wp({\textbf {if}}\ x<y\ {\textbf {then}}\ x:=y\ {\textbf {else}}\ {\textbf {skip}}\ {\textbf {endif}},\ x\geq y)\ =\ (x<y\Rightarrow wp(x:=y,x\geq y))\wedge (\neg x<y\Rightarrow x\geq y)\ =\ (x<y\Rightarrow y\geq y)\ =\ {\textbf {true}}}$ 

Weakest-preconditions of 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.

Other examples of predicate transformers

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. Hence it corresponds to Hoare logic in partial correctness.

Strongest postcondition

Given S a statement and R a precondition (a predicate on the initial state), then ${\displaystyle sp(S,R)}$  is their strongest-postcondition: it implies any postcondition satisfied by the final state of any execution of S, for any initial state statisfying R. In other words, a Hoare triple ${\displaystyle \{P\}S\{Q\}}$  is provable in Hoare logic iff the predicate below is universally satisfiable:

 ${\displaystyle sp(S,P)\Rightarrow Q}$ 

Hence, if we denote ${\displaystyle {\vec {x}}}$  the set of variables occurring free in predicates P and Q, and if S is a statement of state space ${\displaystyle {\vec {x}}}$ , we have the following relation between weakest-preconditions and strongest-preconditions:

 ${\displaystyle (\forall {\vec {x}},P\Rightarrow wp(S,Q))\ \Leftrightarrow \ (\forall {\vec {x}},sp(S,P)\Rightarrow Q)}$ 

For example, on assignment we have:

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

Above, the logical variable y represents the initial value of variable x. Hence,

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

Win and sin predicate transformers

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 statically 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.

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 guarded commands (and 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]