Predicate transformer semantics were introduced byEdsger Dijkstra in his seminal paper "Guarded commands, nondeterminacy and formal derivation of programs". They define the semantics of animperative programming paradigm by assigning to eachstatement in this language a correspondingpredicate transformer: atotal function between twopredicates on the state space of the statement. In this sense, predicate transformer semantics are a kind ofdenotational semantics. Actually, inguarded commands, Dijkstra uses only one kind of predicate transformer: the well-knownweakest preconditions (see below).

Moreover, predicate transformer semantics are a reformulation ofFloyd–Hoare logic. Whereas Hoare logic is presented as adeductive system, predicate transformer semantics (either byweakest-preconditions or bystrongest-postconditions see below) arecomplete strategies to buildvalid deductions of Hoare logic. In other words, they provide an effectivealgorithm to reduce the problem of verifying a Hoare triple to the problem of proving afirst-order formula. Technically, predicate transformer semantics perform a kind ofsymbolic execution of statements into predicates: execution runsbackward in the case of weakest-preconditions, or runsforward in the case of strongest-postconditions.

For a statementS and apostconditionR, aweakest precondition is a predicateQ such that for anypreconditionP,${\displaystyle \{P\}S\{R\}}$ if and only if${\displaystyle P\Rightarrow Q}$. In other words, it is the "loosest" or least restrictive requirement needed to guarantee thatR holds afterS. Uniqueness follows easily from the definition: If bothQ andQ' are weakest preconditions, then by the definition${\displaystyle \{Q^{\prime }\}S\{R\}}$ so${\displaystyle Q^{\prime }\Rightarrow Q}$ and${\displaystyle \{Q\}S\{R\}}$ so${\displaystyle Q\Rightarrow Q^{\prime }}$, and thus${\displaystyle Q=Q^{\prime }}$. We often use${\displaystyle wp(S,R)}$ to denote the weakest precondition for statementS with respect to a postconditionR.

We use T to denote the predicate that is everywhere true and F to denote the one that is everywhere false. We shouldn't at least conceptually confuse ourselves with a Boolean expression defined by some language syntax, which might also contain true and false as Boolean scalars. For such scalars we need to do a type coercion such that we have T = predicate(true) and F = predicate(false). Such a promotion is carried out often casually, so people tend to take T as true and F as false.

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

${\displaystyle wp(\mathtt{\text{abort}},R)=\mathtt{\text{F}}}$

We give below two equivalent weakest-preconditions for the assignment statement. In these formulas,${\displaystyle R[x\leftarrow E]}$ is a copy ofR wherefree occurrences ofx are replaced byE. Hence, here, expressionE is implicitly coerced into avalid term of the underlying logic: it is thus apure expression, totally defined, terminating and without side effect.

• version 1:

${\displaystyle wp(x:=E,R)=(\mathrm{\forall }y.y=E\Rightarrow R[x\leftarrow y])}$ wherey is a fresh variable and not free in E and R (representing the final value of variablex)

• version 2:

Provided that E is well defined, we just apply the so-calledone-point rule on version 1. Then

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

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

An example of a valid calculation ofwp (using version 2) for assignments with integer valued variablex is:

This means that in order for the postconditionx > 10 to be true after the assignment, the preconditionx > 15 must be true before the assignment. This is also the "weakest precondition", in that it is the "weakest" restriction on the value ofx which makesx > 10 true after the assignment.

${\displaystyle wp(S_1;S_2,R)=wp(S_1,wp(S_2,R))}$

For example,

${\displaystyle wp(\mathtt{\text{if}}E\mathtt{\text{then}}{S}_1\mathtt{\text{else}}{S}_2\mathtt{\text{end}},R)=(E\Rightarrow wp(S_1,R))\wedge (\mathrm{\neg }E\Rightarrow wp(S_2,R))}$

As example:

Ignoring termination for a moment, we can define the rule for theweakest liberal precondition, denotedwlp, using a predicateINV, called theLoopINVariant, typically supplied by the programmer:

${\displaystyle wlp(\mathtt{\text{while}}E\mathtt{\text{do}}S\mathtt{\text{done}},R)\Leftarrow \mathit{\text{INV}}\text{if}\begin{array}{l}\\ (E\wedge \mathit{\text{INV}}\Rightarrow wlp(S,\mathit{\text{INV}}))\\ \wedge (\mathrm{\neg }E\wedge \mathit{\text{INV}}\Rightarrow R)\end{array}}$

To show total correctness, we also have to show that the loop terminates. For this we define awell-founded relation on the state space denoted as (wfs, <) and define a variant functionvf , such that we have:

wherev is a fresh tuple of variables

Informally, in the above conjunction of three formulas:

• the first one means that the variant must be part of the well-founded relation before entering the loop;
• the second one means that the body of the loop (i.e. statementS) must preserve the invariant and reduce the variant;
• the last one means that the loop postconditionR must be established when the loop finishes.

However, the conjunction of those three is not a necessary condition. Exactly, we have

${\displaystyle wp(\mathtt{\text{while}}E\mathtt{\text{do}}S\mathtt{\text{done}},R)=\text{the strongest solution of the recursive equation}\begin{array}{l}Z:[Z\equiv (E\wedge wp(S,Z))\vee (\mathrm{\neg }E\wedge R)]\end{array}}$

Actually, Dijkstra'sGuarded Command Language (GCL) is an extension of the simple imperative language given until here with non-deterministic statements. Indeed, GCL aims to be a formal notation to define algorithms. Non-deterministic statements represent choices left to the actual implementation (in an effective programming language): properties proved on non-deterministic statements are ensured for all possible choices of implementation. In other words, weakest-preconditions of non-deterministic statements ensure

• that there exists a terminating execution (e.g. there exists an implementation),
• and, that the final state of all terminating execution satisfies the postcondition.

Notice that the definitions of weakest-precondition given above (in particular forwhile-loop) preserve this property.

Selection is a generalization ofif statement:

${\displaystyle wp(\mathtt{\text{if}}{E}_1\to S_1[]\dots []E_n\to S_n\mathtt{\text{fi}},R)=\begin{array}{l}(E_1\vee \dots \vee E_n)\\ \wedge (E_1\Rightarrow wp(S_1,R))\\ \dots \\ \wedge (E_n\Rightarrow wp(S_n,R))\end{array}}$

^{[citation needed]}

Here, when two guards${\displaystyle E_i}$ and${\displaystyle E_j}$ are simultaneously true, then execution of this statement can run any of the associated statement${\displaystyle S_i}$ or${\displaystyle S_j}$.

Repetition is a generalization ofwhile statement in a similar way.

Refinement calculus extends GCL with the notion ofspecification statement. Syntactically, we prefer to write a specification statement as

${\displaystyle x:l[pre,post]}$

which specifies a computation that starts in a state satisfyingpre and is guaranteed to end in a state satisfyingpostby changing onlyx. We call${\displaystyle l}$ a logical constant employed to aid in a specification. For example, we can specify a computation that increment x by 1 as

${\displaystyle x:l[x=l,x=l+1]}$

Another example is a computation of a square root of an integer.

${\displaystyle x:l[x=l^2,x=l]}$

The specification statement appears like a primitive in the sense that it does not contain other statements. However, it is very expressive, aspre andpost are arbitrary predicates. Its weakest precondition is as follows.

${\displaystyle wp(x:l[pre,post],R)=(\mathrm{\exists }l::pre)\wedge (\mathrm{\forall }s:(\mathrm{\forall }l:pre:post(x\leftarrow s)):R(x\leftarrow s))}$ wheres is fresh.

It combines Morgan's syntactic idea with the sharpness idea by Bijlsma, Matthews and Wiltink.^[1] The very advantage of this is its capability of defining wp of goto L and other jump statements.^[2]

Formalization of jump statements likegoto L takes a very long bumpy process. A common belief seems to indicate the goto statement could only be argued operationally. This is probably due to a failure to recognize thatgoto L is actually miraculous (i.e. non-strict) and does not follow Dijkstra's coined Law of Miracle Excluded, as stood in itself. But it enjoys an extremely simple operational view from the weakest precondition perspective, which was unexpected. We define

${\displaystyle wp(\mathtt{\text{goto}}L,R)=wpL}$ wherewpL is the weakest precondition at labelL.

Forgoto L execution transfers control to labelL at which the weakest precondition has to hold. The way thatwpL is referred to in the rule should not be taken as a big surprise. It is just⁠${\displaystyle wp(L:S,Q)}$⁠ for someQ computed to that point. This is like any wp rules, using constituent statements to give wp definitions, even thoughgoto L appears a primitive. The rule does not require the uniqueness for locations wherewpL holds within a program, so theoretically it allows the same label to appear in multiple locations as long as the weakest precondition at each location is the same wpL. The goto statement can jump to any of such locations. This actually justifies that we could place the same labels at the same location multiple times, as⁠${\displaystyle S(L:L:S1)}$⁠, which is the same as⁠${\displaystyle S(L:S1)}$⁠. Also, it does not imply any scoping rule, thus allowing a jump into a loop body, for example. Let us calculate wp of the following program S, which has a jump into the loop body.

     wp(do x > 0 → L: x := x-1 od;  if x < 0 → x := -x; goto L ⫿ x ≥ 0 → skip fi,  post)   =   { sequential composition and alternation rules }     wp(do x > 0 → L: x := x-1 od, (x<0 ∧ wp(x := -x; goto L, post)) ∨ (x ≥  0 ∧ post)   =   { sequential composition, goto, assignment rules }     wp(do x > 0 → L: x := x-1 od, x<0 ∧ wpL(x ← -x) ∨ x≥0 ∧ post)   =   { repetition rule }     the strongest solution of               Z: [ Z ≡ x > 0 ∧ wp(L: x := x-1, Z) ∨ x < 0 ∧ wpL(x ← -x) ∨ x=0 ∧ post ]       =  { assignment rule, found wpL = Z(x ← x-1) }     the strongest solution of               Z: [ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← x-1) (x ← -x) ∨ x=0 ∧ post]   =  { substitution }     the strongest solution of               Z:[ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← -x-1) ∨ x=0 ∧ post ]   =  { solve the equation by approximation }     post(x ← 0)

Therefore,

wp(S, post) = post(x ← 0).

An important variant of the weakest precondition is theweakest liberal precondition${\displaystyle wlp(S,R)}$, which yields the weakest condition under whichS either does not terminate or establishesR. It therefore differs fromwp in not guaranteeing termination. Hence it corresponds toHoare logic in partial correctness: for the statement language given above,wlp differs withwp only onwhile-loop, in not requiring a variant (see above).

GivenS a statement andR aprecondition (a predicate on the initial state), then${\displaystyle sp(S,R)}$ is theirstrongest-postcondition: it implies any postcondition satisfied by the final state of any execution of S, for any initial state satisfying R. In other words, a Hoare triple${\displaystyle \{P\}S\{Q\}}$ is provable in Hoare logic if and only if the predicate below hold:

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

Usually,strongest-postconditions are used in partial correctness.Hence, we have the following relation between weakest-liberal-preconditions and strongest-postconditions:

${\displaystyle (\mathrm{\forall }x,P\Rightarrow wlp(S,Q))\iff (\mathrm{\forall }x,sp(S,P)\Rightarrow Q)}$

For example, on assignment we have:

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

Above, the logical variabley represents the initial value of variablex.Hence,

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

On sequence, it appears thatsp runs forward (whereaswp runs backward):

${\displaystyle sp(S_1;S_2,R)=sp(S_2,sp(S_1,R))}$

Leslie Lamport has suggestedwin andsin aspredicate transformers forconcurrent programming.^[3]

This section presents some characteristic properties of predicate transformers.^[4] Below,S denotes a predicate transformer (a function between two predicates on the state space) andP a predicate. For instance,S(P) may denotewp(S,P) orsp(S,P). We keepx as the variable of the state space.

Predicate transformers of interest (wp,wlp, andsp) aremonotonic. A predicate transformerS ismonotonic if and only if:

${\displaystyle (\mathrm{\forall }x:P:Q)\Rightarrow (\mathrm{\forall }x:S(P):S(Q))}$

This property is related to theconsequence rule of Hoare logic.

A predicate transformerS isstrict iff:

${\displaystyle S(\mathtt{\text{F}})\iff \mathtt{\text{F}}}$

For instance,wp is artificially made strict, whereaswlp is generally not. In particular, if statementS may not terminate then${\displaystyle wlp(S,\mathtt{\text{F}})}$ is satisfiable. We have

${\displaystyle wlp(\mathtt{\text{while}}\mathtt{\text{true}}\mathtt{\text{do}}\mathtt{\text{skip}}\mathtt{\text{done}},\mathtt{\text{F}})\iff \mathtt{\text{T}}}$

Indeed,T is a valid invariant of that loop.

The non-strict but monotonic or conjunctive predicate transformers are called miraculous and can also be used to define a class of programming constructs, in particular, jump statements, which Dijkstra cared less about. Those jump statements include straight goto L, break and continue in a loop and return statements in a procedure body, exception handling, etc. It turns out that all jump statements are executable miracles,^[5] i.e. they can be implemented but not strict.

A predicate transformerS isterminating if:

${\displaystyle S(\mathtt{\text{T}})\iff \mathtt{\text{T}}}$

Actually, this terminology makes sense only for strict predicate transformers: indeed,${\displaystyle wp(S,\mathtt{\text{T}})}$ is the weakest-precondition ensuring termination ofS.

It seems that naming this propertynon-aborting would be more appropriate: in total correctness, non-termination is abortion, whereas in partial correctness, it is not.

A predicate transformerS isconjunctive iff:

${\displaystyle S(P\wedge Q)\iff S(P)\wedge S(Q)}$

This is the case for${\displaystyle wp(S,.)}$, even if statementS is non-deterministic as a selection statement or a specification statement.

A predicate transformerS isdisjunctive iff:

${\displaystyle S(P\vee Q)\iff S(P)\vee S(Q)}$

This is generally not the case of${\displaystyle wp(S,.)}$ whenS is non-deterministic. Indeed, consider a non-deterministic statementS choosing an arbitrary Boolean. This statement is given here as the followingselection statement:

${\displaystyle S=\mathtt{\text{if}}\mathtt{\text{true}}\to x:=0[]\mathtt{\text{true}}\to x:=1\mathtt{\text{fi}}}$

Then,${\displaystyle wp(S,R)}$ reduces to the formula${\displaystyle R[x\leftarrow 0]\wedge R[x\leftarrow 1]}$.

Hence,${\displaystyle wp(S,x=0\vee x=1)}$ reduces to thetautology${\displaystyle (0=0\vee 0=1)\wedge (1=0\vee 1=1)}$

Whereas, the formula${\displaystyle wp(S,x=0)\vee wp(S,x=1)}$reduces to thewrong proposition${\displaystyle (0=0\wedge 1=0)\vee (1=0\wedge 1=1)}$.

• Computations of weakest-preconditions are largely used to statically checkassertions in programs using a theorem-prover (likeSMT-solvers orproof assistants): seeFrama-C orESC/Java2.
• Unlike many other semantic formalisms, predicate transformer semantics was not designed as an investigation into foundations of computation. Rather, it was intended to provide programmers with a methodology to develop their programs as "correct by construction" in a "calculation style". This "top-down" style was advocated by Dijkstra^[6] andN. Wirth.^[7] It has been formalized further byR.-J. Back and others in therefinement calculus. Some tools likeB-Method now provideautomated reasoning in order to promote this methodology.
• In the meta-theory ofHoare logic, weakest-preconditions appear as a key notion in the proof ofrelative completeness.^[8]

In predicate transformers semantics, expressions are restricted to terms of the logic (see above). However, this restriction seems too strong for most existing programming languages, where expressions may have side effects (call to a function having a side effect), may not terminate or abort (likedivision by zero). There are many proposals to extend weakest-preconditions or strongest-postconditions for imperative expression languages and in particular formonads.

Among them,Hoare Type Theory combinesHoare logic for aHaskell-like language,separation logic andtype theory.^[9]This system is currently implemented as aRocq library calledYnot.^[10] In this language,evaluation of expressions corresponds to computations ofstrongest-postconditions.

Probabilistic Predicate Transformers are an extension of predicate transformers forprobabilistic programs.Indeed, such programs have many applications incryptography (hiding of information using some randomized noise),distributed systems (symmetry breaking).^[11]

• Axiomatic semantics — includes predicate transformer semantics
• Dynamic logic — where predicate transformers appear as modalities
• Formal semantics of programming languages — an overview

• Formal methods
• Program logic
• Edsger W. Dijkstra

• Articles with short description
• Short description matches Wikidata
• All articles with unsourced statements
• Articles with unsourced statements from November 2021