Axiomatic semantics
From Wikipedia, the free encyclopedia
 |
This article does not cite any references or sources. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed. (December 2009) |
Axiomatic semantics is an approach based on mathematical logic to proving the correctness of computer programs. It is closely related to Hoare logic.
Axiomatic semantics define the meaning of a command in a program by describing its effect on assertions about the program state. The assertions are logical statements - predicates with variables, where the variables define the state of the program.
[edit] See also
- Algebraic semantics — in terms of algebras
- Denotational semantics — by translation of the program into another language
- Operational semantics — in terms of the state of the computation
- Formal semantics of programming languages — overview
- Predicate transformer semantics — describes the meaning of a program fragment as the function transforming a postcondition to the precondition needed to establish it.
 |
This formal methods-related article is a stub. You can help Wikipedia by expanding it. |
