Predicate transformer semantics were introduced by Edsger Dijkstra in his seminal paper "Guarded commands, nondeterminacy and formal derivation of programs". They define the semantics of an imperative programming paradigm by assigning to each statement in this language a corresponding predicate transformer: a total function between two predicates on the state space of the statement. In this sense, predicate transformer semantics are a kind of denotational semantics. Actually, in guarded commands, Dijkstra uses only one kind of predicate transformer: the well-known weakest preconditions (see below). 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, { P } S { R } {\displaystyle \{P\}S\{R\}} if and only if P ⇒ Q {\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 { Q ′ } S { R } {\displaystyle \{Q'\}S\{R\}} so Q ′ ⇒ Q {\displaystyle Q'\Rightarrow Q} and { Q } S { R } {\displaystyle \{Q\}S\{R\}} so Q ⇒ Q ′ {\displaystyle Q\Rightarrow Q'} , and thus Q = Q ′ {\displaystyle Q=Q'} . We often use w p ( S , R ) {\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, R [ x ← E ] {\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:
w p ( x := x − 5 , x > 10 ) = x − 5 > 10 ⇔ x > 15 {\displaystyle {\begin{array}{rcl}wp(x:=x-5,x>10)&=&x-5>10\\&\Leftrightarrow &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,
… excerpt ends here. Continue reading the full article.
