tdd - 测试驱动开发与自动定理证明

Question

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

单元测试很方便，但尝试测试(蛮力)每个可能的浮点模块输入几乎是棘手的。相反，您会发现 (1) 它总是会生成正确结果的证据，或者 (2) 表明它至少会生成一个错误结果的证据。

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

Answer 1

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

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

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