测试驱动开发与自动化定理证明答案

【问题标题】：Test Driven Development vs Automated Theorem Proving测试驱动开发与自动化定理证明
【发布时间】：2009-05-07 07:07:36
【问题描述】：

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

单元测试很方便，但尝试（蛮力）测试浮点模块的每个可能输入几乎是棘手的。相反，您会找到一个证明 (1) 它总是会产生正确的结果，或者 (2) 证明它会产生至少一个不正确的结果。

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

【问题讨论】：

【解决方案1】：

过去我在形式验证方面有很多经验，尽管它是针对硬件组件（VHDL/Verilog）的。相同的原则可以应用于软件，但如果您有任何类型的 I/O 或事件，输入空间就会变得难以管理。由于状态空间变得太大，在大型“模型”上证明任何类型的陈述也是不切实际的。

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

【讨论】：

【解决方案2】：

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

查看其他问题：why cant programs be proven
（注意：链接的问题标题具有误导性 - 某些程序可以被证明，但很难）

【讨论】：

【解决方案3】：

你是说你会在数学上证明你的算法在纸上是正确的，还是写代码来做同样的事情？（我对你将如何做后者很感兴趣 - 如果可能，请链接到博客文章或有关如何在 cmets 中执行此操作的一些解释）

在前一种情况下，如果没有测试，您将无法证明您的实现反映了您的意图并按预期工作。
在后一种情况下，如果定理证明代码不执行实现 - 前面的论点成立。

就我个人而言，我只会使用 TDD - 让我和其他人轻松阅读一堆写得很好的测试并弄清楚代码的作用。更不用说更快了。 您不必测试所有可能的输出，而是确定一组有代表性的输入。每个输入都应该通过代码执行不同的结果/路径。

【讨论】：

【解决方案4】：

始终与测试结合使用。否则你无法证明你的实现实际上与你证明是正确的一致。

【讨论】：

这很有意义。我想我要问的不是是否完全消除测试，而只是在轻量级进行测试（而不是详尽地测试所有代码）。
不要放弃测试负载。您需要对其进行详尽的测试。不同之处主要在于您有一个证明，表明如果它是您证明的算法的实现，那么它将适用于您想要的情况，而不仅仅是在大多数情况下：)