Predicate transformer semantics
Encyclopedia
Predicate transformer semantics was introduced by 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 transformers: 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.
function mapping any postcondition
R to a precondition
. Actually, the result of this function, denoted
, 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
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.
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 core logic: it is thus a pure expression, totally defined, terminating and without side effect.
Imperative programming
In computer science, imperative programming is a programming paradigm that describes computation in terms of statements that change a program state...
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
Denotational semantics
In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...
. Actually, in Guarded commands, Dijkstra uses only one kind of predicate transformers: 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
Deductive system
A deductive system consists of the axioms and rules of inference that can be used to derive the theorems of the system....
, predicate transformer semantics (either by weakest-preconditions or by strongest-postconditions see below) are complete strategies to build valid deductions
Deductive reasoning
Deductive reasoning, also called deductive logic, is reasoning which constructs or evaluates deductive arguments. Deductive arguments are attempts to show that a conclusion necessarily follows from a set of premises or hypothesis...
of Hoare logic. In other words, they provide an effective algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
to reduce the problem of verifying a Hoare triple to the problem of proving a first-order formula
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
. Technically, predicate transformer semantics perform a kind of symbolic execution
Symbolic execution
In computer science, symbolic execution refers to the analysis of programs by tracking symbolic rather than actual values, a case of abstract interpretation. The field of symbolic simulation applies the same concept to hardware...
of statements into predicates: execution runs backward in the case of weakest-preconditions, or runs forward in the case of strongest-postconditions.
Definition
Given S a statement, the weakest-precondition of S is afunction mapping any postcondition
Postcondition
In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions within the code itself...
R to a precondition
Precondition
In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification....
. Actually, the result of this function, denoted
, 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
Tuple
In mathematics and computer science, a tuple is an ordered list of elements. In set theory, an n-tuple is a sequence of n elements, where n is a positive integer. There is also one 0-tuple, an empty sequence. An n-tuple is defined inductively using the construction of an ordered pair...
of variables involved in statement S. Then, a given Hoare triple
is provable in Hoare logicHoare logic
Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
for total correctness if and only if the first-order predicate below holds:
Formally, weakest-preconditions are defined recursively over the abstract syntax
Abstract syntax
The abstract syntax of data is its structure described as a data type , independent of any particular representation or encoding....
of statements. Actually, weakest-precondition semantics is a Continuation-passing style
Continuation-passing style
In functional programming, continuation-passing style is a style of programming in which control is passed explicitly in the form of a continuation. Gerald Jay Sussman and Guy L. Steele, Jr...
semantics of state transformers where the predicate in parameter is a continuation.
Skip
 |
Abort
 |
Assignment
We give below two equivalent weakest-preconditions for the assignment statement. In these formulas, is a copy of R where free occurrencesFree variables and bound variables
In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a free variable is a notation that specifies places in an expression where substitution may take place...
of x are replaced by E. Hence, here, expression E is implicitly coerced into a valid term of the core logic: it is thus a pure expression, totally defined, terminating and without side effect.
- version 1:
where y is a fresh variable (representing the final value of variable x)- version 2:
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 reveals also 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.
Sequence
For example,
Conditional
As example:
While loop
Weakest-precondition of while-loop is usually parametrized by a predicate I called loop invariantLoop invariantIn computer science, a loop invariant is an invariant used to prove properties of loops. Informally, a loop invariant is a statement of the conditions that should be true on entry into a loop and that are guaranteed to remain true on every iteration of the loop...
, and a well-founded relationWell-founded relationIn mathematics, a binary relation, R, is well-founded on a class X if and only if every non-empty subset of X has a minimal element with respect to R; that is, for every non-empty subset S of X, there is an element m of S such that for every element s of S, the pair is not in R:\forall S...
on the space state denoted "<" and called loop variantLoop variantIn computer science, a loop variant is a mathematical function defined on the state space of a computer program whose value is monotonically decreased with respect to a well-founded relation by the iteration of a while loop under some invariant conditions, thereby ensuring its termination...
. Hence, we have:
where y is a fresh tuple of variables
Informally, in the above conjunction of three formulas:- the first one means that invariant I must initially hold;
- the second one means that the body of the loop (e.g. statement S) must preserve the invariant and decrease the variant: here, variable y represents the initial state of the body execution;
- the last one means that R must be established at the end of the loop: here, variable y represents the final state of the loop.
In predicate transformers semantics, invariant and variant are built by mimicking Kleene fixed-point theorem. Below, this construction is sketched in set theorySet theorySet theory is the branch of mathematics that studies sets, which are collections of objects. Although any type of object can be collected into a set, set theory is applied most often to objects that are relevant to mathematics...
. We assume that U is a set denoting the state space. First, we define a family of subsets of U denoted
by induction over Natural numberNatural numberIn mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
k. Informally
represents the set of initial states that makes R satisfied after less than k iterations of the loop:
Then, we define:- invariant I as the predicate
. - variant
as the proposition 
With these definitions,
reduces to formula 
.
However in practice, such an abstract construction can not be handled efficiently by theorem provers. Hence, loop invariants and variants are provided by human users, or are inferred by some abstract interpretationAbstract interpretationIn computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer program which gains information about its semantics In...
procedure.
Non-deterministic guarded commands
Actually, Dijkstra's Guarded Command LanguageGuarded Command LanguageThe Guarded Command Language is a language defined by Edsger Dijkstra for predicate transformer semantics. It combines programming concepts in a compact way, before the program is written in some practical programming 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.
Notice that 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
and 
are simultaneously true, then execution of this statement can run any of the associated statement 
or 
.
Specification statement (or weakest-precondition of procedure call)
Refinement calculusRefinement CalculusRefinement calculus is a formalized approach to stepwise refinement for program construction. The required behaviour of the final executable program is specified as an abstract and perhaps non-executable "program", which is then refined by a series of correctness-preserving transformations into an...
extends non-deterministic statements with the notion of specification statement. Informally, this statement represents a procedure call in black box, where the body of the procedure is not known. Typically, using a syntax close to B-MethodB-MethodThe B method is method of software development based on B, a tool-supported formal method based around an abstract machine notation, used in the development of computer software. It was originally developed by Jean-Raymond Abrial in France and the UK. B is related to the Z notation and supports...
, a specification statement is written
@
where- x is the global variable modified by the statement,
- P is a predicate representing the precondition,
- y is a fresh logical variable, bound in Q, that represents the new value of x non-deterministically chosen by the statement,
- Q is a predicate representing a postcondition, or more exactly a guard: in Q, variable x represents the initial state and y denotes the final state.
The weakest-precondition of specification statement is given by:@ 
where z is a fresh name
Moreover, a statement S implements such a specification statement if and only if the following predicate is a tautology:
where
is a fresh name (denoting the initial state)
Indeed, in such a case, the following property is ensured for all postcondition R (this is a direct consequence of wp monotonicity, see below):
@
Informally, this last property ensures that any proof about some statement involving a specification remains valid
when replacing this specification by any of its implementation.
Weakest liberal precondition
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 logicHoare logicHoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
in partial correctness: for the statement language given above, wlp differs with wp only on while-loop, in not requiring a variant.
Strongest postcondition
Given S a statement and R a preconditionPreconditionIn computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification....
(a predicate on the initial state), then
is their strongest-postcondition: it implies any postcondition satisfied by the final state of any execution of S,
for any initial state statisfying R. In other words, a Hoare triple
is provable in Hoare logic if and only if the predicate below hold:
Usually, strongest-postconditions are used in partial correctness.
Hence, we have the following relation between weakest-liberal-preconditions and strongest-postconditions:
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):
Win and sin predicate transformers
Leslie LamportLeslie LamportLeslie Lamport is an American computer scientist. A graduate of the Bronx High School of Science, he received a B.S. in mathematics from the Massachusetts Institute of Technology in 1960, and M.A. and Ph.D. degrees in mathematics from Brandeis University, respectively in 1963 and 1972...
has suggested win and sin as predicate transformers for concurrent programming.
Predicate transformers properties
This section presents some characteristic properties of predicate transformers. Below, T denotes a predicate transformer (a function between two predicates on the state space) and P a predicate. For instance, T(P) may denote wp(S,P) or sp(S,P). We keep x as the variable of the state space.
Monotonic
Predicate transformers of interest (wp, wlp, and sp) are monotonic. A predicate transformer T is monotonic if and only if:
This property is related to Consequence rule of Hoare logic.
Strict
A predicate transformer T is strict iff:
For instance, wp is strict, whereas wlp is generally not. In particular, if statement S may not terminate then
is satisfiable. We have
Indeed, true is a valid invariant of that loop.
Terminating
A predicate transformer T is terminating iff:
Actually, this terminology makes sense only for strict predicate transformers: indeed,
is the weakest-precondition ensuring termination of S.
It seems that naming this property non-aborting would be more appropriate: in total correctness, non-termination is abortion, whereas in partial correctness, it is not.
Conjunctive
A predicate transformer T is conjunctive iff:
This is the case for
, even if statement S is non-deterministic as a selection statement or a specification statement.
Disjunctive
A predicate transformer T is disjunctive iff:
This is generally not the case of
when S is non-deterministic. Indeed, let us consider a non-deterministic 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
.
The same counter-example can be reproduced using a specification statement (see above) instead:
@
Applications
- Computations of weakest-preconditions are largely used to statically check assertions in programsAssertion (computing)In computer programming, an assertion is a predicate placed in a program to indicate that the developer thinks that the predicate is always true at that place.For example, the following code contains two assertions:...
using a theorem-prover (like SMT-solversSatisfiability Modulo TheoriesIn computer science, the Satisfiability Modulo Theories problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality...
or proof assistantsInteractive theorem provingIn computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by man-machine collaboration...
): see Frama-CFrama-CFrama-C stands for Framework for Modular Analysis of C programs. Frama-C is a set of interoperable program analyzers for C programs. Frama-C has been developed by Commissariat à l'Énergie Atomique et aux Énergies Alternatives and Inria...
or ESC/Java2ESC/JavaESC/Java , the "Extended Static Checker for Java," is a programming tool that attempts to find common run-time errors in Java programs at compile time...
.
- Unlike many other semantic formalisms, predicate transformer semantics was not designed as an investigation into foundations of computation. Rather, it was intended to provide programmers with a methodology to develop their programs as "correct by construction" in a "calculation style". This "top-down" style was advocated by Dijkstra and N. WirthNiklaus WirthNiklaus Emil Wirth is a Swiss computer scientist, best known for designing several programming languages, including Pascal, and for pioneering several classic topics in software engineering. In 1984 he won the Turing Award for developing a sequence of innovative computer languages.-Biography:Wirth...
. It has been formalized further by R.-J. BackRalph-Johan BackRalph-Johan Back is a Finnish computer scientist.Back originated the refinement calculus, an important approach to the formal development of programs using stepwise refinement, in his 1978 PhD thesis at the University of Helsinki, On the Correctness of Refinement Steps in Program Development. He...
and others in the Refinement CalculusRefinement CalculusRefinement calculus is a formalized approach to stepwise refinement for program construction. The required behaviour of the final executable program is specified as an abstract and perhaps non-executable "program", which is then refined by a series of correctness-preserving transformations into an...
. Some tools like B-MethodB-MethodThe B method is method of software development based on B, a tool-supported formal method based around an abstract machine notation, used in the development of computer software. It was originally developed by Jean-Raymond Abrial in France and the UK. B is related to the Z notation and supports...
provide now automated reasoningAutomated reasoningAutomated reasoning is an area of computer science dedicated to understand different aspects of reasoning. The study in automated reasoning helps produce software which allows computers to reason completely, or nearly completely, automatically...
in order to promote this methodology.
- In the meta-theory of Hoare logicHoare logicHoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
, weakest-preconditions appear as a key notion in the proof of relative completnessGödel's completeness theoremGödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It was first proved by Kurt Gödel in 1929....
.
Weakest-preconditions and strongest-postconditions of imperative expressions
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.
Among them, Hoare Type Theory combines Hoare logicHoare logicHoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
for a HaskellHaskell (programming language)Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
-like language, Separation logicSeparation logicIn computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs.It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Burstall...
and Type TheoryType theoryIn mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
.
This system is currently implemented as a CoqCoqIn computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...
library called Ynot. In this language, evaluation of expressionsEvaluation strategyIn computer science, an evaluation strategy is a set of rules for evaluating expressions in a programming language. Emphasis is typically placed on functions or operators: an evaluation strategy defines when and in what order the arguments to a function are evaluated, when they are substituted...
corresponds to computations of strongest-postconditions.
Probabilistic Predicate Transformers
Probabilistic Predicate Transformers are an extension of predicate transformers for probabilistic programsRandomized algorithmA randomized algorithm is an algorithm which employs a degree of randomness as part of its logic. The algorithm typically uses uniformly random bits as an auxiliary input to guide its behavior, in the hope of achieving good performance in the "average case" over all possible choices of random bits...
.
Indeed, such programs have many applications in cryptographyCryptographyCryptography is the practice and study of techniques for secure communication in the presence of third parties...
(hiding of information using some randomized noise),
Distributed systems (symmetry breaking).
See also
- Axiomatic semanticsAxiomatic semanticsAxiomatic semantics is an approach based on mathematical logic to proving the correctness of computer programs. It is closely related to Hoare logic....
— includes predicate transformer semantics - Formal semantics of programming languagesFormal semantics of programming languagesIn programming language theory, semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages and models of computation...
— an overview - Hoare logicHoare logicHoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
— the best-known axiomatic semantics - Refinement calculusRefinement CalculusRefinement calculus is a formalized approach to stepwise refinement for program construction. The required behaviour of the final executable program is specified as an abstract and perhaps non-executable "program", which is then refined by a series of correctness-preserving transformations into an...
, an extension of guarded commands (and Hoare logic) exploiting the latticeLattice (order)In mathematics, a lattice is a partially ordered set in which any two elements have a unique supremum and an infimum . Lattices can also be characterized as algebraic structures satisfying certain axiomatic identities...
structure of predicate transformers (for "refinement" order). - Dynamic logicDynamic logic (modal logic)Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs and later applied to more general complex behaviors arising in linguistics, philosophy, AI, and other fields.-Language:...
, where predicate transformers appear as modalities (in the sense of Modal logicModal logicModal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...
).
- version 2: