为什么不能证明程序？

为什么计算机程序不能像数学陈述那样被证明？一个数学证明是建立在其他证明之上的,这些证据是从更多的证据和公理中建立起来的 - 我们认为这些真理是真实的.

计算机程序似乎没有这样的结构.如果您编写计算机程序,那么您如何能够获取以前经过验证的作品并使用它们来展示您的计划的真实性？你不能存在.此外,编程的公理是什么？这个领域的原子真理？

我对上面的内容没有很好的答案.但似乎软件无法被证明,因为它是艺术,而不是科学.你如何证明毕加索？

1> A. Rex..：

---

证明是程序.

对计划进行正式核查是一个巨大的研究领域.(例如,参见卡内基梅隆大学的小组.)

许多复杂的程序已经过验证; 例如,看看用Haskell编写的这个内核.

---

我已经成功地完成了整个大学生涯以及我职业生涯的前几年,不知何故,我从未被介绍过这个令人敬畏的领域.感谢您的链接,这真是有趣的东西!

2> S.Lott..：

---

程序绝对可以被证明是正确的.糟糕的程序很难证明.为了做得更好,你必须进行程序和手头证明.

由于暂停问题,您无法自动化证明.但是,您可以手动证明任意语句或语句序列的后置条件和前置条件.

你必须阅读Dijsktra的A编程学科.

然后,你必须阅读格里斯的编程科学.

然后你就会知道如何证明程序是正确的.

---

Dijkstra +1; -1对于愚蠢的计算机!=评论中的人类辩论; 获得术语术语+1; -1表示浪费评论空间; 为Dijkstra +1 ;-)

---

人类在某种程度上对停止问题有神奇的免疫力吗？当然你可以自动化证明......

---

@一个.雷克斯:如果你设计一个程序停止,你可以证明它确实是否确实停止了.对于任意程序,不一定设计为停止,你无法证明它是否停止.

---

让我把这个问题归结为一个问题:你是否认为我们作为人类可以证明计算机从根本上不能解决的问题(可能是循环的终止),因为停止问题？

---

我也不明白为什么人们在证明正确性时会从根本上优于计算机.

3> John D. Cook..：

---

暂停问题仅表明存在无法验证的程序.一个更有趣,更实际的问题是可以正式验证哪类程序.也许任何人关心的程序都可以(在理论上)得到验证. 实际上,到目前为止,只有非常小的程序被证明是正确的.

4> Sumudu Ferna..：

---

对那些提出不完整性的人来说只是一个小小的评论 - 对于所有公理系统而言,情况并非如此,只有足够强大的系统.

换句话说,Godel证明了一个足以描述自身的公理系统必然是不完整的.然而,这并不意味着它无用,并且正如其他人所关联的那样,已经进行了各种程序证明的尝试.

双重问题(编写检查证明的程序)也很有趣.

5> Wim Coenen..：

---

事实上,您可以编写可证明正确的程序.例如,微软已经创建了一种名为Spec#的C#语言扩展,其中包括一个自动化定理证明器.对于java,有ESC/java.我相信还有更多的例子.

(编辑:显然规格#不再开发,但合同工具将成为.NET 4.0的一部分)

我看到有些海报在停止问题或不完整性定理上挥手致意,这些定理可能会妨碍程序的自动验证.这当然不是真的; 这些问题只是告诉我们,编写无法证明是正确或不正确的程序是可能的.这并不妨碍我们从构建哪些程序是可证明是正确的.

---

nicerobot:你不明白."程序不能被证明"与"无法证明定理"的意义相同 - 不可能证明它们全部*.许多单独的程序*可以通过证明许多单个定理的相同方式得到证明.

6> Boojum..：

---

如果你真的对这个话题感兴趣,那么我首先推荐David Gries的"编程科学",这是一个关于这个主题的经典入门着作.

实际上可以在某种程度上证明程序是正确的.您可以编写前置条件和后置条件,然后证明给定满足前提条件的状态,执行后的结果状态将满足后置条件.

然而,它变得棘手的是循环.对于这些,您还需要找到循环不变量并显示正确的终止,您需要在每个循环后剩余的最大迭代次数上找到上限函数.您还必须能够证明每次迭代循环后这至少减少一次.

一旦你掌握了所有这些程序,证明就是机械的.但不幸的是,没有办法自动派生循环的不变和绑定函数.对于具有小循环的琐碎案例,人类的直觉就足够了,但实际上,复杂的程序很快变得难以处理.

7> andandandand..：

---

首先,你为什么说"程序无法证明"？

无论如何,"节目"是什么意思？

如果通过程序你意味着算法,你不知道Kruskal的吗？Dijkstra的？MST？普里姆的？二进制搜索？归并？DP？所有这些东西都有描述其行为的数学模型.

描述.数学没有解释为什么它只是简单地描绘了如何.我不能向你证明太阳明天会在东方升起,但我可以向他们展示过去曾经做过这件事的数据.

你说:"如果你写了一个计算机程序,你怎么能把以前经过验证的作品用来表明你的程序的真实性？你不能不存在"

等待？你不能吗？ http://en.wikipedia.org/wiki/Algorithm#Algorithmic_analysis

我不能告诉你"真相"我是一个程序,因为我无法向你展示语言的"真相".两者都代表了我们对世界的经验性理解.不是"真相".把所有的胡言乱语放在一边我可以用数学方法向你证明,mergesort算法会对列表中的元素进行排序,其中O(nlogn)性能,Dijkstra将在加权图上找到最短路径,或者Euclid算法会找到你最大的两个数字之间的公约数.在最后一个案例中,"我的计划中的真相"也许我会发现你是两个数字之间最大的常见除数,你不觉得吗？

通过递推方程,我可以描述您的Fibonacci程序是如何工作的.

现在,计算机编程是一门艺术吗？我当然认为是.和数学一样多.

8> Nicolas Dori..：

---

我不是来自数学背景,所以请原谅我的无知,但"证明一个程序"是什么意思？你在证明什么？正确吗？正确性是程序必须验证为"正确"的规范.但是这个规范是由人决定的,你如何验证这个规范是否正确？

在我看来,程序中存在缺陷,因为人类难以表达他们真正想要的东西. alt text http://www.processdevelopers.com/images/PM_Build_Swing.gif

那你在证明什么？缺乏关注造成的错误？