测试驱动开发vs自动化定理证明

Question

我对数字逻辑/体系结构设计感兴趣的一件事是自动化定理证明，例如，验证浮点乘法模块。

单元测试很方便，但尝试测试(蛮力)浮点模块的每一个可能的输入几乎是难以处理的。相反，您要么找到(1)它将始终生成正确结果的证明，要么(2)找到表明它将至少生成一个错误结果的证明。

我现在正在尝试将类似的逻辑集成到我的软件中，我想知道我是否可以将它与测试驱动开发结合使用，或者用它来代替测试驱动开发？

Answer 1

听起来你是在尝试构建“经过数学验证的软件”，这是一件非常非常难实现的事情。

查看其他问题：why cant programs be proven

(注意:链接的问题标题具有误导性-一些程序可以证明，但它很难)

Answer 2

在过去，我有相当多的正式验证经验，尽管它是针对硬件组件(VHDL/Verilog)的。同样的原则也可以应用于软件，但如果您有任何类型的I/O或事件，输入空间将变得无法管理。当状态空间变得太大时，在一个大的“模型”上证明任何类型的陈述也是不切实际的。

理想情况下，您可以使用“计算”函数上的定理证明器来证明它们的正确性。但是，出于以下几个原因，仍应使用测试：

，

• ，你的定理中可能有“bug”。如果编写定理的人是实际编写被测试代码的人，则这尤其“危险”。
• 被测试的定理通常是不完整的。
• 您必须在测试环境中放置断言，以确保用于代码输入(“环境”)的假设是有效的。

Answer 3

你是说你会在纸上从数学上证明你的算法是正确的，还是编写代码来做同样的事情？(我对后者很感兴趣-如果可能，请链接到博客帖子或在评论中解释如何做到这一点)

在前一种情况下，如果没有测试，您无法证明您的实现反映了您的意图并按预期工作。

在后一种情况下，如果定理证明代码没有执行实现-前面的参数成立。

就我个人而言，我只会使用测试驱动开发，因为它是我和其他人的easy，用来阅读一堆写得很好的测试，并弄清楚代码是做什么的。更不用说更快的了。您不必测试每一个可能的输出--而是确定一组有代表性的输入。每个输入应该在代码中使用不同的结果/路径。