Predicate transformer semantics: Difference between revisions

Revision as of 19:51, 12 May 2010

Revision as of 06:48, 13 May 2010

Line 1:

'''Predicate transformer semantics''' is ana extensionreformulation of [[Floyd–Hoare logic]] introduced by [[Edsger W. Dijkstra|Dijkstra]] in its seminal paper "[[ Guarded_commands | Guarded commands, nondeterminacy and formal derivation of programs ]]". It is a method for defining the semantics of an [[imperative programming]] language by assigning to each ''command'' in the language a corresponding ''predicate transformer''. A ''predicate transformer'' is a [[total function]] mapping between two ''[[Predicate (mathematical logic)|predicates]]'' on the state space of a program. Actually, in [[Guarded commands]], Dijkstra uses only one kind of predicate transformers: the well-known '''weakest precondition''' (see below).

Unlike many other semantic formalisms, predicate transformer semantics was not designed as an investigation into foundations of computation. Rather, it is intended to provide programmers with a methodology to develop their programs as "correct by construction" in an "[[Algebraic_structures | algebraic]] style". This style was advocated by Dijkstra and others, and also developed further in a [[Higher-order_logic|higher order logic]] setting by [[Ralph-Johan Back|R.-J. Back]] in the [[Refinement Calculus]]. It has been mechanized in [[B-Method]].

== Examples of predicate transformers ==

Line 7 ⟶ 5:

=== Weakest precondition ===

The canonical ''predicate transformer'' of sequential imperative programming is the so-called "'''weakest precondition'''" <math>wp(S, R)</math>. Here ''S'' denotes a list of ''commands'' and ''R'' denotes a predicate on the space, called the "[[postcondition]]". The result of applying this function gives the "weakest pre-condition" on the initial state for ''S'' terminating with ''R'' satisfied on the final state. AnAs an example, iswe thegive followingbelow to equivalent definition of the assignment statement (in these formulas, <math>R[x \leftarrow E]</math> is a copy of ''R'' with the value of ''x'' replaced by ''E''):

* version 1: <math> wp(x := E, R)\ =\ \forall y, y = E \Rightarrow R[ y \leftarrow x]\ </math> where ''y'' is a fresh variable.

* version 2: <math> wp(x := E, R)\ =\ R[x \leftarrow E] </math>

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 ''E''. The first version reveals also a deep duality between weakest-precondition and strongest-postcondition (see below) through the duality between quantifier <math>\forall</math> (resp. connector <math>\Rightarrow</math>) and <math>\exists</math> (resp. <math>\wedge</math>).

:<math> wp(x := E, R)\ =\ R[x \leftarrow E] </math>

An example of a valid calculation of ''wp'' (using version 2) for assignments with integer valued variablesvariable ''x'' and ''y'' is:

This gives a predicate that is a copy of ''R'' with the value of ''x'' replaced by ''E''.

An example of a valid calculation of ''wp'' for assignments with integer valued variables ''x'' and ''y'' is:

:<math> wp(x := x - 5, x > 10)\ =\ (x - 5 > 10)\ =\ (x > 15) </math>

Line 26 ⟶ 24:

=== Strongest postcondition ===

Given ''S'' a statement (or in other words, a list of commands) and ''R'' a [[ precondition ]] (a predicate on the initial state), then

<math>sp(S, R)</math> is the '''strongest-postcondition''': it implies any postcondition satisfied by the final state of the execution of S,

for any initial state statisfying R. For example, on assignment we have:

:<math> sp(x := E, R)\ =\ \exists y, Rx=E[x \leftarrow y] \wedge x=ER[x \leftarrow y]</math> where <math>y</math> is fresh.

TheAbove, the logical variable <math>y</math> above represents the initial value of variable <math>x</math>.

Hence,

:<math> sp(x := x - 5, x > 15)\ =\ \exists y, x = y >- 155 \wedge x = y -> 515 \ = \ x > 10</math>

=== Others ===

[[Leslie Lamport]] has suggested ''win'' and ''sin'' as ''predicate transformers'' for [[concurrent programming]].

== Applications ==

* Unlike many other semantic formalisms, predicate transformer semantics was not designed as an investigation into foundations of computation. Rather, it is intended to provide programmers with a methodology to develop their programs as "correct by construction" in an "[[Algebraic_structures | algebraic]]calculation style". This style was advocated by Dijkstra and others, and also developed further in a [[Higher-order_logic|higher order logic]] setting by [[Ralph-Johan Back|R.-J. Back]] in the [[Refinement Calculus]]. It has been mechanized in [[B-Method]].

* In the meta-theory of [[Hoare logic]], weakest-preconditions are a key notion of the proof of relative completness.

== Links with [[Guarded commands]] ==