测试不是证明：通过未必可靠

测试验证代码输入形式化

发布于 2026-06-09

版权声明

我们非常重视原创文章，为尊重知识产权并避免潜在的版权问题，我们在此提供文章的摘要供您初步了解。如果您想要查阅更为详尽的内容，访问作者的公众号页面获取完整文章。

查看原文：测试不是证明：通过未必可靠

文章来源：

FunTester

扫码关注公众号

扫码阅读

手机扫码阅读

文章主旨：

本文深入剖析了迪杰斯特拉“测试只能证明缺陷存在，不能证明缺陷不存在”的著名论断，指出软件测试是一种基于经验证据的有限认知活动，而非对代码正确性的最终证明；工程师应采用基于风险的认知论，针对不同组件选择合适的测试策略（从单元测试到形式化验证），并明确每种策略所提供知识的类型与局限。

关键要点：

测试在认识论上存在不对称性：失败提供确定性知识（存在缺陷），而成功仅提供概率性知识（特定条件下未发现缺陷）。
测试 Oracle 问题，即确定“正确输出”的难度，是深层挑战：对于复杂系统，预言机问题甚至比编写代码更困难，错误的预言机会制造误导性的自信。
基于属性的测试（如 QuickCheck、Hypothesis）相比基于示例的测试提出了更好的问题：它验证代码的结构不变性，而非单个输入的值，是一种更强大的经验性方法。
形式化验证（如 TLA+、Coq/Lean）能提供演绎性证明，弥合了经验证据与普遍正确性之间的鸿沟，但为此付出了极高的现实成本（规范编写、专业知识、模型与现实差距）。
成熟的工程实践是风险校准式的，应将最严谨、成本最高的方法（如形式化验证）应用于故障代价最高的关键组件，而将轻量级方法用于其他部分。

内容结构：

1. 引言：迪杰斯特拉的不对称性

文章开篇引用了迪杰斯特拉的名言：“程序测试可以用来发现程序中存在的错误，但永远无法证明程序中不存在错误。” 作者指出，这句话并非愤世嫉俗，而是严谨的逻辑阐述。尽管被广泛引用，业界在实际工作中却常常回避其深层含义。一次测试通过仅证明在当前测试集、环境与预言机假设下，你没有触发某些缺陷，并不能等同于证明代码正确。

2. 测试的核心在于其不对称性

本节阐述了测试的哲学基础：验证与证伪的区别。引用卡尔·波普尔的科学哲学，说明测试的本质是“结构化的反例搜索”，而非给系统颁发合格证。以两个32位整数相加函数为例（输入空间2^64），强调了穷举测试在宇宙学上的不可能性。因此，测试结果并非证明，而是“概率证据”，其价值在于证据的强度和资源的匹配。测试通过只能说明代码在特定的输入、环境及副作用模拟下正常运行，而无法说明其他情况。

3. 测试 Oracle 的问题

本节深入探讨了测试预言机（判断测试是否通过的标准）的深层问题。指出对于复杂系统（如分布式算法、机器学习），指定一个正确的预言机（即知道正确答案）的难度与编写代码相当，甚至更高。文章引用 Weyuker (1982) 的研究，指出许多软件（如机器学习系统、压缩算法）本质上因预言机问题无法完全被测试。检查了错误内容的测试不仅无用，反而会错误地训练直觉，是一种误导。

4. 基于属性的测试：提出更好的问题

本节介绍了应对预言机问题的方法：基于属性的测试。这种方法从一个具体输入是否通过的问题，转变为“对于所有可能的输入，函数是否满足某些结构不变性的问题”。例如，测试反转函数时，不是测试特定输入，而是测试 reverse(reverse(xs)) == xs 对所有列表成立。这种方法将预言机从具体输出提升为可检验的不变量集合。文章介绍了QuickCheck、Hypothesis等工具。然而，它也无法逃脱迪杰斯特拉的警告，它依然是对输入空间的经验性采样。

5. 形式化验证：证明的现实成本

本节讨论了弥合经验证据与普遍正确性之间鸿沟的终极方案：形式化验证。通过数学证明来确保代码满足所有可能输入和路径的规范。文章列举了 seL4 微内核和 CompCert 编译器为代表的成功案例。然而，其高昂成本使其难以普及，主要挑战包括：

规范问题：编写形式化规范本身与编写正确代码一样困难，且验证的是代码与规范的符合度，而非规范与用户意图的符合度（规范鸿沟）。
模型与现实差距：经验证的系统与未经验证的硬件、操作系统、网络协议等交互时，会产生新的不确定性。验证更像是在接口边界将不确定性显式化，而非消灭它。

6. 确定性的层级

本节提供了一张知识获取技术的图谱，描绘了从单元测试到定理证明的“确定性层级”。它列出了每种技术能提供的知识类型、确定性水平、实践成本和应用场景。例如，单元测试提供“针对这些特定输入是正确”的较弱知识但成本低；而定理证明提供“对该属性所有输入成立”的非常高确定性但成本极高。文章指出，没有免费午餐，每向上攀一级，付出的努力和假设也更多。

7. 知足常乐的实用主义

本节总结出应对上述认知局限的方案并非虚无主义，而是“基于风险的认知论”。建议工程师：

将系统按故障代价分层，识别高风险边界。
将关键假设转化为可执行的不变量。
使用更激进的手段（如模糊测试、故障注入）覆盖难以手工枚举的空间。
认识到测试套件的目的是为了构建并维护团队长期共享的系统预期行为模型。迪杰斯特拉的警告本质上是在邀请工程师明确自己声称的知识类型、其局限性，以及这些局限性对推理系统的影响。

8. 结尾：我们学到了什么

文章重申核心结论：测试是经验证据，有其根本局限性；基于属性的测试是更强大的框架，但仍是经验性的；形式化验证能弥合差距，但需付出极高代价且依然存在模型与现实差距。成熟的实践是风险校准式的。了解自己知道什么与不知道什么，是使软件工程成为一门成熟学科的认识论基础。

文章总结：

本文系统性地解构了“测试通过”的认知价值，指出理解测试的哲学根基和认识论约束（即其能告诉我们什么、不能告诉我们什么）是比任何具体测试技术都更实用的工程技能，最终倡导一种基于风险、分层投入且始终明确知识边界的务实态度。认知上的精确性是工程成熟度的标志。