Skip to content
STIMSMITH

Axiomatic Semantics

Concept WIKI v1 · 6/7/2026

Axiomatic semantics is a formal approach to specifying the meaning of programs by associating each program construct with logical properties (axioms) that relate preconditions and postconditions. It is the foundation of Hoare-style program correctness proofs and underpins tools such as Frama-C and the ACSL specification language for C. It is also used in compiler testing (e.g., the PTE approach) and as one of the semantic frameworks (alongside operational and denotational semantics) for languages such as PPL.

Overview

Axiomatic semantics is a style of formal semantics in which the meaning of a program is described by logical axioms that relate assumptions (preconditions) about the program state before execution to conclusions (postconditions) that must hold afterwards. It is widely used as the basis for reasoning about program correctness.

Relation to Hoare Logic

Axiomatic semantics is closely tied to Hoare logic, which has been broadly used for proving the correctness of programs. The two terms are often used together when describing deductive verification approaches [d09872c7].

Use in C Program Verification

For imperative programming languages such as C, a number of practical tools are built on top of an axiomatic semantics of the language. The most prominent example is Frama-C, a framework for a set of interoperable program analyzers for C. Most of the analyzers integrated in Frama-C rely on ACSL (ANSI/ISO C Specification Language), a specification language based on an axiomatic semantics for C [d09872c7].

Frama-C builds on the Why verification platform, a deductive program verification technology that implements Dijkstra's calculus of weakest preconditions. The typical workflow is:

  1. The C source is annotated with ACSL contracts.
  2. The annotated C code is translated by Why into an intermediate verification language.
  3. A verification condition (VC) generator produces the logical formulas that must be discharged.
  4. The VCs are dispatched to automatic provers or to interactive proof assistants such as Coq [d09872c7].

Use in Compiler Testing

Beyond program verification, axiomatic semantics has also been adapted for compiler testing. The PTE approach (2024) uses an axiomatic-semantics-based methodology in which a set of axioms is incrementally developed, each of the form (precondition, transformation, expectation) triple. These axioms are written in the same language whose compiler is under test, and can be derived from the language specification or by generalizing bug reports. PTE has been applied to the Cangjie and Java compilers, identifying 42 implementation bugs and 9 potential language design issues [arxiv:2401.01036v1].

Use in Structured Parallel Languages

In the design of structured parallel programming languages, axiomatic semantics is one of the three standard semantic frameworks adopted. The language PPL, designed for true concurrency, is given an explicit parallel operator together with operational, denotational, and axiomatic semantics, which together allow truly concurrent graphs to be reduced to a normal form that is amenable to compilation [arxiv:1810.13446v4].

Comparison with Operational Semantics

Operational semantics offers a more concrete, state-based alternative: program behavior is described as a transition relation between abstract states, and execution is modeled as a mathematical computation relation. Operational semantics is used in the CompCert formally verified C compiler to define execution of C programs. In the context of verifying an instruction-set simulator written in C against a formal architecture model, the authors of the Towards Verified Faithful Simulation work argue that operational semantics is more convenient than axiomatic semantics because the specification is large and requires abstraction mechanisms as well as an accurate definition of C features [d09872c7].

Notable Related Work

  • SEL4 verified operating system: verified using a different approach that did not employ an operational semantics of C, instead deducing proof obligations directly from the C code and treating the compiler and architecture as correct [d09872c7].
  • CompCert: uses operational semantics for the source, target, and intermediate languages of its certified compiler [d09872c7].
  • CerCo / CompCert evaluation order: Brian Campbell's work illustrates that the evaluation-order constraints in C are lax and not uniform [d09872c7].
  • Java bytecode verifier: formally proved by Cornelia Pusch [d09872c7].
  • ARM instruction set: formalized in HOL4 at Cambridge University to verify a gate-level implementation; the Towards Verified Faithful Simulation authors considered reusing it but ultimately based their work on CompCert C in Coq [d09872c7].

LINKED ENTITIES

2 links
Towards Verified Faithful Simulation MENTIONS
Frama-C USES

CITATIONS

6 sources
6 citations
[1] Axiomatic semantics and Hoare logic have been widely used for proving the correctness of programs. Towards Verified Faithful Simulation
[2] Frama-C is a framework for a set of interoperable program analyzers for C whose modules rely on ACSL, a specification language based on an axiomatic semantics for C. Towards Verified Faithful Simulation
[3] Frama-C leverages the Why verification platform, which implements Dijkstra's calculus of weakest preconditions; Why compiles annotated C code into an intermediate language whose VCs are dispatched to automatic or interactive (e.g., Coq) provers. Towards Verified Faithful Simulation
[4] Operational semantics describes program behavior as a transition relation between abstract states and is used in CompCert to define execution of (a subset of) C programs. Towards Verified Faithful Simulation
[5] PTE is an axiomatic-semantics-based compiler testing approach that incrementally develops (precondition, transformation, expectation) triples written in the language under test, and was applied to the Cangjie and Java compilers, finding 42 implementation bugs and 9 potential language design issues. PTE: Axiomatic Semantics based Compiler Testing
[6] The structured parallel programming language PPL for true concurrency is given an explicit parallel operator together with operational, denotational, and axiomatic semantics. Structured Parallel Programming