AI 中文总结
本文证明基于霍尔逻辑的公理语义存在非标准模型，无法唯一确定编程语言的操作语义，故提出补充额外证明义务的方法来解决歧义，且该方法不改变标准轨迹模型下的霍尔逻辑证明。
AI 中文摘要
类似司寇伦（Skolem）对皮亚诺自然数的非标准模型，本文证明基于霍尔逻辑（Hoare logic）的公理语义存在非标准模型，因此无法唯一、明确且形式化地定义编程语言的操作语义。我们建议通过补充额外的证明义务来丰富公理语义，以解决这种歧义问题；这些证明义务对于标准轨迹模型始终成立，因此霍尔逻辑在这些标准模型下的证明保持不变。
英文摘要
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.
CommentsICTAC 2026
