Axiomatic semantics is an approach based on mathematical logic for 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.

See also

• Algebraic semantics (computer science) — 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.

• Assertion (computing)

References