下界(通过测试)与上限(通过证明)的正确性

Question

克里斯·史密斯的文章“辩论类型系统前要知道的内容”包含以下未解释的声明：

Testing: establishes upper bounds on correctness Proof: establishes lower bounds on correctness

上下文是比较验证程序正确性(例如与类型检查器)和测试程序行为(例如，使用动态类型语言中的TDD )的好处。

在这种情况下，正确性的“上”和“下”界限是什么？

Answer 1

假设你有一个程序，而你根本不知道它是如何工作的。它应该有很多属性(例如，X、Y和Z)，但你不能确定它是否有。你能做什么才能弄清楚这件事？

一种选择是尝试使用程序验证工具来正式证明程序具有X、Y和Z属性。不幸的是，通常不可能自动验证程序是否有任何有趣的属性(谢谢，停止问题！)，所以即使程序实际上具有这些属性，您也可能永远无法确定这一点。但是，如果程序检查程序报告程序确实具有X属性，那么您可以说，程序至少可以做到X。在这个意义上，程序的正确性是“较低的”：它肯定具有属性X，并且可能还有更多的属性。

另一种选择是运行程序，看看会发生什么。假设在测试期间，您发现了一个导致程序行为不当的测试用例，因此绝对没有属性Z。不过，您的测试用例没有暴露任何其他错误。在这种情况下，因为你看到程序行为不当，你肯定知道它没有Z属性。因此，你有“上限”程序是正确的-它绝对没有属性Z，但你不能排除任何其他的。

如果把这两者结合起来，你就得到了一个证据，证明你的程序有X属性，你有直接证据证明它没有Z属性。你不知道它是否有Y属性，因为这两者都没有解决。

希望这能有所帮助！