公理语义与程序逻辑

公理语义通过对程序状态的逻辑断言来刻画程序，其中霍尔逻辑及其后续理论提供了证明程序正确性的规则。

Definition

公理语义通过程序执行前后成立的逻辑断言来指定程序的含义，而程序逻辑是用于证明程序相关断言的推理规则的演绎系统。

Scope

本主题涵盖通过逻辑断言对程序进行推理：霍尔三元组（将前置条件、程序和后置条件关联起来）；迪杰斯特拉的谓词变换器和最弱前置条件；以及用于处理可变、共享堆状态程序的“分离逻辑”。它涉及部分正确性与完全正确性、循环不变式，以及程序逻辑的可靠性与完备性。

Core questions

• 如何证明程序相对于规范是正确的？
• 什么是循环不变式，为什么它对验证至关重要？
• 谓词变换器如何计算正确性所需的条件？
• 如何对修改共享堆内存的程序进行模块化推理？

Key theories

霍尔逻辑

霍尔引入了一个关于三元组 {P} C {Q} 的公理推理系统，提供了一种组合方法来证明程序符合其规范。

最弱前置条件与卫式命令

迪杰斯特拉的谓词变换器语义定义了保证程序达到后置条件的最弱前置条件，支持系统地推导出正确的程序。

分离逻辑

雷诺兹和奥赫恩通过引入分离合取扩展了霍尔逻辑，从而能够对操作共享可变数据结构和指针的程序进行局部、模块化的推理。

Clinical relevance

程序逻辑是演绎程序验证的支柱，用于证明关键软件正确性的工具以及操作系统和编译器组件的机械化证明中。特别是分离逻辑，使得指针操作代码的可扩展验证成为可能。

History

弗洛伊德1967年为流程图赋予意义的方法和霍尔1969年的公理基础奠定了该领域的基础。迪杰斯特拉在20世纪70年代提出的最弱前置条件演算将验证与程序推导联系起来。雷诺兹和奥赫恩在2000年左右提出的分离逻辑，为堆操作代码的程序逻辑注入了新的活力，从而催生了强大的现代验证框架。

Debates

验证工作量与保证程度

一个长期存在的问题是如何平衡编写规范和不变式所需的大量手动工作与演绎验证提供的强大正确性保证，这促使了自动化和更轻量级方法的发展。

Key figures

• C. A. R. Hoare
• Robert Floyd
• Edsger Dijkstra
• John Reynolds
• Peter O'Hearn

Seminal works

• hoare1969
• dijkstra1975
• reynolds2002
• floyd1967

Frequently asked questions

什么是霍尔三元组？

霍尔三元组 {P} C {Q} 断言，如果在执行命令 C 之前前置条件 P 成立，那么之后后置条件 Q 成立（对于部分正确性，前提是 C 终止）。

为什么分离逻辑很重要？

分离逻辑允许证明独立地对堆的不同区域进行推理，从而使得以模块化方式验证带有指针和共享可变状态的程序成为可能。