Go backward to Operational Semantics Go up to Top Go forward to Denotational semantics

Axiomatic semantics

• Language defined by system of logical axioms and inference rules.
• Each construct defined by an axiom.
• Not the meaning of a program but its properties are defined.

{ A } P { B }

P ...program
A ...precondition
B ...postcondition

Provable properties need not characterize program uniquely.