Semantics  



Semantics of programming languages  


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 wellknown 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 weakestpreconditions or by strongestpostconditions 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 firstorder formula. Technically, predicate transformer semantics perform a kind of symbolic execution of statements into predicates: execution runs backward in the case of weakestpreconditions, or runs forward in the case of strongestpostconditions.
For a statement S and a postcondition R, a weakest precondition is a predicate Q such that for any precondition P, if and only if . 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 so and so , and thus . We often use to denote the weakest precondition for statement S with respect to a postcondition R.
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.
We give below two equivalent weakestpreconditions for the assignment statement. In these formulas, 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.
where y is a fresh variable and not free in E and R (representing the final value of variable x) 
Provided that E is well defined, we just apply the socalled onepoint 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 weakestprecondition and strongestpostcondition (see below).
An example of a valid calculation of wp (using version 2) for assignments with integer valued variable x is:
This means that in order 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.
For example,
As example:
Ignoring termination for a moment, we can define the rule for the weakest liberal precondition, denoted wlp, using a predicate \textit{INV}, called the [[loop \textit{INV}ariant]], typically supplied by the programmer:
To show total correctness, we also have to show that the loop terminates. For this we define a wellfounded 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. Exactly, we have
Actually, Dijkstra's Guarded Command Language (GCL) is an extension of the simple imperative language given until here with nondeterministic statements. Indeed, GCL aims to be a formal notation to define algorithms. Nondeterministic statements represent choices left to the actual implementation (in an effective programming language): properties proved on nondeterministic statements are ensured for all possible choices of implementation. In other words, weakestpreconditions of nondeterministic statements ensure
Notice that the definitions of weakestprecondition given above (in particular for whileloop) preserve this property.
Selection is a generalization of if statement:
^{[citation needed]}
Here, when two guards and are simultaneously true, then execution of this statement can run any of the associated statement or .
Repetition is a generalization of while statement in a similar way.
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. We call a logical constant employed to aid in a specification. For example, we can specify a computation that increment x by 1 as
Another example is a computation of a square root of an integer.
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.
where s 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 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. nonstrict) 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
where wpL is the weakest precondition at label L. 
For goto L execution transfers control to label L at which the weakest precondition has to hold. The way that wpL is referred to in the rule should not be taken as a big surprise. It is just 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 , which is the same 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.
wp(do x > 0 → L: x := x1 od; if x < 0 → x := x; goto L ⫿ x ≥ 0 → skip fi, post) = { sequential composition and alternation rules } wp(do x > 0 → L: x := x1 od, (x<0 ∧ wp(x := x; goto L, post)) ∨ (x ≥ 0 ∧ post) = { sequential composition, goto, assignment rules } wp(do x > 0 → L: x := x1 od, x<0 ∧ wpL(x ← x) ∨ x≥0 ∧ post) = { repetition rule } the strongest solution of Z: [ Z ≡ x > 0 ∧ wp(L: x := x1, Z) ∨ x < 0 ∧ wpL(x ← x) ∨ x=0 ∧ post ] = { assignment rule, found wpL = Z(x ← x1) } the strongest solution of Z: [ Z ≡ x > 0 ∧ Z(x ← x1) ∨ x < 0 ∧ Z(x ← x1) (x ← x) ∨ x=0 ∧ post] = { substitution } the strongest solution of Z:[ Z ≡ x > 0 ∧ Z(x ← x1) ∨ x < 0 ∧ Z(x ← x1) ∨ 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 the weakest liberal precondition , 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: for the statement language given above, wlp differs with wp only on whileloop, in not requiring a variant (see above).
Given S a statement and R a precondition (a predicate on the initial state), then is their strongestpostcondition: 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 is provable in Hoare logic if and only if the predicate below hold:
Usually, strongestpostconditions are used in partial correctness. Hence, we have the following relation between weakestliberalpreconditions and strongestpostconditions:
For example, on assignment we have:
where y is fresh 
Above, the logical variable y represents the initial value of variable x. 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.^{[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) and P a predicate. For instance, S(P) may denote wp(S,P) or sp(S,P). We keep x as the variable of the state space.
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.
A predicate transformer S is strict iff:
For instance, wp is artificially made strict, whereas wlp is generally not. In particular, if statement S may not terminate then is satisfiable. We have
Indeed, T is a valid invariant of that loop.
The nonstrict 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 transformer S is terminating if:
Actually, this terminology makes sense only for strict predicate transformers: indeed, is the weakestprecondition ensuring termination of S.
It seems that naming this property nonaborting would be more appropriate: in total correctness, nontermination is abortion, whereas in partial correctness, it is not.
A predicate transformer S is conjunctive iff:
This is the case for , even if statement S is nondeterministic as a selection statement or a specification statement.
A predicate transformer S is disjunctive iff:
This is generally not the case of when S is nondeterministic. Indeed, consider a nondeterministic statement S choosing an arbitrary boolean. This statement is given here as the following selection statement:
Then, reduces to the formula .
Hence, reduces to the tautology
Whereas, the formula reduces to the wrong proposition .
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 weakestpreconditions or strongestpostconditions for imperative expression languages and in particular for monads.
Among them, Hoare Type Theory combines Hoare logic for a Haskelllike language, separation logic and type theory.^{[9]} This system is currently implemented as a Coq library called Ynot.^{[10]} In this language, evaluation of expressions corresponds to computations of strongestpostconditions.
Probabilistic Predicate Transformers are an extension of predicate transformers for probabilistic programs. Indeed, such programs have many applications in cryptography (hiding of information using some randomized noise), distributed systems (symmetry breaking). ^{[11]}