Predicate transformer semantics
Predicate transformer semantics were introduced by Edsger Dijkstra in his seminal paper "Guarded commands, nondeterminacy and formal derivation of programs". They define the semantics of an imperative programming paradigm by assigning to each statement in this language a corresponding predicate transformer: a total function between two 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 transformer: the well-known weakest preconditions (see below).
- Comment
- enPredicate transformer semantics were introduced by Edsger Dijkstra in his seminal paper "Guarded commands, nondeterminacy and formal derivation of programs". They define the semantics of an imperative programming paradigm by assigning to each statement in this language a corresponding predicate transformer: a total function between two 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 transformer: the well-known weakest preconditions (see below).
- Has abstract
- enPredicate transformer semantics were introduced by Edsger Dijkstra in his seminal paper "Guarded commands, nondeterminacy and formal derivation of programs". They define the semantics of an imperative programming paradigm by assigning to each statement in this language a corresponding predicate transformer: a total function between two 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 transformer: the well-known weakest preconditions (see below). Moreover, predicate transformer semantics are a reformulation of Floyd–Hoare logic. Whereas Hoare logic is presented as a deductive system, predicate transformer semantics (either by weakest-preconditions or by strongest-postconditions see below) are complete strategies to build valid deductions of Hoare logic. In other words, they provide an effective algorithm to reduce the problem of verifying a Hoare triple to the problem of proving a 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, or runs forward in the case of strongest-postconditions.
- Is primary topic of
- Predicate transformer semantics
- Label
- enPredicate transformer semantics
- Link from a Wikipage to an external page
- books.google.com/books%3Fid=cCbjBwAAQBAJ
- archive.org/details/disciplineofprog0000dijk
- archive.org/details/mathematicaltheo0000bakk
- archive.org/details/scienceofprogram0000grie
- Link from a Wikipage to another Wikipage
- Algorithm
- Assertion (computing)
- Automated reasoning
- Axiomatic semantics
- B-Method
- Category:Edsger W. Dijkstra
- Category:Formal methods
- Category:Program logic
- Concurrent programming
- Coq
- Cryptography
- Deductive reasoning
- Deductive system
- Denotational semantics
- Distributed systems
- Dynamic logic (modal logic)
- Edsger W. Dijkstra
- Evaluation strategy
- First-order logic
- Floyd–Hoare logic
- Formal Aspects of Computing
- Formal semantics of programming languages
- Frama-C
- Free variables and bound variables
- Gödel's completeness theorem
- Guarded Command Language
- Guarded commands
- Haskell (programming language)
- Hoare logic
- Imperative programming
- Interactive theorem proving
- Java
- Leslie Lamport
- Loop invariant
- Monad (functional programming)
- Monotonic
- Niklaus Wirth
- Postcondition
- Precondition
- Predicate (mathematical logic)
- Ralph-Johan Back
- Randomized algorithm
- Refinement calculus
- Satisfiability modulo theories
- Separation logic
- Symbolic execution
- Total function
- Type theory
- Well-founded relation
- SameAs
- 2iCn5
- m.052trm
- Predicate transformer semantics
- Q291929
- Semàntica de transformació de predicats
- Semántica de transformación de predicados
- Wp-Kalkül
- Предикатно-трансформативна семантика
- Слабейшее предусловие
- 述語変換意味論
- Subject
- Category:Edsger W. Dijkstra
- Category:Formal methods
- Category:Program logic
- WasDerivedFrom
- Predicate transformer semantics?oldid=1124903239&ns=0
- WikiPageLength
- 26651
- Wikipage page ID
- 1453583
- Wikipage revision ID
- 1124903239
- WikiPageUsesTemplate
- Template:Anchor
- Template:Citation needed
- Template:Cite book
- Template:Cite journal
- Template:Edsger Dijkstra
- Template:Mvar
- Template:Refbegin
- Template:Refend
- Template:Reflist
- Template:Semantics
- Template:Short description