每次测试套件通过，开发人员都会悄悄地、含蓄地（通常不经仔细检查）声称： 这段代码是正确的。但正确性体现在什么方面？正确程度如何？基于哪些假设？又是谁认为正确？更准确地说：一次绿色通过只意味着在当前测试集合、当前运行环境与当前预言机假设下，你没有触发被测试到的缺陷。
这些并非纯粹的学术问题。它们决定着测试套件是能发现缺陷，还是只会制造虚假自信。理解测试的认识论——即测试究竟能让我们了解什么、以及它依赖哪些隐含前提——是软件工程师最实用的技能之一。而这一切，必然要从该领域被引用最多却最少被深入探讨的一句话开始。
程序测试可以用来发现程序中存在的错误，但永远无法证明程序中不存在错误。
——艾兹格·W·迪杰斯特拉，《结构化程序设计笔记》，1970 年
迪杰斯特拉并非愤世嫉俗，他只是 严谨地 阐述观点。而这种严谨至关重要，因为五十五年过去了，业界对这句话的态度依然十分尴尬。我们引用它，却常常装作它不适用于我们的测试套件、覆盖率指标和持续集成流水线。指标越漂亮，越需要清楚它覆盖了什么、没有覆盖什么。把一次构建成功当作证据并不荒谬，但把它当作证明就会出错。真正深入理解它的本质——以及存在的替代方案——才是真正智力工作的起点。
测试的核心在于其不对称性
迪杰斯特拉的观察并非针对工程质量，而是针对逻辑——具体而言，是关于 验证 与 证伪 之间的区别。卡尔·波普尔几十年前就对科学做出了同样的观察：你永远无法通过观察实例来验证一个普遍真理，但你可以通过找到一个反例来证伪它。换句话说，测试的本质更像是在一个巨大空间里做结构化的反例搜索，而不是在给系统颁发合格证。测试套件是一种经验工具，它探测的是有限数量的输入和状态。相比之下，你的软件运行于几乎无限的可能输入、执行顺序、硬件状态和环境条件空间中。
考虑最简单的函数：一个将两个 32 位整数相加的函数。其输入空间为 2⁶⁴——大约有 18.4 万亿亿种组合。如果你从公元 1 年开始，每秒运行 1000 次测试，那么你今天仍然在运行。再把调度也算作输入的一部分：测试一个运行在三个线程上的函数，每个线程都可以在任何指令边界被抢占，会产生组合爆炸，这使得穷举测试不仅不切实际，而且在宇宙学上是不可能的。
这并非一个可以解决的工程问题，而是一个根本性的认知约束。一旦你理解了这一点，问题就从 如何证明我的代码是正确的？转变为更诚实的问题：我究竟获得了什么样的知识，我对它应该有多大的信心？而信心的来源，往往不是某个单一指标，而是证据强度、假设数量与故障代价之间的匹配。
==测试结果并非证明。它只是概率证据——一种结构化、带有偏见且在许多方面都不完整的证据，而这些缺陷却至关重要。==
实证检验的知识边界
如果测试无法证明不存在缺陷，人们很容易将其忽略。但这将是一个错误。实证测试能为我们提供真实且有价值的信息——在特定条件下证伪。当测试失败时，我们就能确凿地知道：至少在当前环境下，代码针对特定输入存在错误。这是一个可靠的认识论事实。真正棘手的问题不在于失败的测试告诉我们什么，而在于通过的测试究竟能让我们排除多少风险。
测试通过只能说明代码在特定的输入、特定的执行环境下，并且在特定的副作用被抑制或模拟的情况下运行正常。但它并不能说明其他输入、其他环境或其他并发交错情况。更现实的一句话是：你验证的从来不是代码本身，而是代码加上一组前提的组合。弥合 所有测试通过 和 代码正确 之间的信任鸿沟，并非依靠逻辑，而是依靠开发者对代码行为的非正式模型——这种模型几乎从未被明确阐述，而且几乎总是不完整的。
测试 Oracle 的问题
在测试覆盖率的讨论背后，隐藏着一个更深层次的问题：预言机问题。要编写测试，你需要知道正确答案是什么。对于简单的函数来说，这轻而易举。但对于复杂的系统——例如分布式共识算法、边缘条件下的金融计算、机器学习分类器——指定预言机的难度不亚于编写代码本身，有时甚至更高。许多现实世界中的 bug 恰恰存在于预言机能够表达的内容与代码实际执行的内容之间的鸿沟之中。更糟的是，一个检查了错误内容的测试不仅无法提供任何证据，反而会 误导 你：它会训练你的直觉，让你误以为代码是正确的。工程上常见的缓解手段包括差分测试、变形测试（metamorphic testing）、不变量/属性检查，以及基于真实流量的回放对账。
测试 Oracle 问题
测试预言机是判断测试是否通过的机制——最简单的情况是，它基于一个预期的输出值。预言机问题指的是为复杂系统指定正确预言机的难度，尤其是在正确行为事先无法精确知晓、取决于微妙的不变量或源于多个组件交互的情况下。这是软件测试理论中一个研究较为深入的问题，最早由 Weyuker (1982) 形式化。许多类型的软件——例如机器学习系统、压缩算法和数值模拟——本质上是传统意义上的 不可测试的，因为预言机问题实际上无法解决。
基于属性的测试：提出更好的问题
针对预言机问题以及基于示例的测试方法普遍存在的认知局限性，最有效的应对方法之一是基于属性的测试。它不再问 当输入 2 + 2 时，这个函数是否返回 4？，而是问 对于来自该域的 所有 输入，这个函数是否满足这些结构不变性？这种转变具有重要的哲学意义：它把预言机从一个具体输出，提升为可检验的不变量集合。
QuickCheck 最初由 Koen Claessen 和 John Hughes 于 1999 年为 Haskell 开发，开创了这种方法。在 QuickCheck 中，断言用于描述函数应该满足的逻辑属性；然后，该库会尝试生成能够证伪这些断言的测试用例。当它找到一个失败的用例时，它会将输入缩小到最小的反例——这是一个关键特性，因为随机生成的失败用例通常过于庞大和复杂，难以直接调试。
这个洞察非常精妙。你并非 reverse([1,2,3]) == [3,2,1] 在测试 是否，而是在测试 reverse(reverse(xs)) == xs 所有 x 是否都成立——这体现了反转的本质，而不仅仅是它对单个输入的 影响。此外，你还可以表达诸如 排序是幂等的、序列化和反序列化是逆操作 以及 过滤器的输出中会出现所有输入元素，不会出现其他元素 之类的属性——这些属性可以同时排除一大类错误。很多时候，属性其实就是你系统里那些隐含的结构性假设，把它们写出来，等于把调试成本提前支付了一次。
Hypothesis 库通过其复杂的有状态测试将这种测试方式引入了 Python。基于属性的测试主要由 Haskell 中的 QuickCheck 框架引入，它涵盖了基于示例的测试的所有范围：从单元测试到集成测试。如今，Java（jqwik）、Rust（quickcheck、proptest）、JavaScript（fast-check）、Scala（ScalaCheck）以及大多数其他主流语言都有相应的实现。
然而，基于属性的测试也无法逃脱迪杰斯特拉的警告。它从输入空间中采样——比手写测试更巧妙，但采样仍然是有限的。它将认知问题从 这个特定的输入是否通过？转移到 这 10000 个随机生成的输入中是否有任何输入失败？——这是一个更强大的问题，但仍然是一个经验性的问题。在 10000 次运行中没有找到反例 和 不存在反例 之间的鸿沟依然存在。要彻底跨越这个鸿沟，你需要一种不同的工具：把经验性证据换成演绎性证明。
形式化验证：证明的现实成本
形式化验证有望彻底弥合这一鸿沟。它不再是运行代码并观察输出，而是通过数学方法，并辅以机器可验证的步骤，证明代码满足 所有 可能输入和所有可能执行路径的规范。如果证明正确，迪杰斯特拉警告就不再适用。你不仅拥有证据，而且拥有了最强有力的知识。
这并非科幻小说，而是一个真实且不断发展的领域。seL4 微内核 拥有经过机器验证的功能正确性证明——其 C 语言实现已被证明符合 Isabelle/HOL 中形式化的 C 语言语义规范。CompCert C 编译器也已被证明是正确的：它对任何有效的 C 程序都不会产生错误输出。亚马逊使用 TLA+ 来验证 DynamoDB 和 S3 等服务的设计。高复杂性会增加设计、代码和操作中出现人为错误的概率；行业内的标准验证技术是必要的，但并不充分——深入的设计审查、代码审查、静态代码分析、压力测试和故障注入测试仍然可能在复杂的并发容错系统中遗漏一些不易察觉的错误。
然而，形式化验证的成本使得大多数生产软件开发难以采用，这些成本值得认真审视，而不是轻描淡写地忽略掉。
规范问题
要对代码进行形式化验证，首先需要一份形式化规范。编写一份正确的形式化规范至少与编写正确的代码一样难——有时甚至更难，因为规范必须使用为数学精度而非计算便捷性而设计的语言编写。像 Coq（现为 Rocq）、Lean 4 和 Isabelle/HOL 这样的工具需要大量的专业知识。像 TLA+ 这样的规范语言虽然有用，但难以指定程序的全局正确性属性——例如，很难编写一个契约来规定程序最终必须响应每个用户请求，或者数据库永远不会丢失数据。在实践里，很多团队拿到的是一种有界的确定性：边界来自抽象层级、状态空间裁剪，以及对环境的理想化假设。
此外，经过验证的系统，其可信度仅取决于其规范的可靠性。如果规范未能准确描述系统 应 如何运行，那么证明虽然正确，却毫无意义。这就是规范鸿沟：形式化验证无法捕获系统预期运行层面的缺陷，只能捕获实现过程中与既定规范不符的缺陷。实际上，许多现实世界的故障——包括安全漏洞——恰恰存在于预期与规范的边界处。
验证差距
形式化验证证明代码符合规范，但它无法证明规范是否完全符合用户的实际需求。这种验证正确性和预期正确性之间的区别并非技术上的限制，而是一条不可逾越的认知边界。即使是经过形式化验证的系统，也可能无法满足用户的需求。
模型与现实的差距
即使规范正确，经过验证的系统也会与未经验证的世界交互。硬件存在时序漏洞。操作系统调度器引入了形式化模型中不存在的不确定性。网络协议栈存在缺陷。JVM 添加的抽象层与 CPU 的实际执行模型有所不同。在协议栈的某一层进行验证可以提供该层内的强保证——但协议栈很深，层与层之间的每一次转换都会引入新的认知风险。因此，形式化验证更像是把不确定性推到接口边界，并把剩余风险显式化，而不是凭空消灭它。
确定性的层级
在对现状进行考察之后，有必要诚实地绘制出它的蓝图。不同的技术能够提供不同类型和程度的认知保障。没有任何技术能够不付出代价就保证绝对的确定性。对于任何工程团队来说，问题不在于 哪种技术能够证明正确性？，而在于 我们需要什么样的知识，用于系统的哪些部分，以及我们愿意为此付出多少代价？更工程化的表述是：把预算花在错误最贵的地方，把最强的手段用在最难原谅的失败上。
| 技术 | 事情过去之后你学到了什么 | 确定性水平 | 实际成本 | 最适用于 |
|---|---|---|---|---|
| 单元/集成测试 | 请针对这些特定输入进行更正 | 较弱 | 低的 | 回归检测、文档 |
| 基于属性的测试 | 在 N 个随机输入中未找到反例 | 缓和 | 中等的 | 不变性验证，边缘案例发现 |
| 模糊测试（覆盖率引导） | 已探索的代码路径中未发现崩溃/故障 | 缓和 | 中高 | 安全敏感的解析、I/O 处理 |
| 模型检查（TLA+） | 该属性适用于所有可达状态，直至边界。 | 高（有界） | 高的 | 分布式算法、协议设计 |
| 抽象诠释 | 不存在特定的运行时错误（例如，空引用解引用） | 高（明确） | 高的 | 安全关键型 C/C++ 代码、编译器 |
| 定理证明（Coq、Lean） | 该属性对所有输入、所有路径均成立。 | 非常高 | 非常高 | 密码学原语、操作系统内核、编译器 |
请注意，确定性阶梯每向上攀升一级，您获得的都是更多的知识，但代价是需要付出更多的努力、更多的规范工作，以及——至关重要的是——对工具本身正确性的更多假设。像 Lean 4 这样的证明助手只有一个小型可信内核，而该内核的正确性本身并非由机器验证，而是通过人工审查和社区积累的信任来验证的。最终，所有所谓的确定性都变成了乌龟，而非坚实的基石。
知足常乐的实用主义
这一切似乎会导致无所适从。如果连形式化证明都建立在未经验证的假设之上，如果测试从根本上来说是不完整的，如果规范也可能出错——工程师们究竟应该怎么做？答案并非虚无主义，而是基于风险的认知论。
- 先把系统按故障代价分层，明确哪些组件属于高风险边界（资金、权限、安全、数据一致性）。
- 再把高风险边界的关键假设写成可执行的不变量，让单元测试、基于属性的测试和静态分析围绕它们持续收敛。
- 最后用更激进的手段覆盖你最不愿意手工枚举的空间，比如模糊测试、回放对账与故障注入，把证据长期积累在流水线里。
系统的不同部分会带来不同的故障成本。用户界面组件中的排序算法和金融交易的序列化逻辑并非同一类型的问题。加密哈希函数和配置文件解析器也并非同一类型的问题。适当的认知严谨程度——即对确定性的适当投入——与出错的成本成正比。因此，认真对待测试认知论的工程实践并非 对所有事物都进行形式化验证，而是 针对每个组件应用恰当的知识获取方式，其程度应与知识出错的风险成正比。
纯技术方法往往忽略了其中的社会学维度。测试套件的目的并非仅仅在于孤立地捕获缺陷，而是为了构建并维护团队长期 共享的系统预期行为模型。测试是一种可交流的知识——它们以可执行且可审计的形式编码假设。一个旨在为未来阅读代码的开发人员记录预期行为的测试，与一个旨在探测极端情况故障的测试，在认识论层面上发挥着不同的作用。两者都有效。混淆二者，或者只针对其中一种进行优化，正是测试套件出错的原因。
从这个意义上讲，迪杰斯特拉的警告并非绝望的劝告，而是邀请我们明确你所声称的知识类型、其局限性，以及这些局限性对你构建、测试和推理你所负责的系统有何影响。这种认知上的精确性——清楚自己知道什么，也清楚自己不知道什么——最终才是工程学成为一门成熟学科而非一门充满希望的技艺的开端。
我们学到了什么
迪杰斯特拉在 1970 年提出的观点——测试只能证明缺陷的存在，而不能证明缺陷的不存在——并非悲观论调。它精准地阐述了证伪与验证之间的不对称性。测试是经验证据：样本有限、依赖于环境且受制于预言机。当测试失败时，它能提供强有力的知识；而当测试通过时，它只能提供较弱的概率性知识。
基于属性的测试（QuickCheck、Hypothesis、jqwik）将问题从 这个输入是否通过？转移到 这个不变式是否适用于大量的随机样本？——这是一个更强大的框架，能够更好地映射代码的结构假设，并且其样本缩减机制使得故障可以直接调试。但它仍然是经验性的：没有有限的样本能够弥合与普遍正确性之间的差距。
形式化验证（设计验证使用 TLA+，实现验证使用 Coq/Lean）弥合了这一差距——但代价是牺牲规范的正确性、工具的可信度，以及不可避免的模型与现实之间的差距，即已验证的模型与未经验证的硬件和软件栈交互时产生的差距。seL4 内核和 CompCert 编译器证明了这种差距是存在的；它们也表明，这种差距并不小。
成熟的实践是风险校准式的：单元测试用于回归和文档编写，基于属性的测试用于发现不变性，形式化方法用于正确性关键组件。了解自己知道什么——以及自己不知道什么——是使该学科其他部分连贯一致的认识论基础。