Predicate transformer semantics: Difference between revisions

Revision as of 16:44, 15 May 2010

Revision as of 20:16, 15 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. In this sense, predicate transformer semantics are a kind of [[Denotational semantics]]. 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) giveprovide 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).