Predicate transformer semantics: Difference between revisions

Revision as of 11:56, 12 May 2010

Revision as of 19:51, 12 May 2010

Line 1:

'''Predicate transformer semantics''' is an extension of [[Floyd–Hoare logic]] inventedintroduced by [[Edsger W. Dijkstra|Dijkstra]] andin extendedits andseminal refinedpaper by"[[ otherGuarded_commands researchers.| It was first introduced in Dijkstra's paper "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 aan "calculational[[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 ==

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" for ''S'' terminating with ''R'' true. An example is the following definition of the assignment statement:

=== Weakest precondition ===

:<math> wp(x := E, R)\ =\ R_E^x </math>

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'' truesatisfied on the final state. An example is the following definition of the assignment statement:

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

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 := yx - 5, x > 10)\ =\ (yx - 5 > 10)\ =\ (yx > 15) </math>

This means that in order for the "post-condition" ''x > 10'' to be true after the assignment, the "pre-condition" ''yx > 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 ''yx'' which makes ''x > 10'' true after the assignment.

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

=== Strongest postcondition ===

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

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

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

<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, R[x \leftarrow y] \wedge x=E[x \leftarrow y]</math>

This means that in order for the "post-condition" ''x > 10'' to be true after the assignment, the "pre-condition" ''y > 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 ''y'' which makes ''x > 10'' true after the assignment.

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, y > 15 \wedge x = y - 5 \ = \ x > 10</math>

Dijkstra also defined alternative ('''if''') and repetitive ('''do''') constructs as well as a composition operator (''';''') using ''wp''. The alternative and repetitive constructs used ''[[guarded commands]]'' to influence execution. Because of the rules he imposed on the definition of ''wp'', both constructs allow for non-deterministic execution if the ''[[guard (computing)|guard]]s'' in the commands are non disjoint.

=== Others ===

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 a "calculational 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]].

Although the most common and most widely discussed because of their relevance to sequential programming, "weakest pre-conditions" are not the only ''predicate transformers''. For example, [[Leslie Lamport]] has suggested ''win'' and ''sin'' as ''predicate transformers'' for [[concurrent programming]].

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

Dijkstra also defined alternative ('''if''') and repetitive ('''do''') constructs as well as a composition operator (''';''') using ''wp''. The alternative and repetitive constructs used ''[[guarded commands]]'' to influence execution. Because of the rules he imposed on the definition of ''wp'', both constructs allow for non-deterministic execution if the ''[[guard (computing)|guard]]s'' in the commands are non disjoint.

== See also ==

Line 28 ⟶ 49:

* [[Formal semantics of programming languages]] — an overview

* [[Hoare logic]] — the best-known axiomatic semantics

* [[Refinement calculus]], an extension of Hoare logic exploiting the [[ Lattice_(order) | lattice ]] structure of predicate transformers (for "refinement" order).

* [[Dynamic_logic_(modal_logic)|Dynamic logic]], where predicate transformers appear as modalities (in the sense of [[Modal logic]]).