'''[[Predicate]] transformer semantics''' isare 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 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 hashave been introduced by [[Edsger W. Dijkstra|Dijkstra]] in its seminal paper "[[Guarded_commands |Guarded commands, nondeterminacy and formal derivation of programs]]". ItThey is a method for definingdefine the semantics of an [[imperative programming]] language by assigning to each ''commandstatement'' in thethis language a corresponding ''predicate transformer'': a ''predicate transformer'' is a [[total function]] mapping between two ''[[Predicate (mathematical logic)|predicates]]'' on the state space of athe programstatement. Actually, in [[Guarded commands]], Dijkstra uses only one kind of predicate transformers: the well-known '''weakest preconditions''' (see below).
== Weakest preconditions ==
Line 7 ⟶ 8:
=== Definition ===
Given a ''S'' denotes a ''statement'', the '''weakest-precondition''' of ''S'' is a
function mapping any [[postcondition]] ''R'' (''R'' denotes thus a predicate on the space of states) to a [[precondition]]. Actually, the result of this function, denoted <math>wp(S, R)</math>, is the "weakest" precondition on the initial state ensuring that execution of ''S'' terminates in a final state satisfying ''R''. More formally, a given ''Hoare triple'' <math>\{ P \} S \{ Q \}</math> is provable in [[ Hoare logic ]] for '''total correctness''' iff the first-order predicate below is universally valid (e.g. for all possible values of the space of states):
