Predicate transformer semantics: Difference between revisions

Revision as of 06:48, 13 May 2010

Revision as of 06:14, 14 May 2010

Line 1:

'''Predicate transformer semantics''' is a reformulation of [[Floyd–Hoare logic]]. While [[Hoare logic]] was originally presented as a [[deductive system]], predicate transformer semantics (either by '''weakest-preconditions''' or by '''strongest-postconditions''' see below) give an effective [[algorithm]] to reduce the problem verifying a Hoare triple to the problem of proving a [[First-order logic | first-order formula]].

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''.: Aa ''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 preconditionpreconditions''' (see below).

== Examples of predicate transformers ==

Line 5 ⟶ 7:

=== 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. 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'' withwhere the[[ valueFree_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.

* 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>).

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

Line 43 ⟶ 47:

* 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 "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]].

* Computations of weakest-preconditions are used to check [[Assertion_(computing) | assertions]] in programs using a theorem-prover (like [[Satisfiability_Modulo_Theories|SMT-solvers]] or [[Interactive_theorem_proving |proof assistants]]): see [[Frama-C]] or [[ESC/Java|ESC/Java2]].

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

* In the meta-theory of [[Hoare logic]], weakest-preconditions are a key notion ofin the proof of [[ Gödel's_completeness_theorem | relative completness]].

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