Predicate transformer semantics

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).where y is a fresh variable (representing the final value of variable x)where y is a fresh tuple of variableswhere z is a fresh namewhere x 0 {displaystyle x_{0}} is a fresh name (denoting the initial state)where y is fresh 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. Given a statement S, the weakest-precondition of S is afunction mapping any postcondition R to a precondition P. Actually, the result of this function, denoted w p ( S , R ) {displaystyle wp(S,R)} , is the 'weakest' precondition on the initial state ensuring that execution of S terminates in a final state satisfying R. More formally, let us use variable x to denote abusively the tuple of variables involved in statement S. Then, a given Hoare triple { P } S { R } {displaystyle {P}S{R}} is provable in Hoare logic for total correctness if and only if the first-order predicate below holds: Formally, weakest-preconditions are defined recursively over the abstract syntax of statements. Actually, weakest-precondition semantics is a continuation-passing style semantics of state transformers where the predicate in parameter is a continuation. We give below two equivalent weakest-preconditions for the assignment statement. In these formulas, R [ x ← E ] {displaystyle R} 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. The first version avoids a potential duplication of E 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: 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.