Definition
Axiomatic Semantics
Axiomatic semantics define the meaning of a program by using logical assertions about its state before and after execution. Instead of describing how a program executes, it specifies what must be true of the state.
Core Construct
The primary vehicle for axiomatic semantics is the Hoare triple:
- is the precondition.
- is the program.
- is the postcondition.
Verification
The meaning of program constructs (like assignment, composition, or loops) is given by a set of axioms and inference rules. These rules allow for the formal proof of program properties without simulating execution.
Abstraction
Axiomatic semantics is the most abstract form of semantics, as it ignores intermediate values and execution paths, focusing solely on the relationship between initial and final states. This makes it particularly suitable for formal verification and program proofing.