Predicate transformer semantics: Difference between revisions

Revision as of 06:14, 14 May 2010

Revision as of 12:48, 14 May 2010

Line 3:

Predicate transformer semantics has been 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 preconditions''' (see below).

== Weakest preconditions ==

== Examples of predicate transformers ==

=== Weakest preconditionDefinition ===

Given a ''S'' denotes a ''statement'', the '''weakest-precondition''' of ''S'' is a

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. As an example, we give below to equivalent definition of the assignment statement (in these formulas, <math>R[x \leftarrow E]</math> is a copy of ''R'' where [[ Free_variables_and_bound_variables| fresh occurrences]] of ''x'' are replaced by ''E''):

function mapping any [[postcondition]] ''R'' (''R'' denotes thus a predicate on the space of states) to a [[precondition]]. Actually, the result of this function, denoted <math>wp(S, R)</math>, is the "weakest" precondition on the initial state ensuring that execution of ''S'' terminates in a final state satisfying ''R''. More formally, a given ''Hoare triple'' <math>\{ P \} S \{ Q \}</math> is provable in [[ Hoare logic ]] for '''total correctness''' iff the first-order predicate below is universally valid (e.g. for all possible values of the space of states):

:<math>P \Rightarrow wp(S,Q)</math>

Formally, weakest-preconditions are defined recursively over the [[abstract syntax]] of statements.

=== OthersSkip ===

<math>wp(skip,R) \ =\ R</math>

=== Abort ===

<math>wp(abort,R) \ =\ False</math>

=== Assignment ===

We give below two equivalent weakest-preconditions for the assignment statement (in these formulas, <math>R[x \leftarrow E]</math> is a copy of ''R'' where [[ Free_variables_and_bound_variables| fresh occurrences]] of ''x'' are 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 (representing the final value of variable ''x'').

* version 2:

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

Line 16 ⟶ 30:

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

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

This means that in order for the "post-condition" ''x > 10'' to be true after the assignment, the "pre-condition" ''x > 15'' must be true before the assignment. This is also the "weakest pre-condition", in that it is the "weakest" restriction on the value of ''x'' which makes ''x > 10'' true after the assignment.

=== Weakest liberal preconditionSequence ===

<math>wp(S_1;S_2,R)\ =\ wp(S_1,wp(S_2,R))</math>

As example:

{{Anchor|Weakest liberal precondition}} An important variant of the weakest precondition is the '''weakest liberal precondition''' <math>wlp(S, R)</math>, which yields the weakest condition under which ''S'' either does not terminate or establishes ''R''. It therefore differs from ''wp'' in not guaranteeing termination.

:<math>wp(x:=x-5;x:=x*2\ ,\ x>20)\ =\ wp(x:=x-5,wp(x:=x*2, x > 20))\ =\ wp(x:=x-5,x*2 > 20)\ =\ (x-5)*2 > 20</math>

== ExamplesOther examples of predicate transformers ==

=== Weakest liberal precondition ===

{{Anchor|Weakest liberal precondition}} An important variant of the weakest precondition is the '''weakest liberal precondition''' <math>wlp(S, R)</math>, 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.

=== 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:

Line 39 ⟶ 59:

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

=== Win and sin predicate transformers ===

=== Others ===

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