Predicate transformer semantics: Difference between revisions

Revision as of 16:42, 14 May 2010

Revision as of 16:51, 14 May 2010

Line 1:

'''[[Predicate (mathematical logic)| Predicate]] transformer semantics''' have been introduced by [[Edsger W. Dijkstra|Dijkstra]] in its seminal paper "[[Guarded_commands |Guarded commands, nondeterminacy and formal derivation of programs]]". They define the semantics of an [[imperative programming]] language by assigning to each ''statement'' in this language a corresponding ''predicate transformer'': a [[total function]] mapping between two ''[[Predicate (mathematical logic)|predicates]]'' on the state space of the statement. Actually, in [[Guarded commands]], Dijkstra uses only one kind of predicate transformers: the well-known '''weakest preconditions''' (see below).

'''[[Predicate]] transformer semantics''' are a reformulation of [[Floyd–Hoare logic]]. Whereas 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 of verifying a Hoare triple to the problem of proving a [[First-order logic | first-order formula]].

Technically, predicate transformer semantics perform a kind of [[Symbolic execution]] of statements into predicates.

'''[[Predicate]] transformer semantics''' are a reformulation of [[Floyd–Hoare logic]]. Whereas 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 of verifying a Hoare triple to the problem of proving a [[First-order logic | first-order formula]]. Technically, predicate transformer semantics perform a kind of [[Symbolic execution]] of statements into predicates (execution runs ''backward'' in the case of weakest-preconditions,

and runs ''forward'' in the case of strongest-postconditions).

Predicate transformer semantics have been introduced by [[Edsger W. Dijkstra|Dijkstra]] in its seminal paper "[[Guarded_commands |Guarded commands, nondeterminacy and formal derivation of programs]]". They define the semantics of an [[imperative programming]] language by assigning to each ''statement'' in this language a corresponding ''predicate transformer'': a [[total function]] mapping between two ''[[Predicate (mathematical logic)|predicates]]'' on the state space of the statement. Actually, in [[Guarded commands]], Dijkstra uses only one kind of predicate transformers: the well-known '''weakest preconditions''' (see below).

== Weakest preconditions ==