Predicate transformer semantics were introduced by
Edsger Dijkstra
Edsger Wybe Dijkstra ( ; ; 11 May 1930 – 6 August 2002) was a Dutch computer scientist, programmer, software engineer, systems scientist, and science essayist. He received the 1972 Turing Award for fundamental contributions to developing progra ...
in his seminal paper "
Guarded commands, nondeterminacy and formal derivation of programs". They define the semantics of an
imperative programming
In computer science, imperative programming is a programming paradigm of software that uses statements that change a program's state. In much the same way that the imperative mood in natural languages expresses commands, an imperative program ...
paradigm by assigning to each ''statement'' in this language a corresponding ''predicate transformer'': a
total function
In mathematics, a partial function from a set to a set is a function from a subset of (possibly itself) to . The subset , that is, the domain of viewed as a function, is called the domain of definition of . If equals , that is, if is ...
between two ''
predicates
Predicate or predication may refer to:
* Predicate (grammar), in linguistics
* Predication (philosophy)
* several closely related uses in mathematics and formal logic:
**Predicate (mathematical logic)
** Propositional function
**Finitary relation, ...
'' on the state space of the statement. In this sense, predicate transformer semantics are a kind of
denotational semantics
In computer science, denotational semantics (initially known as mathematical semantics or Scott–Strachey semantics) is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called ''denotations' ...
. 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
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) 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 log ...
. Whereas Hoare logic is presented as a
deductive system
A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A form ...
, 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
In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...
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 In computer science, symbolic execution (also symbolic evaluation or symbex) is a means of analyzing a program to determine what inputs cause each part of a program to execute. An interpreter follows the program, assuming symbolic values for in ...
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 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 ...
''R'', a weakest precondition is a predicate ''Q'' such that for any
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.
If a precondition is violated, the effect of th ...
,
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 repect 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,