💻 computer science

Cyclic Proofs in Hoare Logic and its Reverse

本文研究了标准霍are逻辑及其对偶（反向霍are逻辑）在部分正确性与完全正确性情形下，基于循环证明的公理系统与循环证明系统之间的关系，证明了这些循环系统的可靠性与相对完备性，并揭示了其循环性条件分别具有余归纳（部分正确性）和归纳（完全正确性）的本质特征。

原作者： James Brotherston, Quang Loc Le, Gauri Desai, Yukihiro Oda

发布于 2026-03-03

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： James Brotherston, Quang Loc Le, Gauri Desai, Yukihiro Oda

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文探讨的是如何更聪明、更自动化地证明计算机程序是“正确”的，或者找出它“哪里错了”。

为了让你轻松理解，我们可以把写代码和证明代码正确性想象成**“规划一次旅行”**。

1. 核心角色：两种“旅行指南”

在计算机科学里，我们通常用两种逻辑来检查程序：

霍逻辑 (Hoare Logic) —— “安全指南”
- 它的任务：保证如果你从起点（满足条件 P）出发，无论怎么走，只要程序停下来了，你一定会到达一个安全的终点（满足条件 Q）。
- 比喻：就像导游告诉你：“只要你在早上 8 点出发（P），无论路上遇到什么红绿灯，你肯定能在中午 12 点前到达酒店（Q）。”
- 两种模式：
  - 部分正确：只保证“如果你到了，那一定是酒店”。（如果车半路抛锚了，导游不管。）
  - 完全正确：保证“你不仅会到酒店，而且一定能按时到，不会无限期地堵车”。
反向霍逻辑 (Reverse Hoare Logic) / 错误逻辑 —— “寻宝指南”
- 它的任务：保证如果你从某个特定的终点（满足条件 Q）倒推回去，一定能找到一条路回到起点（满足条件 P）。或者换句话说，证明程序确实能产生某种特定的（可能是错误的）结果。
- 比喻：就像侦探说：“如果你发现酒店里有一具尸体（Q），那么肯定有人是从那个特定的入口（P）进来的。”或者在找 Bug 时：“如果你看到了这个崩溃画面（Q），那么肯定是因为你输入了那个特定的错误数据（P）。”

2. 传统方法的痛点：死记硬背的“路书”

传统的证明方法（公理系统）就像让你死记硬背一本厚厚的路书。

当你遇到一个循环（比如 while 循环，就像在迷宫里转圈）时，你必须先人工发明一个“不变式”（Loop Invariant）。
比喻：这就像你要证明“无论我在迷宫里转多少圈，我都能找到出口”。传统方法要求你先写下一句咒语（不变式），比如“我离出口的距离永远是偶数”，然后拿着这个咒语去证明。
问题：发明这个咒语非常难！就像让你凭空想出一个完美的数学公式来描述迷宫，这往往是自动化证明最大的拦路虎。

3. 论文的新方案：循环证明 (Cyclic Proofs) —— “边走边画地图”

这篇论文提出了一种新方法：循环证明。它不需要你提前发明咒语，而是允许你在证明过程中**“画圈”**。

核心思想：
- 与其提前想好咒语，不如直接把循环展开。
- 当你证明到一半，发现又回到了类似的情况，不要停下来，直接画一条线连回之前的某个步骤。这就形成了一个“循环”。
- 比喻：就像你在迷宫里走，每走一步就画在地图上。当你发现“哎？我又回到了刚才那个路口！”时，你不需要重新发明规则，直接说：“看，我画了个圈，只要这个圈是‘良性’的（不会无限死循环），我的证明就成立。”
如何保证安全（全局一致性条件）？
- 既然允许画圈，怎么保证不是死循环呢？论文引入了两个“安检员”：
  1. 对于“安全指南”（部分正确）：安检员要求，在这个无限循环的路径上，必须无限次地执行真正的代码动作（比如真的走了一步路）。如果只是在原地打转（没有执行代码），证明就无效。这确保了程序不会“假死”。
  2. 对于“完全正确”（必须终止）：安检员要求，在这个循环里，必须有一个数值在无限次地变小（比如离终点的距离从 100 变 99 变 98...）。因为自然数不能无限变小，所以程序一定会停下来。这保证了程序不会无限堵车。

4. 论文的两大贡献

对称之美：
- 作者发现，“安全指南”和“寻宝指南”在数学结构上是镜像对称的。
- 就像照镜子：左边的“部分正确”对应右边的“部分错误”；左边的“完全正确”对应右边的“完全错误”。
- 他们为这四种情况（部分/完全 x 正向/反向）都设计了一套统一的“画圈证明”规则。
自动化潜力：
- 因为不需要人工发明复杂的“不变式咒语”，只需要让计算机去“展开循环”并检查“数值是否变小”，这大大降低了自动化证明的难度。
- 论文证明了：只要传统方法能证明的，这种“画圈”的新方法也能证明（相对完备性）；而且只要“画圈”证明了，结果一定是真的（安全性）。

总结

想象一下，以前证明程序正确，就像让你先背下整本字典才能开始写文章（需要人工发明不变式）。
现在，这篇论文教你**“边写边查字典”，并且允许你引用自己刚才写过的句子**（循环证明），只要你能保证你的引用逻辑是通顺的（不会陷入死循环或无限递减）。

这种方法让计算机更容易自动地帮我们找 Bug（反向逻辑）或者证明代码没 Bug（正向逻辑），是迈向“全自动软件验证”的重要一步。

这是一份关于论文《Cyclic Proofs in Hoare Logic and its Reverse》（霍夫逻辑及其逆向逻辑中的循环证明）的详细技术总结。

1. 研究背景与问题 (Problem)

霍夫逻辑 (Hoare Logic) 是形式化验证程序正确性的基石，通常使用三元组 $\{P\} C \{Q\}$ 表示。

部分正确性 (Partial Correctness)：如果程序 $C$ 在满足前置条件 $P$ 的状态下终止，则结果状态满足 $Q$ 。
完全正确性 (Total Correctness)：程序 $C$ 在满足 $P$ 的状态下不仅终止，且结果满足 $Q$ 。

传统的公理化证明系统 (Axiomatic Proof Systems) 在处理循环（while 循环）时，要求证明者显式地构造循环不变式 (Loop Invariant)。对于完全正确性，还需要构造一个良基终止度量 (Well-founded Termination Measure)。

痛点：自动寻找合适的循环不变式和终止度量是程序验证中的主要难点，阻碍了自动化证明搜索。

逆向霍夫逻辑 (Reverse Hoare Logic, RHL) 及其扩展（如错误逻辑 Incorrectness Logic）关注的是“存在性”而非“不存在性”，即证明程序能够到达某些状态（三元组 $[P] C [Q]$ ）。

问题：现有的逆向逻辑研究主要集中在语义和公理化系统上，缺乏针对循环结构的循环证明 (Cyclic Proofs) 形式化系统。此外，霍夫逻辑与其逆向逻辑在证明论层面的对称性和关系尚未被系统地梳理。

核心问题：如何为部分/完全版本的霍夫逻辑及其逆向逻辑构建统一的循环证明系统？这些系统是否具备声性 (Soundness) 和相对完备性 (Relative Completeness)？它们之间存在怎样的对偶关系？

2. 方法论 (Methodology)

作者提出了一种基于循环证明 (Cyclic Proofs) 的框架，替代传统的公理化证明。

2.1 循环证明系统构建

基本结构：证明被表示为带有“后向链接 (backlinks)"的有限推导树（预证明，Pre-proof）。叶子节点（Bud）可以链接回树内部的节点（Companion），形成循环。
规则风格：采用延续风格 (Continuation Style)。规则结论形式为 $\{P\} C; C' \{Q\}$ ，即程序 $C$ 执行后接续 $C'$ 。
循环处理：
- 用单一的展开规则 (Unfolding Rule) 替代传统的循环不变式规则。
- 对于 while B do C，规则直接展开一次循环体，将剩余部分作为后续程序处理。
- 引入显式替换规则 (Substitution Rule) 以处理变量重命名和语法一致性。

2.2 全局声性条件 (Global Soundness Conditions)

为了证明带有循环的推导树是有效的，必须满足全局声性条件，防止无限循环推理：

部分正确性 (PHL/PRHL)：要求证明树中的每一条无限路径都必须包含无限多次的符号执行规则应用（Symbolic Execution Rules）。
- 直观含义：任何反例（程序执行不满足规范）必须对应一个无限长的执行序列，这在有限步骤的反例假设下是不可能的。
完全正确性 (THL/TRHL)：在部分正确性条件的基础上，要求每一条无限路径上存在一个无限进展的迹 (Infinitely Progressing Trace)。
- 迹 (Trace)：追踪前置条件中的良基度量值（如自然数）。
- 进展 (Progress)：在路径的某些点，度量值严格下降。
- 直观含义：任何反例（程序不终止或结果错误）必须导致度量值的无限下降序列，这与良基性矛盾。

2.3 对偶性分析

作者系统地分析了霍夫逻辑 (HL) 与逆向霍夫逻辑 (RHL) 之间的语义和证明论对偶关系：

语义对偶：部分逆向逻辑 (PRHL) 与完全霍夫逻辑 (THL) 互为对偶；完全逆向逻辑 (TRHL) 与部分霍夫逻辑 (PHL) 互为对偶。
证明论对称：部分版本的逻辑共享相似的声性条件（基于无限执行），完全版本的逻辑共享相似的声性条件（基于良基下降）。

3. 主要贡献 (Key Contributions)

统一的循环证明系统：
- 首次为部分和完全版本的霍夫逻辑及其逆向逻辑（包括 PRHL 和 TRHL）构建了统一的循环证明系统。
- 展示了这些系统仅通过不同的全局声性条件来区分部分/完全正确性，而核心推理规则是共享的。
声性 (Soundness) 证明：
- 通过直接论证证明了所有四个系统（PHL, THL, PRHL, TRHL）的循环证明系统是声的。
- 证明了如果存在循环证明，则不存在反例（对于部分逻辑，反例需无限执行；对于完全逻辑，反例需导致无限下降序列）。
相对完备性 (Relative Completeness)：
- 证明了从标准公理化证明到循环证明的显式转换。
- 如果三元组在标准公理化系统中可证，则必然存在一个对应的循环证明。
- 转换过程通过结构归纳法实现，将标准证明中的循环不变式规则转换为循环证明中的后向链接和迹。
理论关系的澄清：
- 揭示了霍夫逻辑与逆向逻辑在证明论层面的深刻对称性。
- 指出逆向逻辑中的“部分”版本（PRHL）在文献中较少见，本文将其定义为完全正确性的语义对偶，并建立了其形式化基础。

4. 关键结果 (Results)

定理 4.7 & 5.5 (声性)：
- 若 $\{P\} C \{Q\}$ 在 PHL/THL 中有循环证明，则其在语义上有效。
- 若 $[P] C [Q]$ 在 PRHL/TRHL 中有循环证明，则其在语义上有效。
定理 4.9 & 5.7 (相对完备性)：
- 若 $\{P\} C \{Q\}$ 在标准 PHL/THL 中可证，则它在循环 PHL/THL 中可证。
- 若 $[P] C [Q]$ 在标准 PRHL/TRHL 中可证，则它在循环 PRHL/TRHL 中可证。
- 注：对于 PRHL 的相对完备性，作者指出目前尚未完全确立（依赖于逻辑蕴含的 Oracle），但高度可信。
转换机制：
- 成功构建了从标准证明树到循环预证明树的转换算法，确保了转换后的结构满足全局声性条件（如迹的进展性）。

5. 意义与影响 (Significance)

自动化验证的潜力：
- 循环证明系统消除了对人工构造循环不变式和终止度量的依赖。这使得自动定理证明器（如 Cyclist）能够更自然地处理循环程序，通过搜索循环结构而非猜测不变式来验证程序。
统一理论框架：
- 本文提供了一个统一的视角，将霍夫逻辑（关注“无坏行为”）和逆向/错误逻辑（关注“有特定行为”）纳入同一个循环证明框架。这有助于理解程序验证中“安全性”与“活性”性质的对偶关系。
逆向逻辑的形式化推进：
- 为逆向霍夫逻辑（特别是部分逆向逻辑 PRHL）提供了首个循环证明形式化，填补了该领域在证明论方面的空白，为基于错误逻辑的自动漏洞检测提供了新的理论基础。
未来工作方向：
- 论文建议将这些系统实现到现有的定理证明平台（如 Cyclist）中。
- 探索将循环证明原则扩展到更复杂的程序特性（如并发、分离逻辑）中。

总结：这篇论文通过引入循环证明技术，成功地将霍夫逻辑及其逆向逻辑的公理化系统转化为更易于自动化处理的循环系统，并严格证明了其声性和完备性。这项工作不仅简化了循环验证的理论基础，还揭示了程序正确性验证中不同逻辑体系之间深刻的对称性。