Axiomatic Semantics
Axiomatic semantics is an approach based on mathematical logic to proving the correctness of computer programs.
It is defined as follows:
Axiomatic semantics defines 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.
Mathematical logic includes the mathematical study of logic and the applications of formal logic to other areas of mathematics.
Axiomatic semantics are closely related to Hoare logic:
Hoare logic is to provide a set of logical rules in order to reason about the correctness of computer programs with the rigour of mathematical logic.
Hoare logic has axioms and inference rules for all the constructs of a simple imperative programming language.
The central feature of Hoare logic is the Hoare triple.
A triple describes how the execution of a piece of code changes the state of the computation.
A Hoare triple is of the form
{P} C {Q}
where P and Q are assertions and C is a command.
P is called the precondition and Q the postcondition:
- Preconditions:
Assertions about things that are true just before execution of the construct.
- Postconditions:
Assertions about things that are true just after the execution of the construct.