Nonstandard Axiomatic Semantics
2026-08-24 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors show that the usual way of describing how programs behave using axiomatic semantics and Hoare logic can have unexpected, nonstandard versions, meaning it doesn't always give a single, clear meaning to programs. To fix this, they suggest adding extra rules (proof obligations) to clarify the meaning. These extra rules work well with the standard ways of modeling program behavior and do not change existing proofs for these standard models.
Hoare logicaxiomatic semanticsoperational semanticsPeano arithmeticnonstandard modelsprogram verificationproof obligationstrace models
Authors
Patrick Cousot
Abstract
Similar to Skolem's nonstandard models of Peano's naturals, we show that axiomatic semantics based on Hoare logic has nonstandard models and so does not specify a unique, well-defined, and formal operational semantics of programming languages. We propose to enrich axiomatic semantics with additional proof obligations to solve this ambiguity problem. These proof obligations are always satisfied for standard trace models so that Hoare logic proofs are unchanged for these standard models.