Revision as of 13:09, 14 May 2010 edit Boulme (talk \| contribs) 90 edits link to symbolic execution ← Previous edit		Revision as of 13:11, 14 May 2010 edit undo Boulme (talk \| contribs) 90 edits mNo edit summary Next edit →
Line 1: '''[[Predicate]] transformer semantics''' are a reformulation of [[Floyd–Hoare logic]]. ~~While~~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: Difference between revisions