Predicate transformer semantics

Moreover, predicate transformer semantics are a reformulation of Floyd–Hoare logic. Whereas Hoare logic is presented as a deductive system, predicate transformer semantics (either by weakest-preconditions or by strongest-postconditions see below) are complete strategies to build valid deductions of Hoare logic. In other words, they provide 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, or runs forward in the case of strongest-postconditions.

Weakest preconditions

Definition

For a statement S and a postcondition R, a weakest precondition is a predicate Q such that for any precondition P, ${\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 that R holds after S. Uniqueness follows easily from the definition: If both Q and Q' 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 statement S with respect to a postcondition R.

Conventions

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.

Skip

Abort

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 free occurrences of x are replaced by E. Hence, here, expression E is implicitly coerced into a valid term of the underlying logic: it is thus a pure expression, totally defined, terminating and without side effect.

• version 1:

• version 2:

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

The first version avoids a potential duplication of x in R, whereas the second version is simpler when there is at most a single occurrence of x in R. The first version also reveals 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 \begin{array}{rcl}wp(x:=x-5,x>10)& =& x-5>10\\ & \iff & x>15\end{array}}$

This means that, for the postcondition x > 10 to be true after the assignment, the precondition x > 15 must be true before the assignment. This is also the "weakest precondition", in that it is the "weakest" restriction on the value of x which makes x > 10 true after the assignment.

Sequence

For example,

${\displaystyle \begin{array}{rcl}wp(x:=x-5;x:=x\ast 2,x>20)& =& wp(x:=x-5,wp(x:=x\ast 2,x>20))\\ & =& wp(x:=x-5,x\ast 2>20)\\ & =& (x-5)\ast 2>20\\ & =& x>15\end{array}}$

Conditional

As example:

${\displaystyle \begin{array}{rcl}wp(\mathtt{\text{if}}x<y\mathtt{\text{then}}x:=y\mathtt{\text{else}}\mathtt{\text{skip}}\mathtt{\text{end}},x\ge y)& =& (x<y\Rightarrow wp(x:=y,x\ge y))\wedge (\mathrm{\neg }(x<y)\Rightarrow wp(\mathtt{\text{skip}},x\ge y))\\ & =& (x<y\Rightarrow y\ge y)\wedge (\mathrm{\neg }(x<y)\Rightarrow x\ge y)\\ & \iff & \mathtt{\text{true}}\end{array}}$

While loop

Partial correctness

Ignoring termination for a moment, we can define the rule for the weakest liberal precondition, denoted wlp, using a predicate INV, called the Loop INVariant, typically supplied by a programmer:

Total correctness

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

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. statement S) must preserve the invariant and reduce the variant;
• the last one means that the loop postcondition R must be established when the loop finishes.

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

Non-deterministic guarded commands

Actually, Dijkstra's Guarded 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.

The definitions of weakest-precondition given above (in particular for while-loop) preserve this property.

Selection

Selection is a generalization of if statement:

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

Repetition is a generalization of while statement in a similar way.

Specification statement

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

<span class="mwe-math-element mwe-math-element-inline" typeof="mw:Extension/math" about="#mwt48" data-mw='{"name":"math","attrs":{},"body":{"extsrc":" x:l[pre, post] "}}' id="mwzg"><span class="mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" class="mathjax_ignore" alttext="{\displaystyle x:l[pre,post]}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>:</mo> <mi>l</mi> <mo stretchy="false">[</mo> <mi>p</mi> <mi>r</mi> <mi>e</mi> <mo>,</mo> <mi>p</mi> <mi>o</mi> <mi>s</mi> <mi>t</mi> <mo stretchy="false">]</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x:l[pre,post]}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/0047410e927d5b20c3135661e45feba120e7ef95" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:13.816ex; height:2.843ex;" alt="{\displaystyle x:l[pre,post]}"/></span>

which specifies a computation that starts in a state satisfying pre and is guaranteed to end in a state satisfying post by changing only x. 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

<span class="mwe-math-element mwe-math-element-inline" typeof="mw:Extension/math" about="#mwt50" data-mw='{"name":"math","attrs":{},"body":{"extsrc":" x:l[x = l, x = l+1] "}}' id="mw1Q"><span class="mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" class="mathjax_ignore" alttext="{\displaystyle x:l[x=l,x=l+1]}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>:</mo> <mi>l</mi> <mo stretchy="false">[</mo> <mi>x</mi> <mo>=</mo> <mi>l</mi> <mo>,</mo> <mi>x</mi> <mo>=</mo> <mi>l</mi> <mo>+</mo> <mn>1</mn> <mo stretchy="false">]</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x:l[x=l,x=l+1]}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ffd2b07a04dfcae9395e4c05a9823e36e45d7af3" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:20.533ex; height:2.843ex;" alt="{\displaystyle x:l[x=l,x=l+1]}"/></span>

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

<span class="mwe-math-element mwe-math-element-inline" typeof="mw:Extension/math" about="#mwt51" data-mw='{"name":"math","attrs":{},"body":{"extsrc":" x:l[x = l^2, x = l] "}}' id="mw2A"><span class="mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" class="mathjax_ignore" alttext="{\displaystyle x:l[x=l^{2},x=l]}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>:</mo> <mi>l</mi> <mo stretchy="false">[</mo> <mi>x</mi> <mo>=</mo> <msup> <mi>l</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>2</mn> </mrow> </msup> <mo>,</mo> <mi>x</mi> <mo>=</mo> <mi>l</mi> <mo stretchy="false">]</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x:l[x=l^{2},x=l]}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7c9231bf8b7395e4acd035ef28a6753fa5584dfd" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:17.585ex; height:3.176ex;" alt="{\displaystyle x:l[x=l^{2},x=l]}"/></span>

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

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

Goto statement

Formalization of jump statements like goto 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 that goto 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

For goto L execution transfers control to label L at which the weakest precondition must hold. The way that wpL is referred to in the rule should not be taken as a big surprise. It is only ⁠${\displaystyle wp(L:S,Q)}$⁠ for some Q computed to that point. This is like any wp rules, using constituent statements to give wp definitions, even though goto L appears a primitive. The rule does not require the uniqueness for locations where wpL 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).