锈蚀测试或验证：为什么不能两者兼而有之？

Dijkstra著名地贬低测试，他说“程序测试可以用来显示错误的存在，但永远不能用来显示它们的存在！”好像您应该选择一个而不是另一个。我不认为它们是对立的，而是作为互补的技术，两者都应该用来提高代码的质量。

我是正式验证的忠实粉丝。正式验证工具可能是您使用过的最好的错误查找工具。它们可以从您的代码中完全消除整类错误。但是，正式验证不会在您的规范中、在您对依赖项的假设中、或者在您的构建/CI工具等中发现错误。(有关测试在正式验证的系统中发现错误的更多示例，请参见Fonseca。)。

而且，我们都勉强同意Dijkstra是对的：即使是一个彻底的、执行完美的测试计划也可能遗漏错误。

所以，在过去的几个月里，我一直在尝试两者兼而有之。我们(我和我在Google的团队)一直在重新实现Jason Lingle的Protest属性测试库，以便与Rust正式验证工具一起使用。最初的Protest允许您编写测试工具来测试您的代码(可能)是否满足属性。今天，我们发布了Protest接口的重新实现，使您能够使用完全相同的测试工具来正式验证属性是否成立。到目前为止，我们只尝试了K.Protest。1个。

[在我进一步讨论之前，我应该提到，我们本周发布的是一个非常早期的研究原型。它还没有准备好正式使用，而且它绝对不是官方的、受谷歌支持的产品。我们现在正在放松它，目前处于不成熟的状态，因为我们想就程序员希望如何正式验证Rust代码进行对话，我们认为有一些东西可以推动它是有帮助的。我们欢迎增加对其他验证器的支持的拉请求，或者将设计推向更好方向的拉请求。]。

为了了解属性测试在protest中是什么样子，我们将查看protest书中的一个示例。

Fn add(a：i32，b：i32)->；I32{a+b}protest！{#[test]fn test_add(a in 0..1000i32，b in 0..1000i32){let sum=add(a，b)；assert！(sum&>；=a)；assert！(sum&>；=b)；}}。

此示例定义了一个名为test_add的属性，用于测试名为add的函数。特别地，它检查对于非负值a和b，sum(a，b)的结果是否至少与a和b一样大。

符号0..1000i32表示范围[0..1000)中的所有值的集合，而0..1000i32中的符号a表示应该从该集合中选择一个值a。

最大的推进器！宏将此属性转换为测试函数，该函数重复生成a和b的随机值并执行属性体。

(在添加了一些附加的粘合代码之后)我们可以使用以下命令运行此示例。

正在运行%1 testtest test_add...。OK测试结果：OK。1通过；0失败；0忽略；0测量；0过滤掉。

而且，如果我们故意编写一个不成立的属性，那么Cargo测试会产生类似以下内容的输出。

正在运行%1 testtest test_add...。FAILED失败：-test_add标准输出-线程'；test_add'；断言死机失败：sum>；=a+100'；，src/main.rs：11：9thread'；test_add'；死机测试失败：断言失败：sum&>；=a+100；最小失败输入：a=0，b=0成功：0本地。，src/main.rs：7：1故障：test_addtest结果：失败。通过0次；失败1次；忽略0次；测量0次；过滤出0次。

Proptest通过生成随机值和测试来检查上述属性，但我们也可以将该属性解释为，对于集合中的所有值a和b，属性主体不会出现恐慌，也就是说，我们可以将其解释为一个普遍量化的规范。

为了验证上述属性，我们使用一个脚本来编译Rustcode，调用Klee符号执行引擎，并过滤Klee的输出，以确定是否存在可能导致属性主体死机的a和b选项。

而且，如果我们更改示例属性，使该属性不成立，Cargo-Verify将生成此输出。

线程'；test_add'；在'；断言处死机失败：sum>；=a+100'；，src/main.rs：11：9正在运行1测试值a=0值b=0test test_add...。FAILED失败：失败：test_addtest结果：失败。通过0次；失败1次；忽略0次；测量0次；过滤出0次。

在这个例子中，随机测试和正式验证产生了相似的结果。我可以选择一个正式验证发现随机测试遗漏的bug的例子。或者我也可以选择一个随机测试很容易发现bug但正式验证永远旋转的例子。但是，在这篇文章中，我想重点关注这两种方法之间的相似之处，而不是区别。

在本文中，我们使用了一个易于解释但并未真正展示命题的威力的示例。

其中我们检查涉及标准Rust集合类型的属性，比如向量和B树。(这应该与protest文档一起阅读。)。

在Dynamic.rs中，我们通过对特征的可能实例的子集进行量化来检查涉及特征对象的属性。

你可以把它理解为我们计划做的事情的草图，或者是对我们还没有做的事情的承认。就像弗雷德和金杰说的那样，“西红柿。番茄。“]。

这部分是因为正式验证还不够流行，不足以让足够多的Debian/Homebrew包存在，部分原因是我们需要一些非常具体的版本。(也可以删除一些依赖项！)

我们正在将Crux-Mir支持添加到库和工具中。Crux-Mir是Galois软件分析工作台(SAW)的一个新部分，用于验证由Rust编译器生成的MIR代码。

这比使用KLEE花费的时间要长一些，因为我们的货物的功能-验证与Crux-Mir的功能相似，但它们的方法略有不同-我们仍在研究处理由此产生的冲突的最佳方法。

一次把注意力集中在一个板条箱上是很有用的，我们有一些关于如何通过模糊和验证来做到这一点的想法，但我们还没有机会尝试它们。

Proverify库中的集合支持有一些技巧来避免一些明显的伸缩问题，但是我们不知道这些技巧是否适用于所有的验证工具，而且它们可能只触及了需要做的事情的皮毛。

测试和正式验证通常被描述为致命的敌人，我认为这错过了一个利用您对测试的现有熟悉度和舒适性来让您从正式验证工具中获得价值的巨大机会。

我鼓励您下载我们的库和工具，试用并给我们反馈。如果您正在开发锈蚀验证工具，我们会很高兴您尝试将我们的库与您的工具一起使用。如果您给我们发送一个拉取请求，我们会更喜欢。

在这个阶段承诺使用库可能不是一个好主意：目前它不是很健壮，我希望随着我们从将库移植到其他类型的正式验证工具中获得经验，它会有很大的变化。

Goodman：NDSS：2018将一些非常类似的想法应用于2018年的C++测试，使用GoogleTest DSL作为起点，并为Angr、Manticore和Dr.Fuzz提供支持。

他们遇到并解决了日志记录(导致路径爆炸)、符号循环界限和符号数组索引(导致路径爆炸)以及如何将群测试与验证相结合的问题。

好的，我必须承认目前针对Rust的验证工具并不多。到目前为止，我们的大部分时间都花在向Klee提交补丁，以便Klee可以用来验证Rust程序。-↩