2025年9月23日·1 分钟
托尼·霍尔的正确性思想：从逻辑到安全代码
了解托尼·霍尔关于霍尔逻辑、快速排序与安全思维的工作如何塑造了编写和审查正确软件的实用技术。
了解托尼·霍尔关于霍尔逻辑、快速排序与安全思维的工作如何塑造了编写和审查正确软件的实用技术。
当人们说一个程序“正确”时，他们常常的意思是：“我跑了几次，输出看起来没问题。”这是个有用的信号——但这并不是正确性。从直白的角度看，正确性意味着程序满足它的规范：对于每一个允许的输入，它产生所需的结果，并遵守关于状态变更、时间和错误处理的规则。
问题在于，“满足规范”比听起来难得多。
首先，规范通常模糊不清。产品需求可能写着“对列表排序”，但这是不是稳定排序？重复值、空列表或非数字项怎么办？如果规范没说明，不同的人会做不同假设。
其次，边界情况并不罕见——只是测试得少。空值、溢出、越界、异常的用户操作序列和外部失败都会把“看起来能用”变成“在生产中崩了”。
第三，需求会变化。相对于昨天的规范代码可能是正确的，相对于今天的规范则可能不正确。
托尼·霍尔的主要贡献并不是主张我们事事都做形式证明，而是提出：我们可以更精确地描述代码应做什么，并以有纪律的方式推理。
在这篇文章里，我们会沿着三条相关线索展开：
大多数团队不会写完整的形式证明。但即使是部分的、“证明式”的思考也能让缺陷更易被发现、评审更犀利、行为在代码发布前更清晰。
托尼·霍尔是少数那些研究成果没有停留在论文或课堂里的计算机科学家之一。他在学界与产业间穿梭，关注一个每个团队仍在面对的实用问题：我们如何知道一个程序确实做了我们以为它做的事——尤其当利害关系很高时？
本文聚焦几条在真实代码库中经常出现的霍尔思想：
{P} C {Q} 来描述程序行为。你不会在这里看到深奥的数学形式主义，也不会尝试给快速排序做完整的机器可检验证明。目标是保持概念可接近：提供足够的结构以让你的推理更清楚，而不会把代码审查变成研究生研讨会。
霍尔的思想体现在诸多平常决策中：函数依赖了哪些假设、向调用者保证了什么、中途循环必须保持什么、以及如何在评审中发现“几乎正确”的改动。即便你从不显式写出 {P} C {Q}，以这种结构思考也会改进 API、测试和关于棘手代码的讨论质量。
霍尔的观点比“通过几个例子”更严格：正确性关乎达成一致的承诺，而不是在少量样本上看起来没问题。
错误常常在于团队跳过中间步骤：直接从需求写到代码，使“承诺”变得模糊。
经常被混淆的两种宣称：
对真实系统来说，“永远不结束”可能和“给出错误答案”一样有害。
正确性声明从来不是普适的；它们依赖于关于：
把假设说清楚，会把“在我机器上可以跑”变成别人也能推理的东西。
考虑函数 sortedCopy(xs)。
一个有用的规范可以是：“返回一个新列表 ys，满足 (1) ys 按升序排序，(2) ys 与 xs 含有完全相同的元素（计数相同），(3) xs 未被修改。”
现在“正确”意味着代码在声明的假设下满足这三点——而不仅仅是输出看起来有序。
霍尔逻辑是一种用合同式语言谈论代码的方法：如果你的初始状态满足某些假设，运行这段代码后，系统会到达满足某些保证的状态。
核心记法是霍尔三元组：
{precondition} program {postcondition}
前置条件陈述在程序片段运行前必须为真的内容。它不是你“希望”成立，而是代码“需要”成立的条件。
示例：假设一个函数在没有溢出检查的情况下返回两数的平均值。
a + b 能在该整数类型内表示avg = (a + b) / 2avg 等于 a 和 b 的数学平均值如果前置条件不成立（可能溢出），后置条件的保证就不适用。三元组迫使你把这点说清楚。
后置条件陈述在代码运行后会为真的内容——假设前置条件成立。好的后置条件是具体且可检验的。不要写“结果有效”，而要说明“有效”具体指什么：已排序、非负、在界内、除特定字段外未改动等。
霍尔逻辑可以从微小语句扩展到多步代码：
x = x + 1 之后关于 x 的什么事实成立？重点不是到处加花括号，而是让意图可读：清楚的假设、清楚的结果，审查时少一些“看起来能用”的争论。
循环不变式是在循环开始前为真、在每次迭代后保持为真并在循环结束时仍为真的陈述。这个简单想法能带来很大回报：它把“看起来能用”替换为每步都可检查的断言。
没有不变式，审查常常听起来像：“我们遍历列表并逐步修复。”不变式强制精确：现在到底有什么已经是正确的，即便循环还没结束？一旦你能清楚地说出这一点，越界和遗漏等错误就更容易显现，因为它们会在某次迭代时破坏不变式。
日常代码大多能用几类可靠模板。
1) 边界 / 索引安全
保持索引在安全范围内。
0 <= i <= nlow <= left <= right <= high这类不变式对防止越界访问和让数组推理更具体非常有用。
2) 已处理 vs 未处理的项
将数据分成“已完成”区域和“未完成”区域。
a[0..i) 中的所有元素已被检查。”result 的每个项都满足过滤谓词。”这把模糊的进展变成了关于当前“已处理”到底是什么的清晰契约。
3) 已排序的前缀（或已分区的前缀）
常见于排序、合并和划分。
a[0..i) 已排序。”a[0..i) 中的所有元素都 <= pivot，而 a[j..n) 中的所有元素都 >= pivot。”即便整个数组未排序，你也能钉住已知的部分。
正确性不仅仅是“正确”，循环还必须结束。一个简单的论证方法是给出一个度量（通常称为变元），每次迭代该度量都会变小且不可能无限减小。
示例：
n - i 每次减 1。”如果找不到收缩的度量，你可能发现了真正的风险：某些输入会导致无限循环。
快速排序的承诺很简单：给定一个片段（或数组区间），重新排列其元素使之按非降序排列，且不丢失或凭空产生任何值。算法的高层结构也易于总结：
它是一个很好的教学示例：足够小可以记住，但又足够丰富，能展示非形式推理何时失效。一个在随机测试下“看起来能用”的快速排序仍可能在特定输入或边界条件下出错。
几个问题导致大多数错误：
用霍尔风格推理，通常把证明分成两部分：
这种分离使推理更可管理：先把分区做好，再在其上构建排序的正确性。
快速排序的速度依赖于一个看似微小的例程：partition。如果 partition 有一丁点错误，快速排序可能排序错、永远递归或在边界上崩溃。
我们将使用经典的 Hoare 分区方案（两个指针向内移动）。
输入： 数组切片 A[lo..hi] 和选定的 pivot 值（通常是 A[lo]）。
输出： 一个索引 p，使得：
A[lo..p] 中的每个元素都 <= pivotA[p+1..hi] 中的每个元素都 >= pivot注意未保证的一点：基准不一定会最后落在位置 p，且等于基准的元素可以出现在任一侧。那也没关系——快速排序只需要一个正确的分割。
当算法推进两个索引——从左边的 i 和从右边的 j——良好的推理关注那些已经“固定”的部分。一个实用的不变式集合是：
A[lo..i-1] 中所有元素都 <= pivot（左侧已清理）A[j+1..hi] 中所有元素都 >= pivot（右侧已清理）A[i..j] 中的一切都是未分类（尚待检查）当我们发现 A[i] > pivot 且 A[j] < pivot 时，交换它们会保持这些不变式并缩小未分类的中间区间。
i 向右运行；分区仍需终止并返回合理的 p。j 向左运行；同样要关注终止。< 与 <= 混用），指针会停滞。Hoare 的方案依赖一致的规则以保证进展。存在不同的分区方案（Lomuto、Hoare、三路分区）。关键是选定一种、明确其契约，并在审查时始终以该契约为准。
当你能清楚回答两个问题时，递归最容易令人信任：**何时停止？和为什么每一步都是有效的？**霍尔式思考有助于强制你陈述在调用之前必须为真和返回后将为真的内容。
递归函数需要至少一个基例，它不再做递归调用且仍满足承诺。
对排序而言，典型基例是“长度为 0 或 1 的数组已经有序”。这里“有序”应显式说明：对于排序关系 ≤，若对任意索引 i < j，都有 a[i] ≤ a[j]，则数组被认为已排序。（是否保持相等元素的原始相对顺序是“稳定性”的问题；快速排序通常不是稳定的，除非特别设计。）
每一步递归应在严格更小的输入上调用自己。这个“缩小”是终止的论证：如果大小在递归中减小且不可能低于 0，就不可能无限递归。
缩小也关乎栈安全。即便代码正确，如果递归深度过深也会崩溃。在快速排序中，不平衡的分区会导致深递归。这既是终止证明的内容，也是提醒在实际中考虑最坏深度的提示。
快速排序在极端不平衡分区时最坏时间复杂度会降到 O(n²)，但这是性能问题，不是正确性问题。推理目标是：假设分区保全元素并按基准分割，子区间排序正确则整体有序。
测试与证明式思维都旨在提高信心，但路径不同。
测试擅长捕捉具体错误：越界、遗漏边界、回归等。但测试套件只能对输入空间进行采样。即便“覆盖率 100%”也不意味着“所有行为都被检查”；它更多意味着“所有行都被执行”。
证明式思维（尤其是霍尔式推理）从规范出发，问：当满足这些前置条件时，代码是否总能建立后置条件？做好后，你不仅能发现一个缺陷，通常还能排除某一整类缺陷（比如“数组访问保持在界内”或“循环从未破坏分区属性”）。
清晰的规范本身就是测试生成器。
如果你的后置条件写着“输出已排序且是输入的置换”，你会自动得到测试想法：
<= pivot 在左侧）规范告诉你什么叫“正确”，测试则检查现实是否与之匹配。
基于属性的测试介于证明与示例之间。不是手工挑选少数用例，而是声明属性并让工具生成大量输入。
对于排序，两个简单属性效果显著：
这些属性本质上是可执行的后置条件检查。
一个可伸缩的轻量流程：
如果想制度化此流程，可以把“规范 + 推理说明 + 测试”放到 PR 模板或代码审查清单中（另见 /blog/code-review-checklist）。
如果你使用基于对话生成代码的工作流（从聊天接口生成代码），相同的纪律更重要。在 Koder.ai 中，例如，可以在 Planning Mode 先钉死前置/后置条件再生成代码，同时用快照和回滚和基于属性的测试迭代。工具能加速实现，但规范仍然是防止“快”变“脆弱”的关键。
正确性不仅关乎“程序返回正确值”。安全思维问一个不同的问题：哪些结果是不可接受的，我们如何在代码受压、被误用或部分失败时仍防止它们发生？实践中，安全就是在正确性上加一层优先级：有些失败只是烦人，有些失败会造成经济损失、隐私泄露或人身伤害。
缺陷 是代码或设计中的错误。危害 是可能导致不可接受结果的情形。一个缺陷在一个上下文可能无害，在另一个上下文可能危险。
例如：相册应用中的一次越界一位错误可能只会把图片错位；但同样的错误出现在药物剂量计算器中可能会伤人。安全思维要求你把代码行为与实际后果联系起来，而不仅仅看是否满足规范。
不需要重度形式方法就能立刻提升安全性。团队可以采用可重复的小实践：
这些技术天然契合霍尔式推理：把前置条件显式化（哪些输入可接受），并将后置条件包含安全属性（不能发生的事）。
面向安全的检查会有成本——CPU 时间、复杂度或偶发的误拒绝。
安全思维不在于证明优雅，而在于防止你无法承受的失效模式。
代码审查是正确性思维最快见效的地方，因为你可以在缺陷到达生产前就发现缺少的假设。霍尔的核心动作——说明“运行前必须为真”和“运行后将为真”——可以直接转化为审查问题。
阅读变更时，尝试把每个关键函数当成一个小承诺：
一个简单的审查习惯：如果你不能用一句话说出前/后条件，这段代码很可能需要更清晰的结构。
对有风险或核心的函数，在签名上方加一段小的契约注释。保持具体：输入、输出、副作用与错误。
def withdraw(account, amount):
"""Contract:
Pre: amount is an integer > 0; account is active.
Post (success): returns new_balance; account.balance decreased by amount.
Post (failure): raises InsufficientFunds; account.balance unchanged.
"""
...
这些注释不是形式证明，但它们给审查者提供了可检验的精确信息。
当代码处理以下内容时要格外明确：
若变更触及这些内容，问：“前置条件是什么，在哪里被强制执行？”以及“即便发生错误，我们提供了哪些保证？”
形式推理不必把整个代码库变成数学论文。目标是在价值最大的地方投入额外确定性：那些仅靠“测试看起来没问题”不够的地方。
当你有一个小且关键的模块（认证、支付规则、权限、安全联锁），或一个棘手的算法（越界难查的解析器、调度器、缓存/淘汰、并发原语、类似分区的代码、边界密集的数据转换）时，形式方法很合适。
一个实用规则：如果一个 bug 会造成真实伤害、重大金钱损失或静默的数据损坏，你应该使用超过普通审查+测试的手段。
可以从“轻量级”到“重量级”选择，通常组合使用效果更好：
按下列权衡决定形式化深度：
在实践中，也可以把“形式化”看作渐进过程：先写明契约与不变式，再用自动化工具监督这些约束。
对于使用 Koder.ai 快速生成前端、后端与数据库模式的团队来说，快照/回滚与源码导出能让你在快速迭代同时，通过测试和静态分析在 CI 中执行契约，保持较高保证。
在规划或代码审查中把这个作为“是否应当形式化更多？”的门槛：
延伸阅读主题：契约式设计、基于属性的测试、状态机的模型检查、针对你所用语言的静态分析器，以及形式化证明工具和规范的入门材料。
正确性意味着程序满足一个达成共识的规范：对于每一个允许的输入和相关的系统状态，它产生期望的输出与副作用（并按承诺处理错误）。“看起来能用”通常只是你检查了几个例子，而不是整个输入空间或棘手的边界条件。
需求是业务目标（“为展示对列表进行排序”）。规范是可精确检验的承诺（“返回一个按升序排序的新列表，元素的多重集合与输入相同，且不修改输入”）。实现是你写的代码。错误常在于团队直接从需求跳到实现，而没有写出可检验的规范。
部分正确性：如果代码返回，则结果是正确的。完全正确性：代码会返回且结果正确 —— 因此终止是声明的一部分。
在实际中，当“永远不返回”是用户可见的失败、资源泄漏或安全风险时，完全正确性就很重要。
霍尔三元组 {P} C {Q} 可以这样读：
P（前置条件）：在运行 C 之前必须为真的条件C：代码片段前置条件是代码需要的东西（例如“索引在范围内”、“元素可比较”、“已持有锁”）。如果调用方可能违反前置条件，要么：
否则，后置条件只是美好的愿望，而非可信保证。
循环不变式是在循环开始之前为真、在每次迭代后保持为真并且在循环结束时仍然为真的陈述。常用模板包括：
0 <= i <= n）如果你无法表述不变式，说明循环在一次做太多事或边界不清楚。
通常给出一个度量（变元），每次迭代该度量都会减小且不可能无限减小，例如：
n - i 每次减 1如果找不到这样的度量，你可能发现了真实的非终止风险（尤其在存在重复或指针停滞时）。
在快速排序中，partition 是所有工作依赖的小例程。如果 partition 稍有错误，你可能会得到：
因此最好明确 partition 的契约：左侧和右侧各自应满足的关系，并保证仅对元素进行重排（是一个置换）。
重复元素与“等于 pivot”的处理是常见来源。实践规则：
当重复很多时，三路分区既能减少错误，也能降低递归深度。
测试擅长发现具体错误：越界、少处理的边界、回归。但测试只能采样输入空间。证明式思维（如霍尔风格）则从规范出发，问：在这些前置条件下，代码是否总能建立后置条件？良好地做这件事可以排除整类错误（如数组访问越界或保持不变式）。
一个实用的混合流程：
对于排序，两条高价值属性是：
QCP你不必在代码里写出符号——在审查时用“先决条件进来，保证条件出来”的结构就是实用收获。