proof - 有没有办法证明程序没有错误？

Question

我在想我们可以证明一个程序有错误的事实。我们可以对其进行测试，以评估它或多或少具有抗虫性。

但是有没有办法（甚至理论上）证明一个程序没有错误？

对于简单的程序，比如“Hello World”，我想我们应该可以做到。但是更大的程序呢？

Answer 1

现在有许多不同的形式可以用来证明程序的正确性（例如，证明助手中的形式化、依赖类型的编程语言、分离逻辑……）。正如其他人所指出的，没有自动的方法来证明任何给定的程序是正确的（参见停机问题）。然而，那些提到的形式主义通常适用于特定的程序。（这样的应用程序可能远非自动化，需要大量的创造力。）

另一个非常重要的一点是我们通过证明程序正确或如您所说证明程序没有错误的实际意思。即使使用正式的方法，通常也无法说程序不会出错。原因是形式化方法通常表明程序符合规范。

您可以将规范视为逻辑公式（说明程序的某些属性），将正确性证明视为程序满足该公式（即享有相应属性）的正式证明。由于这种设置，规范之外的所有内容甚至都没有被证明“考虑”。因此，要真正证明程序没有错误，您首先必须写下一个逻辑公式，说明程序何时没有错误。

所以说正式方法通常能够（毫无疑问地）证明程序没有某些类型的错误（取决于使用的规范）可能更诚实。