为什么不能像数学陈述一样证明计算机程序？数学证明建立在其他证明的基础上，这些证明建立在更多证明和公理之上——我们认为这些真理是不言而喻的。
计算机程序似乎没有这样的结构。如果你写一个计算机程序，你怎么能把以前证明过的作品拿来用它们来证明你的程序的真实性？你不能，因为不存在。此外，编程的公理是什么？该领域的原子真理？
我对上述问题没有很好的答案。但似乎软件无法被证明，因为它是艺术而不是科学。如何证明毕加索？
问问题
12791 次
31 回答
80
证明是程序。
程序的形式验证是一个巨大的研究领域。（例如，参见卡内基梅隆大学的小组。）
许多复杂的程序已经过验证；例如，查看这个用 Haskell 编写的内核（已修复的 404 链接用于seL4，另请参阅移至位置和项目网站）。
于 2009-01-25T00:57:56.190 回答
32
程序绝对可以被证明是正确的。糟糕的程序很难证明。为了做得更好，您必须改进程序并携手证明。
由于停机问题，您无法自动化证明。但是，您可以手动证明任意语句或语句序列的后置条件和前置条件。
您必须阅读 Dijsktra 的A Discipline of Programming。
然后，您必须阅读 Gries 的《编程科学》。
然后你就会知道如何证明程序是正确的。
于 2009-01-25T00:59:54.317 回答
15
停机问题仅表明存在无法验证的程序。一个更有趣和更实际的问题是可以正式验证哪类程序。也许任何人关心的每个程序都可以（理论上）得到验证。 在实践中，到目前为止，只有非常小的程序被证明是正确的。
于 2009-01-25T00:59:42.413 回答
15
对那些提出不完整性的人来说只是一个小小的评论——并非所有公理系统都是如此，只有足够强大的公理系统。
换句话说，哥德尔证明了一个足以描述自身的公理系统必然是不完整的。然而，这并不意味着它没有用，并且正如其他人所链接的那样，已经对程序证明进行了各种尝试。
双重问题（编写程序来检查证明）也很有趣。
于 2009-01-25T01:01:18.587 回答
15
实际上，您可以编写可证明正确的程序。例如，微软创建了一个名为Spec#的 C# 语言扩展，其中包括一个自动定理证明器。对于 java，有ESC/java。我敢肯定还有更多的例子。
（编辑：显然 spec# 不再被开发，但合约工具将成为 .NET 4.0 的一部分）
我看到一些海报对暂停问题或不完整性定理挥手致意，这可能会阻止程序的自动验证。这当然不是真的；这些问题只是告诉我们有可能编写无法证明正确或不正确的程序。这并不妨碍我们构建可证明是正确的程序。
于 2009-01-25T01:37:25.630 回答
8
如果你真的对这个话题感兴趣，让我先推荐 David Gries 的《The Science of Programming》，这是一本关于这个话题的经典入门著作。
实际上，在某种程度上证明程序是正确的是可能的。您可以编写前置条件和后置条件，然后证明给定一个满足前置条件的状态，执行后的结果状态将满足后置条件。
然而，它变得棘手的地方是循环。对于这些，您还需要找到一个循环不变量并显示正确的终止，您需要在每个循环后剩余的最大可能迭代次数上找到一个上限函数。您还必须能够证明，在循环的每次迭代之后，这至少会减少 1 个。
一旦你为一个程序准备了所有这些，证明是机械的。但不幸的是，没有办法自动导出循环的不变函数和绑定函数。对于具有小循环的琐碎情况，人类的直觉就足够了，但实际上，复杂的程序很快就会变得难以处理。
于 2009-01-25T00:58:53.117 回答
6
首先，你为什么说“程序无法被证明”？
无论如何，您所说的“程序”是什么意思？
如果通过程序你的意思是算法你不知道克鲁斯卡尔的吗？迪杰斯特拉？MST？普里姆？二进制搜索？合并排序？DP？所有这些事物都有描述其行为的数学模型。
描述。数学没有解释事情的原因，它只是描绘了如何。我无法向你证明太阳明天会在东方升起，但我可以显示过去它在哪里做这件事的数据。
你说：“如果你写一个计算机程序，你怎么能把以前证明过的作品拿来用它们来证明你的程序的真实性？你不能，因为不存在”
等待？你不能？ http://en.wikipedia.org/wiki/Algorithm#Algorithmic_analysis
我无法向您展示“真相”，就像我无法向您展示有关语言的“真相”一样。两者都是我们对世界的经验理解的代表。不在“真相”之上。抛开所有的胡言乱语，我可以在数学上向你证明，归并排序算法将以 O(nlogn) 性能对列表中的元素进行排序，Dijkstra 将找到加权图上的最短路径，或者欧几里得算法会发现你是最棒的两个数之间的公约数。在最后一种情况下，“我的程序中的真相”也许是我会找到两个数字之间的最大公约数，你不觉得吗？
通过递归方程，我可以向您描述您的斐波那契程序是如何工作的。
现在，计算机编程是一门艺术吗？我当然认为是。和数学一样。
于 2009-01-25T01:37:26.020 回答
5
我不是来自数学背景，所以请原谅我的无知，但是“证明程序”是什么意思？你在证明什么？正确性？正确性是程序必须验证为“正确”的规范。但是这个规范是由人决定的，你如何验证这个规范是正确的？
在我看来，程序中存在错误是因为人类难以表达他们真正想要的东西。 替代文字 http://www.processdevelopers.com/images/PM_Build_Swing.gif
那你证明什么？注意力不集中导致的bug？
于 2009-01-25T23:31:21.770 回答
4
此外，编程的公理是什么？该领域的原子真理？
我已经完成了一门名为基于合同的编程的课程（课程主页：http ://www.daimi.au.dk/KBP2/ ）。这是我可以从课程中推断出来的（以及我参加过的其他课程）
您必须正式（数学上）定义语言的语义。让我们考虑一种简单的编程语言；一个只具有全局变量、整数、整数数组、算术、if-then-else、while、赋值和无操作[你可以使用任何主流语言的一个子集作为这个的“实现”]。
执行状态将是对（变量名，变量值）的列表。将“{Q1} S1 {Q2}”读作“执行语句 S1 将您从执行状态 Q1 带到状态 Q2”。
一个公理将是"if both {Q1} S1 {Q2} and {Q2} S2 {Q3}, then {Q1} S1; S2 {Q3}"。也就是说，如果语句 S1 将您从状态 Q1 带到 Q2，并且语句 S2 将您从 Q2 带到 Q3，那么“S1；S2”（S1 后跟 S2）将您从状态 Q1 带到状态 Q3。
另一个公理是"if {Q1 && e != 0} S1 {Q2} and {Q1 && e == 0} S2 {Q2}, then {Q1} if e then S1 else S2 {Q2}"。
现在，进行一点改进：{} 中的 Qn 实际上是关于状态的陈述，而不是状态本身。
假设 M(out, A1, A2) 是一个合并两个排序数组并将结果存储在 out 中的语句，并且我在下一个示例中使用的所有单词都被正式表达（数学上）。然后"{sorted(A1) && sorted(A2)} A := M(A1, A2) {sorted(A) && permutationOf(A, A1 concatened with A2)}"是声称 M 正确地实现了合并算法。
可以尝试通过使用上述公理来证明这一点（可能需要其他一些公理。您可能需要一个循环）。
我希望这能说明证明程序正确的样子。相信我：即使是看似简单的算法，也需要大量的工作来证明它们是正确的。我知道，我读了很多尝试 ;-)
[如果你读到这个：你的交接很好，是所有其他的都让我头疼；-)]
于 2009-01-31T03:54:53.010 回答
3
他们当然可以，正如其他人所发布的那样。
证明一个非常小的子程序正确是一个很好的练习，恕我直言，每个与编程相关的学位课程的本科生都应该被要求做。它让您深入了解如何使您的代码清晰、易于审查和维护。
然而，在现实世界中，它的实际用途有限。
首先，就像程序有错误一样，数学证明也有。如何证明数学证明确实正确并且没有任何错误？你不能。举个反例，任何数量的已发表的数学证明都在其中发现了错误，有时甚至是几年后。
其次，如果没有“先验”对程序应该做什么的明确定义，您就无法证明程序是正确的。但是任何对程序应该做什么的明确定义都是程序。（虽然它可能是某种规范语言的程序，但你没有编译器。）因此，在你证明一个程序是正确的之前，你必须首先有另一个等价的程序并且事先知道是正确的。所以 QED 整个事情都是徒劳的。
我建议您参考 Brooks 的经典“ No Silver Bullet ”文章。
于 2009-01-29T21:41:04.387 回答
2
在这方面有很多研究......正如其他人所说，程序语言中的结构很复杂，当尝试验证或证明任何给定的输入时，情况只会变得更糟。
然而，许多语言允许规范，关于哪些输入是可接受的（前置条件），并且还允许指定最终结果（后置条件）。
此类语言包括：B、Event B、Ada、fortran。
当然，有许多工具旨在帮助我们证明程序的某些属性。例如，为了证明死锁自由，可以通过 SPIN 处理他们的程序。
还有许多工具也可以帮助我们检测逻辑错误。这可以通过静态分析（goanna、satabs）或实际执行代码（gnu valgrind？）来完成。
但是，没有一种工具可以真正让人们证明整个程序，从开始（规范）、实施和部署。B 方法很接近，但它的实现检查非常弱。（它假设人类在将规范转化为实现方面是无懈可击的）。
附带说明一下，在使用 B 方法时，您会经常发现自己从较小的公理构建复杂的证明。（这同样适用于其他详尽的定理证明）。
于 2009-01-25T00:49:32.073 回答
2
他们能。作为一名大学新生，我花了很多很多时间做程序正确性证明。
在宏观上它不实用的原因是编写程序的证明往往比编写程序要困难得多。此外，今天的程序员倾向于构建系统，而不是编写函数或程序。
在微观范围内，我有时会在心里为个别功能做这件事，并且倾向于组织我的代码以使它们易于验证。
有一篇关于航天飞机软件的著名文章。他们做证明，或类似的东西。这是非常昂贵和耗时的。这种级别的验证对他们来说可能是必要的，但对于任何类型的消费者或商业软件公司来说，使用当前技术，你的午餐会被竞争对手以 1% 的成本提供 99.9% 的解决方案吃掉。没有人愿意花 5000 美元购买稍微稳定一点的 MS Office。
于 2009-01-25T01:12:25.430 回答
2
如果您正在寻找信心，证明程序的替代方法是测试它们。这更容易理解并且可以自动化。如上所述，它还允许在数学上不可能证明的程序类。
最重要的是，没有任何证据可以替代通过验收测试：*
仅仅因为一个程序确实做到了它所说的，并不意味着它做了用户想要它做的事情。
除非你能证明它所说的就是用户所说的他们想要的。
- 然后你必须证明他们真正想要的是什么，因为作为用户，他们几乎肯定不知道他们想要什么。等等。 荒谬的归约。
*更不用说单元、覆盖率、功能、集成和所有其他类型的测试。
希望这对您的道路有所帮助。
于 2009-01-25T06:01:05.253 回答
2
这里没有提到的是B - Method，它是一个基于正式方法的系统。它被用来开发巴黎地铁的安全系统。有一些工具可用于支持 B 和 Event B 开发，尤其是Rodin。
于 2009-01-25T16:55:54.533 回答
2
您不仅可以证明程序，还可以让您的计算机从证明中构建程序。请参阅Coq。因此，您甚至不必担心在您的实施过程中出现错误的可能性。
于 2009-01-30T17:17:54.263 回答
1
尽管有哥德尔定理......这有什么意义？你想证明什么简单的“真理”？你想从这些真理中得到什么？虽然我可以吃这些话......实用性在哪里？
于 2009-01-25T00:45:32.020 回答
1
程序可以被证明。如果您使用诸如新泽西标准 ML (SML/NJ) 之类的语言编写它们，这将非常容易。
于 2009-01-30T17:35:04.820 回答
1
你的陈述很广泛，所以它钓到了很多鱼。
底线是：某些程序绝对可以被证明是正确的。不能证明所有程序都是正确的。
请注意，这是一个简单的例子，它与过去破坏集合论的证明完全相同：编写一个可以确定自身是否正确的程序，如果它发现它是正确的，则给出错误的答案。
这就是哥德尔定理，简单明了。
但这不是问题，因为我们可以证明很多程序。
于 2009-04-27T08:56:37.673 回答
1
让我们假设一种纯函数式语言（即 Haskell）。在这些语言中可以非常清楚地考虑副作用。
证明程序产生正确的结果需要您指定：
- 数据类型和数学集之间的对应关系
- Haskell 函数和数学函数之间的对应关系
- 一组公理，指定您可以从其他人构建哪些函数，以及数学方面的相应构造。
这组规范称为指称语义。它们允许您证明使用数学的程序的原因。
好消息是“程序的结构”（上面的第 3 点）和“数学集的结构”非常相似（流行语是topos或笛卡尔封闭类别），所以 1/ 你在数学方面所做的证明将很容易地转换为程序结构 2/ 您编写的程序很容易证明在数学上是正确的。
于 2011-07-29T11:53:23.720 回答
0
阅读停止问题（这是关于证明程序是否完成这样简单的事情的难度）。从根本上说，这个问题与哥德尔的不完备定理有关。
于 2009-01-25T00:50:33.243 回答
0
程序的某些部分可以被证明。例如，如果编译成功，静态验证和保证类型安全的 C# 编译器。但我怀疑您问题的核心是证明程序执行正确。许多（我不敢说大多数）算法可以被证明是正确的，但是由于以下原因，可能无法静态地证明整个程序：
- 验证需要遍历所有可能的分支（调用、ifs 和中断），这在高级程序代码中具有超立方时间复杂度（因此它永远不会在合理的时间内完成）。
- 某些编程技术，无论是通过制作组件还是使用反射，都无法静态预测代码的执行（即，您不知道其他程序员将如何使用您的库，编译器很难预测消费者中的反射将如何调用功能。
而这些只是一些...
于 2009-01-25T00:51:32.757 回答
0
此外，编程的公理是什么？该领域的原子真理？
操作码是“原子真理”吗？比如看到...
mov ax,1
... 程序员可能不会断言，除非出现硬件问题，否则在执行此语句后 CPU 的ax寄存器现在将包含1?
如果你写一个计算机程序，你怎么能把以前证明过的作品拿来用它们来证明你的程序的真实性？
那么“以前的工作”可能是新程序运行的运行时环境。
新程序可以被证明：除了形式证明之外，它可以通过“检查”和各种形式的“测试”（包括“验收测试”）来证明。
如何证明毕加索？
如果软件更像工业设计或工程而不是艺术，那么更好的问题可能是“你如何证明一座桥梁或一架飞机？”
于 2009-01-25T00:56:42.700 回答
0
证明程序正确只能相对于程序的规范进行；这是可能的，但昂贵/耗时
一些 CASE 系统产生的程序比其他系统更适合证明——但这又依赖于规范的形式语义......
...那么您如何证明规范正确？对！规格更多！
于 2009-01-25T16:01:38.213 回答
0
我读了一些关于这个，但有两个问题。
首先，你不能证明一些叫做正确性的抽象事物。如果设置正确，您可以证明两个形式系统是等价的。您可以证明一个程序实现了一组规范，并且通过或多或少并行构建证明和程序来做到这一点是最简单的。因此，规范必须足够详细，以提供一些可以证明的东西，因此规范实际上是一个程序。编写程序以满足目的的问题变成了编写程序的正式详细规范以满足目的的问题，这不一定是向前迈出的一步。
第二，程序复杂。正确性证明也是如此。如果您在编写程序时会犯错误，那么您肯定可以进行一次证明。Dijkstra 和 Gries 基本上告诉我，如果我是一个完美的数学家，我可以成为一个优秀的程序员。这里的价值在于证明和编程是两个有些不同的思维过程，至少根据我的经验，我犯了不同类型的错误。
以我的经验，证明程序并不是没有用的。当我尝试做一些我可以正式描述的事情时，证明实现正确可以消除很多难以发现的错误，主要是留下愚蠢的错误，我可以在测试中轻松发现这些错误。在必须生成极无错误代码的项目中，它可能是一个有用的辅助工具。它并不适合所有应用程序，当然也不是灵丹妙药。
于 2009-01-30T18:30:13.600 回答
0
正如其他人指出的那样，（某些）程序确实可以得到证明。
然而，实践中的一个问题是，您首先需要一些您想要证明的东西（即假设或定理）。因此，要证明某个程序的某些内容，您首先需要正式描述它应该做什么（例如，前置条件和后置条件）。
换句话说，您需要程序的正式规范。但是即使是一个合理的（更不用说严格的正式的）规范已经是软件开发中最困难的事情之一了。因此，证明（现实世界）程序的有趣之处通常非常困难。
然而，有些事情可以（并且已经）更容易形式化（和证明）。如果您至少可以证明您的程序不会崩溃，那已经是:-)。
顺便说一句，一些编译器警告/错误本质上是关于程序的（简单）证明。例如，Java 编译器将证明您永远不会在代码中访问未初始化的变量（否则它会给您一个编译器错误）。
于 2009-04-27T11:01:25.813 回答
0
我还没有阅读所有的答案，但我看到它的方式，证明程序是没有意义的，这就是为什么没有人这样做。
如果您有一个相对较小/中型的项目（例如，10K 行代码），那么证明可能也是 10k 行，如果不是更长的话。
想想看，如果程序可以有bug，那么证明也可以有“bug”。也许你需要一个证明来证明！
要考虑的另一件事是，程序非常正式和精确。你不能变得更严格和正式，因为程序代码必须由一台非常愚蠢的机器执行。
虽然证明将被人类阅读，但它们往往不如实际代码严格。
您唯一需要证明的是对特定数据结构进行操作的低级算法（例如快速排序、插入二叉树等）。
这些事情有些复杂，它们为什么起作用和/或它们是否会一直起作用并不是很明显。它们也是所有其他软件的基本构建块。
于 2009-05-07T07:31:01.193 回答
0
大多数答案都集中在实践上，这没关系：在实践中，您并不关心正式的校对。但理论上是什么？
程序可以像数学陈述一样被证明。但不是你说的那个意思！在任何足够强大的框架中，都有无法证明的数学语句（和程序）！看这里
于 2009-11-07T14:57:22.733 回答
0
这里有这么多噪音，但无论如何我都会在风中大喊大叫......
“证明正确”在不同的语境中有不同的含义。在正式系统中，“证明正确”意味着一个公式可以从其他经过证明的（或公理化的）公式推导出来。编程中的“证明正确”只是显示代码等同于正式规范。但是你如何证明正式的规范是正确的？可悲的是，除了通过测试之外，没有办法证明规范没有错误或解决任何现实世界的问题。
于 2010-12-08T19:19:57.567 回答
0
只是我的 2 美分，增加了已经存在的有趣的东西。
在所有无法证明的程序中，最常见的是那些执行 IO（与世界或用户进行一些不可预测的交互）的程序。即使是自动证明有时也会忘记“经过验证的”程序在某些物理硬件上运行，而不是模型描述的理想硬件。
另一方面，数学证明并不关心世界。数学中一个反复出现的问题是它是否描述了任何真实的东西。每当发明虚数或非欧几里得空间等新事物时，它就会被提出。然后这个问题就被遗忘了，因为这些新理论是很好的工具。就像一个好的程序一样，它可以正常工作。
于 2011-11-09T00:43:27.337 回答
0
从不那么抽象的角度来看，证明某事是将不确定性领域减少到已证明的零集的问题。这是一厢情愿的想法，因为在现实世界中无法达到完美。
如果计算机程序的环境没有（或不能）被证明，则计算机程序可以在现实世界中证明是正确的并失败：
必须证明 OS 内核、驱动程序和所有用户模式库和并发执行的程序，包括它们的直接和间接短期和长期副作用，
硬件必须始终按预期运行（包括停电、洪水、地震、EMF 干扰等），
最终用户必须始终按预期行事（著名的因素“X”）。
自动纠错是在各种硬件组件（RAM、磁盘、控制器等）中实现的，但是仍然会发生硬件故障——在provably correct程序中产生级联错误和/或故障。
而且我什至不想对最终用户的创造力进行尾声……
因此，（正确）评级的程序provably correct并不意味着它provably safe在现实生活中。
这意味着，对于定义研究中考虑的集合（只能是现实世界的一个子集），该程序将按预期运行。
于 2012-06-10T10:47:48.633 回答