有没有办法证明程序没有错误? [英] Is there a way to prove a program has no bug?

问题描述

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

但是有没有办法(甚至从理论上)证明程序没有错误?

对于简单的程序，例如"Hello World"，我想我们应该可以做到. 但是大型程序呢?

解决方案

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

另一个非常重要的要点是证明程序正确或您所说的证明程序没有bug 的实际含义.即使使用形式化方法，通常也无法说任何事情都不会出错.原因是形式化方法通常表明程序符合规范.

您可以将规范视为逻辑公式(陈述了程序的某些属性)，而将正确性证明视为程序满足该公式(即享有相应属性)的形式证明.由于这种设置，证明甚至不会考虑"规范之外的所有内容.因此，要真正表明程序没有错误，您首先必须写下一个逻辑公式，指出程序何时没有错误.

所以说正规方法通常能够(毫无疑问)证明程序没有某些种类的错误(取决于所使用的规范)也许会更诚实./p>

I was thinking about the fact that we can prove a program has bugs. We can test it to assess that it is more or less bug resistant.

But is there a way (even theoretically) to prove that a program has no bug ?

For simple programs, such as a "Hello World", I guess we should be able to do it. But what about larger programs ?

解决方案

There are nowadays many different formalisms that can be used to prove programs correct (e.g., formalizations in proof assistants, dependently typed programming languages, separation logic, ...). As noted by others, there is no automatic way to prove any given program correct (see the halting problem). However, those mentioned formalisms are often applicable to specific programs. (Such an application can be far from automatic and require a tremendous amount of creativity.)

Another very important point is what we actually mean by proving a program correct or as you stated prove that a program has no bug. Even with formal methods there is typically no way to say that nothing whatsoever can go wrong with a program. The reason is that formal methods usually show that a program conforms to a specification.

You can think of a specification as a logical formula (that states some property about a program) and of the correctness proof as a formal proof that a program satisfies this formula (i.e., enjoys the corresponding property). Due to this setup, everything outside the specification is not even "considered" by the proof. So to really show that a program has no bugs you would first have to write down a logical formula that states when a program does not have bugs.

So it would maybe be more honest to say that formal methods are often able to prove (without doubt) that a program does not have certain kinds of bugs (depending on the used specification).

这篇关于有没有办法证明程序没有错误?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！