通过契约结合测试与证明以实现更优的软件验证

《Communications of the ACM》：Combining Tests and Proofs with Contracts for Better Software Verification

　　

# 测试还是证明？

## 摘要

测试还是证明？软件测试的这两种方法长期以来一直被视为对立的两极。一种是动态方法，另一种是静态方法：测试通过执行程序来验证程序，而证明则仅分析程序文本。一种新的视角正在兴起——在这种视角中，测试与证明是互补的，而非彼此竞争的软件质量验证技术。本文回顾了近年来所做的相关工作，这些工作通过利用"契约式设计"——在Eiffel语言中提供的机制——并结合现代程序证明工具基于"满足性调谐理论"（SMT）的一个特性——反例生成——来发展这种互补关系。反例是一组导致程序失败的输入组合。当我们试图证明一个程序的正确性时，我们希望不找到任何反例。然而，我们也可以对错误程序应用反例生成技术，将其作为自动测试生成的工具。我们还可以在正确程序中人为引入故障，然后将反例转化为具有完整覆盖率的自动回归测试套件。此外，我们还能利用这些机制帮助为错误程序生成修复方案，并保证修复的正确性。这三种应用都基于Eiffel和契约式设计的机制，在应对软件测试、软件维护和自动程序修复中的一些挑战方面具有巨大潜力。

软件开发不仅仅是智力活动，更是一项工程事业，成功时收益颇丰，出错时风险巨大。软件验证旨在避免此类不良后果。它有两个变体：动态方法和静态方法。动态验证，也称为测试，是在样本输入条件下执行系统并检查结果是否符合预期属性（"预言机"）。对于许多工业项目来说，测试是唯一的验证形式。相比之下，编程研究者口中的验证通常指静态方法，它不执行程序，而是分析程序文本，通常是其源代码形式。这种分析可以是针对特定属性的，也可以执行完整的形式化正确性证明——后者需要程序预期行为的正式规格说明，以便据此评估程序的实际行为。

## 关键见解

- **软件验证的重要性与挑战性使得我们有理由不排除任何可能有用的方法。** 静态方法（证明）和动态方法（测试）各有其适用之处，每种方法都能弥补另一种的局限性。

- **将二者结合可以将失败的证明尝试转化为失败的测试，从而立即提供问题出在哪里的线索。** 其他应用包括自动生成100%覆盖率的测试套件、自动生成保证正确的程序修复方案、改进包含循环的程序测试，以及验证MC/DC测试标准。

- **本文的工作及底层的AutoProof框架利用了"契约"——即嵌入在代码中的规格说明，如在Eiffel中找到的那样。**

## 测试与证明的长期对立

长期以来，测试与证明被放在一起比较。从业者常常拒绝证明，认为其过于困难、昂贵且不切实际。测试的批评者则认为测试无效，因为测试仅覆盖所有可能情况的极小部分；正如Dijkstra那句名言所言："程序测试可以用来证明缺陷的存在，但永远无法证明缺陷的不存在！"1 这场争论有时非常激烈，证明被强烈否定1?（针对Naur的证明尝试），1?,33 而证明倡导者对测试的局限性也做出了同样严厉的批评。

近年来，更加调和的态度开始出现，2007年以来举办的**测试与证明**（TAP）会议就是这一趋势的例证之一。任何形式的验证都充满挑战，不应让教条主义排除任何潜在有用的技术。即便是最坚定的证明倡导者也必须承认，可能无法以形式化的方式指定所有属性——尤其是性能、容错性等"非功能性"属性——而且任何证明的价值都取决于一个假设：编译器和硬件均能保留程序语义，这为测试留出了空间。此外，我们也能注意到双方在失败方面的作用：

- **失败的测试实际上是一种证明：** 它证明了程序是不正确的——正如波普尔的科学观中，否定性实验证明理论有误一样。（从这个角度看，Dijkstra那句通常被听作对测试的指责的俏皮话，实际上可以看作是对测试的一种**推荐**：软件验证的目标之一正是帮助发现缺陷。）

- **失败的证明尝试往往让我们无从下手。** 要理解问题所在，看到触发潜在故障的测试很有帮助。这一思想将在后文进一步展开。

测试与证明的互补性超越了以上观察。本文讨论的工作催化剂是现代程序证明工具（如基于满足性调谐理论/SMT的工具2）中的一个特性：尝试生成违反规格说明的反例。如果证明无法产生任何反例，则证明成功；但对于错误程序，反例可以转化为测试用例。我们还可以利用所得信息来提出程序修复建议。对于正确程序，我们可以通过注入故障并产生反例来获取回归测试套件。

我们已将上述思想应用于开发利用这种互补性的验证和程序修复技术，同时利用契约式设计方法进行软件构建。2? 在此之前，该流程的各个步骤曾在不同的文章中分别描述，1??23 本文则面向更广泛的读者提供了一个全面的、最新的内容展示。首先，我们阐述总体思想：利用与证明失败相关的信息。然后回顾契约式设计——该方法的关键要素。在后续章节中，我们介绍基本思想的逐步改进：

- **Proof2Test**1? 将失败的证明（通常看起来毫无用处）转化为有用的测试用例，为证明失败提供具体的证据，使程序员能够理解并解决根本问题。
- **Proof2Fix**1? 将测试与证明的结合扩展到自动程序修复，通过证明器提供修复方案的正确性保证。
- **"种子矛盾法"**21 将该能力扩展到系统性测试生成。通过故意创建失败的证明并使其经过Proof2Test处理，它可以生成满足代码覆盖率标准的测试集合。它还结合循环展开技术来创建探索循环行为的测试，并帮助评估修正条件/判定覆盖率（MC/DC）——这一测试标准有时受到质疑，但在工业界被广泛使用。

在最后几节中，我们回顾相关领域的早期工作并得出结论。

## 核心思想：证明及其失败

证明程序正确性的思想可以追溯到上世纪40年代末Turing和Von Neumann富有远见的文章，以及Floyd、Hoare、Dijkstra、McCarthy、Naur等人1970-1980年代开创性的工作。近年来发生的变化在于实用工具——"证明器"——的出现，这些工具能够证明程序（包括大型程序）的正确性。证明一个显著规模的程序涉及过多的步骤，使得人工检查要么不切实际，要么（假设它可行的话）不可信。因此，自动化的角色至关重要。尽管仍只有少数项目使用证明器，但证明器已在工业界取得了一些成功。1?

证明器基于程序与规格说明（通常以"契约"的形式表达，详见下文）的组合来工作。本文工作的起点是利用许多现代证明器内部使用的技术：寻找一个或多个"反例"——即违背预期属性的示例输入。如果这一尝试失败，则证明成功。?

**重点在于证明失败时的中间步骤**——即反例搜索成功的时候——更具体地说，重点在于反例本身。

逐步发展的研究表明，这一思想有多个富有成效的应用。第一个是将反例转化为测试。证明失败令人不安："后置条件违反"并不能帮助程序员理解究竟犯了什么错误。然而在内部，证明器已经拥有一个反例——"对于输入5，输出为-3，但要求必须为正数"——这对程序员来说就信息丰富得多，如果再附带一个自动生成的、可运行的测试来重现该失败，那就更加有效了。换言之，一种工具可以将失败的证明转化为失败的测试，这有两个主要优势：为程序员提供具体的、可运行的证据；以及生成一个回归测试，在后期项目历史中bug修复后可以再次运行。这就是Proof2Test的功能。

下一个应用是利用反例生成程序修复方案。自动程序修复（APR）需要描述失败执行的"不变量"。本方法可以自动生成保证正确性的不变量，而不是从手动生成的测试中获取；可以通过将修复方案经过证明器验证来保证修复的正确性，而不是通过测试来验证。这就是Proof2Fix的功能。

对于关键系统，测试套件必须达到高水平的覆盖率，超越基本的"分支覆盖率"，达到MC/DC等行业标准度量指标，并展开循环以使测试能执行多个连续迭代，而不仅仅是零次或一次。

## 契约的作用

虽然本文报告的成果具有普遍适用性，但这些成果依赖于契约机制，该机制由多种语言提供，包括本文所使用的Eiffel语言。验证程序的正确性需要拥有其预期行为的规格说明，因此契约是必需的。契约是嵌入在代码本身（而非单独文档中）的规格说明元素，因此既可用于测试（在测试运行中评估它们），也可用于证明。契约有以下几种形式：

- **简单断言**（图5中的check）：必须在代码特定位置成立的属性
- **前置条件**（图2第3-4行的require）：调用者在任何调用中必须满足的属性
- **后置条件**（图2第18-20行的ensure）：例程（供应者）保证的属性
- **循环不变量**（图2第9-11行的invariant）：在循环初始化和每次迭代之后保证成立的属性
- **循环变元**（图2第16行的variant）：保持非负且在每次循环迭代中递减的整数度量，确保循环终止

作为一个例子，图2展示了一个Eiffel类MAX。max函数的意图是将数组a（大小为a.count的整数数组）中的最大元素返回到Result中。第19和20行的后置条件子句（is_max和result_in_array）指定了函数的意图：数组中的每个元素都应小于或等于Result；并且至少有一个元素应等于Result。

契约是测试和证明的强力推动因素，因为它们是嵌入在代码本身的规格说明元素。对于测试，它使得能够精确识别缺陷来源：前置条件违反表明缺陷在客户端；如果测试通过了前置条件，则后续任何失败都是供应者方法代码中的缺陷。AutoTest2?等工具已利用这些思想提供自动化随机测试。对于证明，大多数工具依赖Dijkstra的最弱前置条件（wp）计算12，当代码已包含后置条件和显式的循环变元与不变量时，这些工具能够充分发挥其潜力。

许多编程语言（如Java、C#、C++和Python）支持简单断言，但没有为上述其他用途提供专门的结构。一些语言的扩展引入了这些结构：Java的JML?和C#的Spec#。不过，只有少数语言享有内置的契约机制，包括Eiffel、SPARK、Dafny以及即将到来的"C++26" ISO/IEC C++标准。本文工作基于Eiffel，原因是它对契约提供了作为核心原生机制（而非附加组件）的广泛支持、通过EiffelStudio编译器和IDE等工具的实用可用性，以及它在利用契约进行自动测试生成（AutoTest）、自动程序修复（AutoFix）和证明（AutoProof，即本文所述工具集中使用的）方面的研究经验。2?,3?,3? 本文描述的所有工具和技术都已集成到EiffelStudio的研究版本中（图1）。

**图1.** 程序验证、测试和修复的工具组合。

契约对于应用许多现代证明器所使用的理论也是必需的：即Dijkstra最弱前置条件（wp）计算12的变体——"Hoare逻辑"。

为建立例程 r（属于类 b）、前置条件 P 和后置条件 Q 的基本条件，需满足：P?(bwpQ)，其中 bwpQ 是最弱保证条件，即当 b 在满足 P 的状态下开始时，将终止于满足 Q 的状态。证明器会为每个 r 计算该条件，然后证明每个调用都满足它。如下一节所述，基于 SMT 求解的证明器通过尝试寻找一个变量赋值（反例）来反驳该条件，以此实现该目标。如果找不到反例，证明成功。本研究利用了相反的情况。

**从失败的证明中生成测试**

前一节的观察阐明了失败在证明和测试过程中的含义，以及两种情况如何相互关联。失败的证明会让程序员困惑于究竟哪里出了错。失败的测试则提供了具体证据。

对于试图证明程序正确性的任何人来说，失败是熟悉的伙伴。教科书通常展示成功的证明，但在实践中，通往成功的道路可能令人沮丧。例如，假设你正在使用证明器并仔细准备了下一步证明：程序、其规范（契约）以及被称为验证条件的额外注释。你点击"验证"，证明器告诉你无法成功完成证明。图2展示了这种响应，针对 AutoProof 证明器，在引入下文讨论的工具之前。

图2 一个失败的证明。

接下来该怎么做？消息表明某个后置条件（第28行），描述例程 is_max 的预期效果，可能未被违反。这甚至不意味着例程不正确，只意味着证明器无法证明它是正确的。是实现有误（最常见情况）？是规范有误？开发者是否忘记包含某些验证条件？还是该任务超出了证明器的能力？

获得成功证明的过程有时被称为静态调试，与传统的动态调试形成对比，因为后者涉及在测试中运行程序。静态技术在成功时提供一组测试无法比拟的正确性保证。但失败的测试具有实用优势，即为程序员直接提供有用的故障证据，帮助识别失败根源——缺陷（故障）并加以修正。在心理学文献中，这类响应被称为建设性反馈，尽管基本思想从日常生活经验中就很清楚（"你的答案错了"不如"第3页你把磅误认为千克了"有效）。在处理编程错误时，程序员需要心理上重现故障程序的执行。失败的测试提供了这种可直接利用的指示；而图2中的失败证明消息则没有。

现代证明工具有可能告诉我们更多。为了建立如前节所述的 Hoare 风格属性，AutoProof 依赖于 Boogie，而 Boogie 本身使用" SMT 求解器"如 Z3，其证明属性的方法是寻找击败它的反例。当找不到反例时证明成功。如果找到一个或多个则失败。为了获取更多具体信息，程序员原则上可以深入求解器内部寻找反例。然而，通常这些信息分散在数百行内部文件中，其格式 SMT-LIB 是为验证专家设计的。BVD（Boogie 验证调试器）和 Boogaloo 等工具可以提供帮助，但仍然是静态的。

Proof2Test 扩展了 AutoProof 并提供了缺失的环节。它分析内部信息以展示一个可直接理解的输入示例，说明导致失败的原因，在此例中包括数组的大小和部分元素（图3a），然后生成一个测试用例（图3b）。

图3 失败的证明提供具体的（最小化）错误案例。

在图3a中，值很小：一个包含值0和1的二元素数组。如果被要求产生一个反例，SMT 求解器通常会产生大得多的值。此处，它初始产生的数组大小 a.count 为 11,800，值为 a[11799]=0 和 a[11800]=5。就反证目的（证明后置条件不成立）而言，它们与其他任何值一样有效。由于 Proof2Test 的目的是提供具体证据以帮助程序员具体地理解发生了什么，我们更偏好具有人类尺度意义的值。Proof2Test 利用底层证明器生成多个反例（提供不同种子时）的能力，应用最小化算法生成连续的候选值直到找到最小值，如图3中的值。与传统程序员设计的测试用例一样，这些值使程序员能通过尝试它们来关联失败，如图2所示，并发现在线10-12的循环初始化处 Result=0 且 i=2，使得在第18行退出条件求值为 True，终止循环并暴露缺陷：过早终止阻止程序获取第2个位置的最大值。为消除错误，只需加强退出条件允许再进行一次循环迭代：将 i≥a.count 改为 i>a.count。

除了产生帮助程序员理解和修正失败背后故障的信息外，Proof2Test 还能将反例转化为测试。图3b实际上是 Proof2Test 生成的可执行测试用例，以编程语言表达。程序员可以运行该测试并逐步观察它如何违反规范：

- 创建 MAX 类的实例 current_object（第7行）。
- 创建整型数组 a 并填充值：位置1为0，索引2为1（第8-9行）。
- 以 a 为参数调用 current_object 上的错误函数 max（第10行）。

在 AutoTest 中运行此代码会产生由后置条件 is_max 被违反导致的运行时失败，为图2版本中存在什么问题提供了切实证据（这是失败尝试无法获得的），使开发过程得以继续。

在20个 Eiffel 程序上对 Proof2Test 的初步评估展示了该方法潜力。使用 Intel 12核处理器和32GB RAM，上述过程平均耗时不到0.5秒。在大多数情况下，生成的失败测试是有用的：执行它会产生特定跟踪，说明程序如何导致与使证明失败的同一契约违反；程序员可以使用调试器的逐步模式来理解问题。

在少数情况下，生成的测试未导致失败。原因通常是实现在某种直觉意义上是"正确"的——它做了程序员某种程度上的意图——但规范是不完整的。这些通过的测试运行也是有用的，尽管方式不同于失败的运行：它们提醒开发者规范存在问题。（如果我们无法精确陈述程序应该做什么，我们几乎不能说法程序是正确的。）在两种情况下，生成的测试作为回归测试都很重要。一旦缺陷被修正，每个先前失败的测试都应成为项目回归测试套件的一部分。

实验结果也表明最小化是成本效益高的：在大多数情况下，它将整型变量的值减少了80%以上，平均额外成本不到四次重新验证运行。大多数最小化后的值很小且易于关联：在125个值中，108个在 [-2, 2] 范围内，其中58个为零；其余通常接近程序中出现的某些常数。

**结合测试和证明实现更好的程序修复**

识别缺陷是好的；修正它们更好。自动程序修复已展示了产生有用修复的潜力。大多数现有 APR 方法的致命弱点是它们依赖测试用例进行缺陷识别和修复验证。编写测试用例是乏味的；运行它们可能耗时；而（最显著的局限）通过测试验证不保证其正确性（再次想到 Dijkstra）。基于 Proof2Test 的 Proof2Fix 实现了一种静态 APR 方法。

工具链（图4）源自 APR 中的标准工作流，通过将测试替换为证明。流程从使用证明器（此处为 AutoProof）验证程序开始。如果证明器检测到故障，Proof2Test 生成反例，每个反例代表一个失败的执行轨迹，其中程序进入违反所需属性的状态。传统 APR 技术分析失败的测试（通常手工生成）以识别可能定位失败原因的共同元素；Proof2Fix 使用相同思路，但以自动静态生成的反例替换测试。

图4 Proof2Fix 工作流。

从反例中生成抽象通用属性使用 Daikon，一个推断工具，产生一组反例不变量：在反例中成立的输入变量谓词，匹配一组模式（变量之间或与常数的等式、线性关系 e1=a·e2+b 或 e1=a·old e2+b 等）。这些不变量使得为契约或实现产生候选修复成为可能。（实证研究表明缺陷来自这两种错误。）AutoProof 随后过滤掉无效修复，仅保留通过证明的修复（它们消除了原始证明失败且未引入新失败）。有效选择可以呈现给程序员。在缺陷发现阶段和修复阶段都不需要发明测试数据或产生测试框架。

对修复80个证明失败的评估表明该方法可以产生有意义的、经过形式化验证的修复。它为所有失败的82.5%生成至少一个有效修复，为37.5%的失败生成至少一个程序员批准的修复。修复会话耗时约一分钟。Proof2Fix 对两类故障导致的失败最有效：赋值中错误的源表达式和条件指令中错误的条件。在这两种情况下，推断的反例不变量正确描述了需要排除的故障案例。然而，该方法不太擅长修复由过弱契约导致的失败，因为生成的反例表现出太多多样性。

**以证明为基础实现高效的测试套件生成**

当验证结果出现多个失败时，Proof2Test 会产生多个不同的测试。播种矛盾策略利用了这一可能性。

每个严肃的软件项目都需要回归测试套件，对管理项目演进至关重要，确保新开发不使先前正常工作的功能失效。（软件工程历史中不乏回归缺陷的例子，如2012年 Knight Trading Group 的缺陷，在45分钟内造成该公司4.4亿美元损失并几乎使其破产，以及2024年7月 CrowdStrike Falcon 传感器更新。）除了实践中建议将历史上每个失败的案例包含一个测试外，要产生一个覆盖所有可能执行路径的高覆盖率回归测试套件是非常困难的。

乍看之下，前面描述的 Proof2Test 技术似乎不适用，因为它们处理有缺陷的程序，而我们需要为正常运行的程序创建回归测试套件。播种矛盾背后的想法，顾名思义，是通过在每个分支中插入缺陷，以多种方式使正确程序变为不正确。虽然起初这有些反直觉（软件工程通常的目标是从不正确到正确！），但这个想法使我们能受益于前面为有缺陷程序生成反例的技术。在适当条件下，一个不正确程序的反例可以是相应正确程序的一个示例（正确行为的一个案例）。

Proof2Test 配合 SC 在每个控制分支中插入错误指令（"陷阱属性"），如图5所示。

该指令是 check p end 指令的一个特例，后者要求布尔属性 p 必须在相应的程序点上成立，否则验证将失败。如果尝试执行该指令，而 p 在运行时不成立，则会导致异常。当 p 取值为 False 时，该分支将无法通过验证，并且上一节所述的 Proof2Test 机制将生成相应的反例。实际上，该技术不仅适用于错误的程序，也适用于正确的程序。尽管它使用了通常用于配备契约元素（前置条件、后置条件、类和循环不变量、循环变体）的程序的验证器，但它也适用于无契约的程序，如下例所示。

图 5：带有植入矛盾的分支程序。

```
simple (a: INTEGER)
do
if a > 0 then
check False end
x := 1 -- 指令 1
else
check False end
x := 2 -- 指令 2
end
end
```

通过构造，生成的测试套件对可行分支实现了 100% 的分支覆盖率（排除不可达分支，因为任何测试都不可能执行它们）。Proof2Test 从两个互补的方面超越了分支覆盖率：

• **MC/DC（修正条件/判定覆盖率）**：可选地，Proof2Test 强制实施"修正条件/判定覆盖率"标准，该标准在多个重要的工业软件安全标准中受到推荐，尤其在航空航天行业中得到广泛应用。

• **循环展开**：标准 "while" 或 "until" 循环的循环体，按其定义，可以执行可变次数的操作；但分支覆盖率只需要一条执行零次的路径和一条执行至少一次的路径。换言之，它像对待条件语句一样对待循环，从而遗漏了仅在其余执行次数下才会出现的缺陷。Proof2Test 包含一种循环展开机制，该机制考虑循环体执行（"展开"）任意次数，直至达到用户可设置的最大次数，该最大次数需考虑性能约束来确定。

我们对实施 MC/DC 和循环展开的结果进行了测量，23 结果表明两种增强措施都能发现单纯分支覆盖率会遗漏的缺陷。虽然示例程序虽然意义重大且在某些情况下相当复杂（例如来自验证竞赛），但它们仍然规模较小，因此我们避免得出概括性结论，但结果是令人鼓舞的：

• MC/DC 使发现的缺陷数量比分支覆盖率增加 12.2%，对于具有复杂多重条件判定的程序，这一比例增长至 14.6%。21 这一结果意义重大，因为测试界对 MC/DC 存在一定程度的怀疑态度（部分原因是原始论文缺乏实证结果）——有些作者甚至否定了这种方法。4

• 循环展开随着展开深度的增加发现更多故障。测量表明，与 5 级展开相比，相比单纯分支覆盖率有 14.5% 的提升，发现了所有故障的 86.1%。23 在较小的展开级别（≤ 5），检测到的故障数急剧上升；从 1 级到 2 级带来了 9% 的提升。超过 5 级后，效果减弱（从 5 级到 8 级降低 3%）。

许多先进的测试生成技术，如有向自动化随机测试和合流测试，36 仍然需要一些代码执行。本文描述的技术完全基于静态分析：它们使用验证器执行验证，但不执行程序，因此不需要测试数据（尽管它们生成此类数据）或测试框架。如前所述，它们适用于正确和错误的程序。如果程序调用带有前置条件的例程，生成的测试将满足前置条件，这得益于 SC 的约束求解技术。

上述基于实证研究的21f–23结果，在合理的性能下实现。SC 策略生成测试套件的速度比某些动态技术快得多，例如 IntelliTest37（以前称为 Pex，一种用于 .NET 的符号执行测试生成工具）和 AutoTest（一种使用自适应随机测试的 Eiffel 测试生成工具，具体为 ARTOO）。8 对于典型的小型程序，SC 大约需要 0.5 秒来生成一个 100% 分支覆盖率的测试套件；这比 IntelliTest 快约 50 倍，比 AutoTest 快约 500 倍。添加 MC/DC 大约将使生成时间翻倍，测试套件的大小（这在实践中是一个重要关注点，因为良好的软件流程会频繁运行测试套件）增加不到 10 倍。根据循环控制流结构的复杂度，为测试生成添加展开功能会导致生成时间不同程度的增加。对于简单循环（既无嵌套条件也无嵌套循环），随着展开深度的增加，生成时间将大致线性增长。而对于包含更复杂条件嵌入的嵌套循环或循环，随着测试生成过程中引入更多失败的指令，生成时间的增加变得更加显著。Huang 等人的23评估表明，对于包含嵌套循环的程序，时间呈指数级增长，当展开深度达到 8 时变得不可接受（超过一小时）。

**相关工作**

许多先前或平行的工作将验证失败生成的反例转化为诊断信息。Boogie 验证调试器（BVD）26 允许程序员静态地"调试"Boogie 证明失败报告。26 其他工具7,32 追求类似的目标。这些方法提供静态追踪用于分析；本文报告的方法更进一步，通过生成动态追踪和程序员可以运行以直观了解实际情况的测试来实现。

许多测试项目使用 SMT 求解技术来生成测试。其中一些，如 Klee、6 PathCrawler、40 Pex/IntelliTest37 和 CUTE，36 基于符号执行。它们探索程序中的路径，并使用约束求解器推理其可行性。这些策略包含一个动态组件，因此无法提供穷尽分支覆盖率的保证。本文报告的测试策略是静态的。

据我们所知，最早应用这一思想的工作1使用有界模型检测（BMC）25 为低级 C 程序生成测试，产生具有穷尽分支覆盖率的测试套件。一个更近期的变体是针对 Java 字节的 JBMC，5 每次验证运行仅激活一个断言，产生一个反例（C 版本1使用编译时宏，每个块一个，以避免实际生成多个程序）。相比之下，SC 框架只产生一个程序，使用一个运行时变量表示块编号。同样，Beyer 等人3扩展了软件模型检测器 Blast 以生成相对于给定谓词完全覆盖的测试套件。基于 BMC 的方法依赖于执行追踪边界的正确性：如果边界未正确设置，某些分支可能无法被覆盖，需要更多的验证运行以获得更好的边界。SC 方法不需要此类机制。一种应用故障注入思想生成测试的方法34（建立在利用反例进行程序修复的工作35之上）在 Hoare 风格的验证中利用 OpenJML9 验证工具产生的反例来生成 JUnit 格式的单元测试。这些方法都与本文讨论的工作有相似之处，后者似乎提供了最广泛和统一的证明-测试组合技术集合，从利用证明失败到反例最小化、覆盖多种代码覆盖率的测试生成，以及自动程序修复。

自动化测试生成是一个活跃的研究领域（例如 Gorla 等人16），近年来越来越多地使用大语言模型（LLM），通常导致平均覆盖率水平在 75% 到 90% 之间。Proof2Test 的效率要高得多。LLM 也可以用于自动生成规范，27 尽管仍存在疑问：虽然此类规范可能使代码可证明，但它们也可能是错误的规范，从而阻止生成某些相关的测试。

本文的与众不同之处在于使用了 Eiffel 语言。虽然这可以被视为一种局限，但这一选择也带来了相当大的优势，因为它不需要为另一种语言添加内容（如 Java 的 JML），而是使用一种现有的（ISO 标准化）语言，利用内置的契约机制，因此可以直接使用带有契约的原始源代码来同时用于测试（通过 EiffelStudio 在测试期间评估断言的机制）和证明。其他语言的用户可能将这些结果视为"实验室工作"，即在理想条件下为其他人扩展结果到不同环境铺平道路。

**结论**

本文呈现的工作存在若干局限性。目前的示例仍然规模较小，尽管有些涉及复杂的算法。部分应用（但不是全部）假设程序已配备契约，这并非所有程序员都愿意采取的步骤。而且目前的程序修复应用主要覆盖基本类型的变量，需要扩展到复杂数据结构。

然而，这些结果令人振奋，尤其是在性能方面：验证比运行许多测试更快，这一优势随着程序规模和复杂度的增加而迅速扩大。更广泛地说，任何声称程序员不想编写契约的论断都应该与程序员在当今主导的基于测试的方法中必须执行的任务进行权衡。通常使用的术语"自动化测试"在其当前含义下是一个误称，掩盖了不愉快的现实：测试用例生成（仍然在很大程度上是一项手动任务）给程序员带来的巨大负担。（AI 工具会有所帮助，但它们也会帮助编写契约。）采用静态方法，这项任务可以自动化。

更广泛地说，程序证明和动态测试追求相同的最终目标——软件正确性。本文已经表明，可以将它们视为互补而非排他的关系。我们看到了这一思想的三个主要应用，利用现代证明工具底层 SMT 求解器的特性：将失败的证明（通常对程序员来说难以捉摸）转化为可直接使用的测试（特别是在最小化之后），以直观地证明失败，将实例缩小到人类可处理的规模；完全自动生成 100% 覆盖率的测试套件；以及提供保证的缺陷修复。当今的工具仍不完美，但它们指明了软件验证和修复有效性实现重大飞跃的道路，结合了软件工程社区从测试和证明中学到的最佳实践。

**作者简介**

李黄是德国不来梅州康斯坦茨大学计算机科学与工程系的讲师。

Bertrand Meyer（[e-mail]）是瑞士联邦理工学院苏黎世联邦理工学院的教授（荣誉退休），也是 Eiffel Software 和 Recognyze AI（均位于美国加利福尼亚州圣巴巴拉）的首席技术官。

Manuel Oriol 是瑞士伊夫雷讷莱班沃大学工程与管理学院（HES-SO）的副教授，也是德国不来梅州康斯坦茨大学的兼任教授。他仍然参与 Oriol Consulting 的咨询活动。