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.
Actually, in guarded commands, Dijkstra uses only one kind of predicate transformer: the well-known weakest preconditions (see below).
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.
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.
Such a promotion is carried out often casually, so people tend to take T as true and F as false.
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.
For example, As example: 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 the programmer: 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: where v is a fresh tuple of variables Informally, in the above conjunction of three formulas: However, the conjunction of those three is not a necessary condition.
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.
Refinement calculus extends GCL with the notion of specification statement.
Syntactically, we prefer to write a specification statement as 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.
[1] The very advantage of this is its capability of defining wp of goto L and other jump statements.
[2] Formalization of jump statements like goto L takes a very long bumpy process.
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.
This actually justifies that we could place the same labels at the same location multiple times, as
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.
Hence it corresponds to Hoare logic in partial correctness: for the statement language given above, wlp differs with wp only on while-loop, in not requiring a variant (see above).
is provable in Hoare logic if and only if the predicate below hold: Usually, strongest-postconditions are used in partial correctness.
Hence, On sequence, it appears that sp runs forward (whereas wp runs backward): Leslie Lamport has suggested win and sin as predicate transformers for concurrent programming.
Predicate transformers of interest (wp, wlp, and sp) are monotonic.
A predicate transformer S is monotonic if and only if: This property is related to the consequence rule of Hoare logic.
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.
It turns out that all jump statements are executable miracles,[5] i.e. they can be implemented but not strict.
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 (like division by zero).
There are many proposals to extend weakest-preconditions or strongest-postconditions for imperative expression languages and in particular for monads.
Indeed, such programs have many applications in cryptography (hiding of information using some randomized noise), distributed systems (symmetry breaking).