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

Question

我在想我们可以证明一个程序有错误.我们可以对其进行测试,以评估它是否或多或少具有抗虫性.

但有没有办法(甚至在理论上)证明程序没有错误？

对于简单的程序,例如"Hello World",我想我们应该能够做到.但是大型项目呢？

Answer 1

现在有许多不同的形式可以用来证明程序的正确性(例如,证明助手的形式化,依赖类型的编程语言,分离逻辑......).正如其他人所指出的那样,没有自动的方法来证明任何给定的程序是正确的(参见暂停问题).但是,那些提到的形式主义通常适用于具体的计划.(这样的应用程序可能远非自动化,需要大量的创造力.)

另一个非常重要的一点是我们通过证明程序正确或正如您所说的证明程序没有错误而实际意味着什么.即使使用正式的方法,通常也没有办法说任何程序都不会出错.原因是形式化方法通常表明程序符合规范.

您可以将规范视为逻辑公式(表示程序的某些属性)和正确性证明,作为程序满足此公式的正式证明(即,享有相应的属性).由于这种设置,证据之外甚至没有"考虑"规范之外的所有内容.因此,要真正显示程序没有错误,首先必须写下一个逻辑公式,说明程序何时没有错误.

因此,可能更诚实地说,正式方法通常能够(毫无疑问地)证明程序没有某些类型的错误(取决于使用的规范).