Predicate transformer semantics: Difference between revisions

Revision as of 14:35, 1 March 2010

Revision as of 13:33, 3 March 2010

Line 1:

'''Predicate transformer semantics''' is an extension of [[Floyd–Hoare logic]] invented by [[Edsger W. Dijkstra|Dijkstra]] and extended and refined by other 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|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.