托尼·霍尔的正确性思想：从逻辑到安全代码

为什么“正确性”不等于“看起来能用”

当人们说一个程序“正确”时，他们常常的意思是：“我跑了几次，输出看起来没问题。”这是个有用的信号——但这并不是正确性。从直白的角度看，正确性意味着程序满足它的规范：对于每一个允许的输入，它产生所需的结果，并遵守关于状态变更、时间和错误处理的规则。

问题在于，“满足规范”比听起来难得多。

为什么正确性是真正困难的

首先，规范通常模糊不清。产品需求可能写着“对列表排序”，但这是不是稳定排序？重复值、空列表或非数字项怎么办？如果规范没说明，不同的人会做不同假设。

其次，边界情况并不罕见——只是测试得少。空值、溢出、越界、异常的用户操作序列和外部失败都会把“看起来能用”变成“在生产中崩了”。

第三，需求会变化。相对于昨天的规范代码可能是正确的，相对于今天的规范则可能不正确。

本文其余部分你会看到什么

托尼·霍尔的主要贡献并不是主张我们事事都做形式证明，而是提出：我们可以更精确地描述代码应做什么，并以有纪律的方式推理。

在这篇文章里，我们会沿着三条相关线索展开：

• 霍尔逻辑：用前置条件和后置条件做轻量、结构化的推理。
• 快速排序：一个熟悉的算法，展示像划分这样的“显而易见”小步骤需要仔细思考。
• 安全思维：把正确性当作在失败带来实质后果时的实用责任。

大多数团队不会写完整的形式证明。但即使是部分的、“证明式”的思考也能让缺陷更易被发现、评审更犀利、行为在代码发布前更清晰。

托尼·霍尔简述：影响日常代码的思想

托尼·霍尔是少数那些研究成果没有停留在论文或课堂里的计算机科学家之一。他在学界与产业间穿梭，关注一个每个团队仍在面对的实用问题：我们如何知道一个程序确实做了我们以为它做的事——尤其当利害关系很高时？

本文关注的重要贡献

本文聚焦几条在真实代码库中经常出现的霍尔思想：

• 霍尔逻辑：用前置条件、后置条件和闻名的霍尔三元组 {P} C {Q} 来描述程序行为。
• 循环不变式：对循环进行比“我本地跑过”更有纪律的推理。
• 快速排序（尤其是它的划分步骤）：一个著名例子，说明精确的正确性陈述带来的澄清效果。
• 安全思维：把正确性视为非奢侈品；当失败会带来现实后果时，它可能是区分不便与伤害的关键。

本文不会做什么

你不会在这里看到深奥的数学形式主义，也不会尝试给快速排序做完整的机器可检验证明。目标是保持概念可接近：提供足够的结构以让你的推理更清楚，而不会把代码审查变成研究生研讨会。

为什么这些工作会影响日常编程

霍尔的思想体现在诸多平常决策中：函数依赖了哪些假设、向调用者保证了什么、中途循环必须保持什么、以及如何在评审中发现“几乎正确”的改动。即便你从不显式写出 {P} C {Q}，以这种结构思考也会改进 API、测试和关于棘手代码的讨论质量。

正确性在实践中的含义

霍尔的观点比“通过几个例子”更严格：正确性关乎达成一致的承诺，而不是在少量样本上看起来没问题。

需求、规范与实现的区别

• 需求 是业务上的目标（以自然语言描述的利益相关者想要什么）。
• 规范 是该需要的精确、可检验版本（函数必须做什么）。
• 实现 是你写的代码（它如何做到）。

错误常常在于团队跳过中间步骤：直接从需求写到代码，使“承诺”变得模糊。

部分正确性 vs 完全正确性

经常被混淆的两种宣称：

• 部分正确性：如果代码返回，结果就是正确的。
• 完全正确性：代码会返回，且结果正确。（因此终止也是声明的一部分）

对真实系统来说，“永远不结束”可能和“给出错误答案”一样有害。

正确性总是依赖假设

正确性声明从来不是普适的；它们依赖于关于：

• 输入（例如列表能装进内存，元素可比较）
• 约束（例如时间限制、整数范围）
• 环境（例如并发、I/O 失败、配置）

把假设说清楚，会把“在我机器上可以跑”变成别人也能推理的东西。

一个小示例规范

考虑函数 sortedCopy(xs)。

一个有用的规范可以是：“返回一个新列表 ys，满足 (1) ys 按升序排序，(2) ys 与 xs 含有完全相同的元素（计数相同），(3) xs 未被修改。”

现在“正确”意味着代码在声明的假设下满足这三点——而不仅仅是输出看起来有序。

霍尔逻辑基础：前置条件、后置条件、三元组

霍尔逻辑是一种用合同式语言谈论代码的方法：如果你的初始状态满足某些假设，运行这段代码后，系统会到达满足某些保证的状态。

核心记法是霍尔三元组：

{precondition} program {postcondition}

前置条件：你假设了什么

前置条件陈述在程序片段运行前必须为真的内容。它不是你“希望”成立，而是代码“需要”成立的条件。

示例：假设一个函数在没有溢出检查的情况下返回两数的平均值。

• 前置条件：a + b 能在该整数类型内表示
• 程序：avg = (a + b) / 2
• 后置条件：avg 等于 a 和 b 的数学平均值

如果前置条件不成立（可能溢出），后置条件的保证就不适用。三元组迫使你把这点说清楚。

后置条件：你保证了什么

后置条件陈述在代码运行后会为真的内容——假设前置条件成立。好的后置条件是具体且可检验的。不要写“结果有效”，而要说明“有效”具体指什么：已排序、非负、在界内、除特定字段外未改动等。

赋值与顺序（不需过多符号）

霍尔逻辑可以从微小语句扩展到多步代码：

• 赋值 精确地改变状态。推理要问：在 x = x + 1 之后关于 x 的什么事实成立？
• 顺序（先做这个再做那个）把保证串联起来：如果步骤 1 建立了步骤 2 的前置条件，那么整个块更容易信任。

重点不是到处加花括号，而是让意图可读：清楚的假设、清楚的结果，审查时少一些“看起来能用”的争论。

团队可写的循环不变式

循环不变式是在循环开始前为真、在每次迭代后保持为真并在循环结束时仍为真的陈述。这个简单想法能带来很大回报：它把“看起来能用”替换为每步都可检查的断言。

为什么不变式阻止含糊推理

没有不变式，审查常常听起来像：“我们遍历列表并逐步修复。”不变式强制精确：现在到底有什么已经是正确的，即便循环还没结束？一旦你能清楚地说出这一点，越界和遗漏等错误就更容易显现，因为它们会在某次迭代时破坏不变式。

可复用的不变式模板

日常代码大多能用几类可靠模板。

1) 边界 / 索引安全

保持索引在安全范围内。

• 0 <= i <= n
• low <= left <= right <= high

这类不变式对防止越界访问和让数组推理更具体非常有用。

2) 已处理 vs 未处理的项

将数据分成“已完成”区域和“未完成”区域。

• “a[0..i) 中的所有元素已被检查。”
• “移动到 result 的每个项都满足过滤谓词。”

这把模糊的进展变成了关于当前“已处理”到底是什么的清晰契约。

3) 已排序的前缀（或已分区的前缀）

常见于排序、合并和划分。

• “a[0..i) 已排序。”
• “a[0..i) 中的所有元素都 <= pivot，而 a[j..n) 中的所有元素都 >= pivot。”

即便整个数组未排序，你也能钉住已知的部分。

以通俗方式论证终止：一个会收缩的度量

正确性不仅仅是“正确”，循环还必须结束。一个简单的论证方法是给出一个度量（通常称为变元），每次迭代该度量都会变小且不可能无限减小。

示例：

• “n - i 每次减 1。”
• “未处理项的数量在减少。”

如果找不到收缩的度量，你可能发现了真正的风险：某些输入会导致无限循环。

用快速排序作为关于代码推理的案例研究

快速排序的承诺很简单：给定一个片段（或数组区间），重新排列其元素使之按非降序排列，且不丢失或凭空产生任何值。算法的高层结构也易于总结：

1. 选择一个 pivot（基准） 值。
2. 划分 区间，使“小于基准”的元素移到一侧，“大于基准”的元素移到另一侧（对“等于”的处理有规则）。
3. 对左右子区间 递归。

它是一个很好的教学示例：足够小可以记住，但又足够丰富，能展示非形式推理何时失效。一个在随机测试下“看起来能用”的快速排序仍可能在特定输入或边界条件下出错。

会破坏“显然正确”实现的陷阱

几个问题导致大多数错误：

• 重复元素：如果分区对“等于基准”的处理不一致，可能导致无限递归（子区间不缩小）或分区自身的规则被破坏。
• 空区间或单元素区间：基例必须精确，否则会越界或无限递归。
• 越界一位错误：分区常用两个指针；一次错误的比较或递增可能跳过元素或在区间外交换。

实际上需要证明的是什么

用霍尔风格推理，通常把证明分成两部分：

• 分区正确性：分区后，左边的每个元素都满足与基准的选定关系，右边的每个元素满足相反关系，并且结果是原始元素的一个置换。
• 递归正确性：递归调用作用于严格更小的区间（终止性），并且在假设它们能把子区间排序的前提下，整体区间最终有序。

这种分离使推理更可管理：先把分区做好，再在其上构建排序的正确性。

划分正确性：快速排序的核心

快速排序的速度依赖于一个看似微小的例程：partition。如果 partition 有一丁点错误，快速排序可能排序错、永远递归或在边界上崩溃。

分区契约（必须保证的内容）

我们将使用经典的 Hoare 分区方案（两个指针向内移动）。

输入： 数组切片 A[lo..hi] 和选定的 pivot 值（通常是 A[lo]）。

输出： 一个索引 p，使得：

• A[lo..p] 中的每个元素都 <= pivot
• A[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 在左侧）
• 无效输入：null、NaN、越界索引、不一致的比较器

规范告诉你什么叫“正确”，测试则检查现实是否与之匹配。

基于属性的测试作为实践桥梁

基于属性的测试介于证明与示例之间。不是手工挑选少数用例，而是声明属性并让工具生成大量输入。

对于排序，两个简单属性效果显著：

• 已排序性： 结果按非降序排列。
• 置换性： 结果包含与输入完全相同的元素（计数相同）。

这些属性本质上是可执行的后置条件检查。

团队可用的工作流

一个可伸缩的轻量流程：

1. 先写规范（前置条件、后置条件、关键不变式）。
2. 推理棘手部分（循环、分区、递归边界）。
3. 把规范变成测试（边界用例 + 基于属性的检查）。
4. 将它们与代码和审查捆绑在一起，以免未来改动暗中违反初始意图。

如果想制度化此流程，可以把“规范 + 推理说明 + 测试”放到 PR 模板或代码审查清单中（另见 /blog/code-review-checklist）。

如果你使用基于对话生成代码的工作流（从聊天接口生成代码），相同的纪律更重要。在 Koder.ai 中，例如，可以在 Planning Mode 先钉死前置/后置条件再生成代码，同时用快照和回滚和基于属性的测试迭代。工具能加速实现，但规范仍然是防止“快”变“脆弱”的关键。

安全思维：带现实后果的正确性

正确性不仅关乎“程序返回正确值”。安全思维问一个不同的问题：哪些结果是不可接受的，我们如何在代码受压、被误用或部分失败时仍防止它们发生？实践中，安全就是在正确性上加一层优先级：有些失败只是烦人，有些失败会造成经济损失、隐私泄露或人身伤害。

危害 vs 缺陷：为何影响力重要

缺陷 是代码或设计中的错误。危害 是可能导致不可接受结果的情形。一个缺陷在一个上下文可能无害，在另一个上下文可能危险。

例如：相册应用中的一次越界一位错误可能只会把图片错位；但同样的错误出现在药物剂量计算器中可能会伤人。安全思维要求你把代码行为与实际后果联系起来，而不仅仅看是否满足规范。

防止最坏结果的简单技术

不需要重度形式方法就能立刻提升安全性。团队可以采用可重复的小实践：

• 失败安全的默认值： 当系统无法确信时，选择更安全的行为。例如授权检查出错时选择“拒绝”而不是“允许”。
• 在边界处校验输入： 把用户输入、文件内容和网络数据当作不可信。尽早验证类型、范围、格式和不变式。
• 限制与超时： 限制内存使用、请求大小、递归深度、重试次数和执行时间。许多事故是“正确”的代码在不合理输入下运行的结果。

这些技术天然契合霍尔式推理：把前置条件显式化（哪些输入可接受），并将后置条件包含安全属性（不能发生的事）。

权衡：校验并非免费

面向安全的检查会有成本——CPU 时间、复杂度或偶发的误拒绝。

• 性能 vs 校验： 快路径有价值，但关键边界值得做校验、限流与超时。
• 严格 vs 可用性： 拒绝所有不完美输入会让用户受挫；接受一切又可能造成模糊和滥用。实用的折中是“核心严格，边缘宽容”，同时记录并衡量边缘情况的发生频率。

安全思维不在于证明优雅，而在于防止你无法承受的失效模式。

在代码审查中应用霍尔式推理

代码审查是正确性思维最快见效的地方，因为你可以在缺陷到达生产前就发现缺少的假设。霍尔的核心动作——说明“运行前必须为真”和“运行后将为真”——可以直接转化为审查问题。

把霍尔思想变成审查问题

阅读变更时，尝试把每个关键函数当成一个小承诺：

• 假设（前置条件）： 关于输入、状态和环境必须为真的是什么？（例如“列表非空”、“用户已认证”、“持有锁”）。
• 保证（后置条件）： 之后什么为真，包括返回值和副作用？（例如“余额减少了 amount”、“记录只插入一次”）。
• 不变式： 在循环、重试或多步工作流期间什么必须保持为真？（例如“processed_count ≤ total”、“借方之和等于到当前为止的贷方之和”）。
• 失败行为： 出错时会怎样——系统是否处于安全状态？部分更新是否回滚？

一个简单的审查习惯：如果你不能用一句话说出前/后条件，这段代码很可能需要更清晰的结构。

对关键函数的“契约注释”

对有风险或核心的函数，在签名上方加一段小的契约注释。保持具体：输入、输出、副作用与错误。

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 会造成真实伤害、重大金钱损失或静默的数据损坏，你应该使用超过普通审查+测试的手段。

可考虑的工具（概览）

可以从“轻量级”到“重量级”选择，通常组合使用效果更好：

• 类型系统（更强的类型、非空、单位/量纲）：防止整类无效状态。
• 静态分析：发现可疑路径、API 误用、数据竞争、污点流。
• 契约（前置/后置、断言）：把你在推理中使用的霍尔式陈述变为可执行检查。
• 模型检查：探索状态机（对协议、并发和序列性问题很有用）。
• 形式验证：对最高保证部分进行机器检验的证明。

你应达到何种深度？

按下列权衡决定形式化深度：

• 风险： 影响 × 可能性。风险越高需要越强的保证。
• 成本： 规范、证明和维护所需时间。
• 变更频率： 频繁变动的代码更难保持形式化；先稳定接口再做形式化。
• 团队技能： 若证明会显著拖慢交付，可先从契约与静态分析开始。

在实践中，也可以把“形式化”看作渐进过程：先写明契约与不变式，再用自动化工具监督这些约束。

对于使用 Koder.ai 快速生成前端、后端与数据库模式的团队来说，快照/回滚与源码导出能让你在快速迭代同时，通过测试和静态分析在 CI 中执行契约，保持较高保证。

实用清单

在规划或代码审查中把这个作为“是否应当形式化更多？”的门槛：

1. 最坏的可信失败是什么，谁会受影响（用户、运维、监管）？
2. 测试能否现实地覆盖重要边界与状态？
3. 逻辑是否有状态性、并发性或大量不变式/边界？
4. 我们能否为公共入口写出清晰的前置/后置条件？
5. 是否有小核心可以隔离并更深地验证？
6. 哪种工具在这里回报最高：更强类型、静态分析、契约、模型检查或证明？
7. 下个季度会发生什么变动，如何防止保证漂移？

延伸阅读主题：契约式设计、基于属性的测试、状态机的模型检查、针对你所用语言的静态分析器，以及形式化证明工具和规范的入门材料。