为什么程序不能被证明？

StackOverflow https://stackoverflow.com/questions/476959

题

为什么计算机程序不能像数学陈述那样被证明？数学证明是建立在其他证明的基础上的，而其他证明又是由更多的证明和公理组成的——我们认为这些真理是不言而喻的。

计算机程序似乎没有这样的结构。如果你编写一个计算机程序，你如何能够采用以前经过验证的作品并用它们来证明你的程序的真实性？你不能，因为不存在。此外，编程的公理是什么？该领域的原子真理？

对于以上问题我没有很好的答案。但软件似乎无法被证明，因为它是艺术而不是科学。如何证明毕加索的作品？

有帮助吗？

解决方案

证明是程序。

节目

形式化验证是的巨大的研究领域。 （参见，例如，卡内基梅隆中的基团。）

许多复杂的程序已被核实;例如，参照写入在Haskell 此内核。

其他提示

只是那些谁带来了不完整小评 - 它不是的情况下的所有的公理系统，只有足够强大的那些

。

换句话说，哥德尔证明了强大到足以描述本身一个公理系统必然是不完全的。这并不意味着这将是无用然而，和其他人的联系，在程序证明各种尝试已经进行了。

对偶问题（编写程序以检查样张）也很有趣。

事实上，您可以编写可证明正确的程序。例如，Microsoft 创建了 C# 语言的扩展，称为 规格# 其中包括一个自动定理证明器。对于java来说，有 ESC/java. 。我确信还有更多的例子。

(编辑:显然，spec# 不再被开发，但是 合约工具将成为.NET 4.0的一部分)

我看到一些海报挥舞着关于 停止问题 或者 不完备性定理 据推测，这会阻止程序的自动验证。这当然不是真的。这些问题只是告诉我们 可能编写无法证明正确或错误的程序. 。这并不妨碍我们构建程序 是 已证明是正确的。

在停机问题仅显示有不能被验证的程序。一个更有趣，更实用的问题是什么类的节目能正式确认。也许每一个程序谁会关心可以（在理论上）进行验证。 <击>在实践中，到目前为止，只有非常小的方案已被证明是正确的。

如果你的话题很感兴趣，让我先推荐戴维·格里斯‘规划的科学’，关于这一主题的经典的入门工作。

它实际上是可以证明正确一定程度的程序。可以写条件和结束条件，然后证明，给定的满足先决条件，执行后所得到的状态将满足后置条件的状态。

地方变得棘手，但是，是循环。对于这些，您还需要找到一个不变的循环，以显示正确的终止，你需要找到在每次循环后剩余迭代的最大可能数量上限功能。你还必须能够表明，这种由至少一个通过循环每次迭代之后降低。

一旦你有了这一切的程序，证明是机械的。但不幸的是，有没有办法自动推导出循环不变和约束功能。人的直觉足以满足简单的情形与小环，但实际上，复杂的程序，迅速成为棘手。

首先，你为什么说“节目不能被证明”？

你是什么意思的 “程序” 呢？

如果通过程序你的意思算法难道你不知道克鲁斯卡的？ Dijkstra的？ MST？普里姆的？二进制搜索？归并？ DP？所有这些东西都有描述其行为的数学模型。

DESCRIBE。数学没有解释为什么东西它只是绘制怎样的画面。我不能向你证明太阳会升起在东明，但我可以告诉它一直在为过去的那个东西的数据。

您表示： “如果你写了一个计算机程序，它是如何，你可以采取以前的工作证明，并用它们来显示你的程序的真相吗？你不能因为没有这样的”

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

我不能告诉你“真理”我一个像我不能显示的语言你“真相”节目。两者都是我们的世界的经验的理解表示。不是“真理”。把所有的胡言乱语抛开我能证明你在数学上是一个合并algorith将与O（nlogn）的性能名单上的元素进行排序，一个Dijkstra算法会发现一个加权图的最短路径，或Euclid算法会发现你最大的两个数字之间的最大公约数。在后一种情况下也许就是我给你找两个数的最大公约数“真相在我的节目”，你不觉得吗？

通过递推方程，我可以划定到您在斐波那契程序是如何工作的。

现在，是计算机编程一门艺术？我当然认为它是。多达数学。

我不来从数学的背景，所以请原谅我的无知，但到底是什么“来证明一个节目”是什么意思？ 你有什么证明？正确性？正确性是程序必须验证是“正确”的规范。但这种规范是由人决定的，你怎么验证这个规范是正确的吗？

在我看来，也有程序错误，因为人类有困难表达他们真正想要的东西。 替代文字http://www.processdevelopers.com/images/PM_Build_Swing.gif

那你证明？缺乏所引起的关注错误？

  

此外，什么是编程的公理？该字段的非常原子的真理？

我TA'ed一门课程叫做合同基于编程（当然主页：的http：// www.daimi.au.dk/KBP2/ ）。在这里我可以从课程（等课程我已经采取了）推断

您必须正式（数学）定义语言的语义。让我们考虑一个简单的编程语言;一个只具有全局变量，整数，INT阵列，算术，IF-THEN-ELSE，同时，分配和什么也不做的[你大概可以使用任何主流语言的子集作为这个“执行”。

这是执行状态将是对列表（变量名，变量的值）。读 “{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（出，A1，A2）是做两个已排序的阵列的合并，并将结果存储在出，一个声明，所有我在接下来的例子中使用的话被正式表示（数学）。然后"{sorted(A1) && sorted(A2)} A := M(A1, A2) {sorted(A) && permutationOf(A, A1 concatened with A2)}"在权利要求THA中号正确实现合并算法。

一个可以尝试使用上述公理（可能会需要几个人。你可能会需要一个循环，一个）来证明这一点。

我希望这说明了一点看起来可能证明程序的正确性等。相信我：它需要的很多的工作，即使是看似简单的算法，证明他们是正确的。我知道，我读了很多尝试; - ）

[如果你这样说的：的您的手在被罚款，这是所有其他的人引起了我的头痛; - ）]

当然，他们可以，如其他人公布。

证明一个非常小的子程序正确是一个很好的锻炼是恕我直言在编程相关的学位课程每一个大学生应该是的需要的做。它给你带来很大的洞察思考如何使你的代码清晰，容易审查的，可维护的。

然而，在现实世界中是有限的实际用途。

首先，就像程序有缺陷，所以做数学证明。如何证明一个数学证明确实是正确的，并没有任何错误？你不能。而对于反例，任何数量的出版数学证明的曾在他们发现，有时年后的错误。

二，你不能证明一个程序，而不必“先天”什么样的程序是应该做一个明确的定义是正确的。但是，什么样的程序是应该做任何明确的定义是一个程序。 （虽然它可能是某种你没有为编译器规范语言的程序）。因此，才可以证明一个程序是正确的，你必须先有另外一个程序，它是相当于在预先知道是正确的。所以QED整个事情是徒劳的。

我会建议追查经典的“没有银弹”布鲁克斯的文章。

即使世界很多这方面的研究..正如其他人所说，一个程序语言中的构造是复杂的，并试图验证或者证明对于任何给定输入时，这只能越来越糟。

然而，许多语言允许的规格，对什么样的输入是可接受的（前提条件），并且还允许指定最终结果（后置条件）。

这样的语言包括：B，事件B，阿达，FORTRAN

。

当然，也有其目的是为了帮助我们证明有关程序的某些属性的工具。例如，为了证明死锁，人们可以通过SPIN紧缩其程序。

也有很多工具，有也帮助我们检测的逻辑错误。这可以通过静态分析（goanna，satabs）或代码的实际执行（GNU的valgrind？）来完成。

然而，没有一个工具，它确实允许人们证明整个程序，从一开始（规格），实施和部署。 B法接近，但其实施的检查是非常非常弱。 （它假定人类是在speicficaiton翻译成implmentation infalible）。

作为一个方面说明，使用B方法时，你会经常发现自己从较小的公理构建复杂的证明。 （而且这同样适用于其他exhasustive定理证明）。

它们可以。我花了很多很多时间作为一个大一的学生做程序的正确性证明。

这不是在宏观尺度上的实际的原因是，写一个程序的证明往往比在写程序的要困难得多。此外，今天的程序员倾向于建立系统，不写功能或程序。

在微观尺度上，我有时会做精神上的各个功能，并趋向于组织我的代码，使他们很容易验证。

有是关于航天飞机软件一篇著名的文章。他们这样做证明，或等同的东西。这是令人难以置信的昂贵和费时。验证该水平可能需要他们，但对于任何类型的消费者或商业软件公司，与当前的技术，你会得到你的午餐被竞争对手谁提供，而成本的1％，99.9％溶液食用。没有人会支付$ 5000的微软Office这是稍微更稳定。

如果你是在寻找信心，替代证明的程序是检测它们。这是更容易理解，并可以被自动化。它还允许这类计划证明其在数学上是不可能的，如上所述。

上述所有，没有证据证明是一个替代的传递的接受测试：*

  • 仅仅因为一个节目真的不会做什么，它说，它的作用，并不意味着它做什么用户想要它做的。

    • 除非 你能证明什么说它不会是什么样的用户说他们想要的。

      • 然后必须证明为什么他们 真正想要的, 因为，作为一个用户，他们几乎肯定不知道他们想要什么。等等。玩归谬法

*不提单元，复盖范围、职能、一体化和所有其他类型的测试。

希望这可以帮助你在道路上。

还没有被这里提到的东西是乙 - 方法这是一个形式化方法为基础的系统。它被用于开发在巴黎地铁的安全系统。 有可用于支持B和事件B的发展，特别是罗丹工具。

您不仅可以证明的程序，你可以让你的电脑从样张建设项目。请参见勒柯克。所以，你甚至不必担心你的执行犯了错误的可能性。

哥德尔定理尽管的......会是什么点？你想什么简单的“真理”来证明？你会想从什么这些真理派生？虽然我可以吃这些话......哪来的实用性？

程序可以证明。它是安静的容易，如果你在这样的语言写出来的新泽西州（SML / NJ）。

的例子标准ML

您声明宽，所以它捕捉大量的鱼。

底线是：一些程序也可以确实地证明是正确的。所有程序都可以的不的被证明是正确的。

下面是一个简单的例子，你要知道，是完全一样的一种证明，在毁于一旦集合论回来的：做一个程序，可以判断自身是否正确，如果发现它的是的正确的，给出一个不正确的答案。

这是哥德尔定理，简单明了。

但是，这也不是那么有问题的，因为我们可以证明许多程序。

让我们假设一个纯粹的功能语言(即Haskell).副作用可以采取相当干净虑到在这样的语言。

证明这一程序产生正确结果需要你来指定：

  1. 一的对应关系之间的数据类型和数学集合
  2. 一的对应关系之间，Haskell的功能和功能的数学
  3. 一套公理指定什么样的功能，只允许从其他人，并相应敷设渠道的数学侧。

这一组规格被称为 denotational义.他们让你到证明的原因有关的程序使用数学。

好消息是，"结构的程序"(第3点以上)和"结构的数学集合"是相当类似(在的时髦词是 topos, 或 笛卡尔的封闭类别)，使1/证明你在数学方面将很容易被转移到方案结构2/程序，你写的很容易显示可以在数学上正确的。

阅读上的停机问题（这是要证明简单的东西的难度作为是否程序完成或没有）。根本问题是关系到哥德尔不完备定理。

一些零部件的程序可以证明。例如,C#编译器，静态地验证和担保的类型安全，如果汇编成功。但我怀疑的核心你的问题是要证明这一程序进行正确。许多(我不敢说最)的算法可以证明是正确的，但是整个程序很可能无法被证明是静态的，原因如下：

  • 核查要求所有可能的分支机构(电话，如果和之前)可以走，其在先进的程序编码具有超立方时间的复杂性(因此，它将永远不会完成在合理的时间)。
  • 一些编程技术，无论是通过制作组件或使用反射，使得它不可能是静态预测的执行的代码(即你不知道如何另一个程序员会使用你的图书馆和编译器已经很难预测反映在消费者将援引的功能。

和那些只是一些...

如果该方案具有良好限定的目标和初始假设（忽略哥德尔...）可以证明。找到所有素数，X，6 <= X <= 10，你的答案是7，并且可以证明。我写了一个节目播放NIM （第一Python程序我写过），并在理论计算机总是赢得比赛落入其中的计算机可以赢得状态之后。我一直没能证明它是真实的，但它是真实的（数学由二进制数字之和证明）我相信，除非我在代码中犯了一个错误。我做出的一个错误，没当回事，可有人告诉我，如果这个方案是不可战胜的？

有已被“证明”以计算机代码像四个色定理。但也有反对意见，因为就像你说的，你能证明程序？

另外，什么是公理的编程？非常原子真理的领域？

是的 操作码 "原子的真相"?例如，在看到...

mov ax,1

...可能不是一个程序员主张作为不言自明的是，除了硬件的问题，之后，执行该声明的CPU ax 登记册将包含现在 1?

如果你写一个计算机程序，它怎么说，你可以把以前的经验证的工作，并利用它们来表演的真相你的计划？

将"以往的工作"然后可能在运行时的环境，在这新的程序运行。

新的程序可以证明：除了正式的证据，可以证明"通过检验"，并通过各种形式的"测试"(包括"可接受性测试").

你怎么证明这一索?

如果软件更像工业设计或工程，比如艺术、更好的问题可能是"你如何证明一座桥，或飞机吗?"

证明程序正确只能相对于程序的规范进行;它是可能的，但昂贵的/耗时

某些CASE系统产生的程序更易于证明比别人 - 但是，这依赖于规范...

的形式语义

...等等，你如何证明规格是否正确？对！随着越来越多的规格！

予读出的位有关这一点，但有两个问题。

首先，你不能证明一些所谓的正确性抽象的东西。你可以，如果事情设置正确，证明了两次正式制度是等价的。您可以证明一个程序实现了一组规范，它是最容易通过构建证明和程序或多或少平行做到这一点。因此，规格必须足够详细，以提供某物，以证明对，和因此本说明书是有效的程序即可。编写一个程序以满足目的的问题变得编写的程序的形式详细说明以满足目的的问题，这并不一定是一个进步。

其次，程序复杂。那么，正确性的证明。如果你能犯了一个错误写一个程序，你肯定可以做一个证明。 Dijkstra算法和格里斯告诉我，从本质上讲，如果我是一个完美的数学家我可以做一个优秀的程序员。这里的价值在于证明和编程两种有所不同的思维过程，并至少在我的经验，我让不同类型的错误。

在我的经验，证明程序的也不是一无是处。当我试图做一些事情，我可以正式地描述，证明了实现正确消除了一大堆难以发现的错误，主要是离开哑的人，我可以在测试中容易赶上。在必须产生极其没有bug的代码的项目，它可以是一个有用的辅助。它不适合于每一个应用程序，它当然是没有银子弹。

正如其他指出的，（部分）程序可以确实得到证明。

在实践中的一个问题是但是，你首先需要的的东西的，你想要的（即假设或定理）来证明。因此，为了证明一些事情，你首先需要的是应该做的正式描述一个程序（如前置和后置条件）。

在换句话说，你需要的节目的正式规范。但是，让即使是合理的（更严格正规的）规范已经是软件开发中最困难的事情之一。因此，一般很难证明的有趣的事情有关（现实世界的）计划。

有然而一些东西可以（已经）更容易形式化（和证实）。如果你至少可以证明你的程序将不会崩溃，这已经不错了： - ）

顺便说一句，一些编译器警告/错误基本上是（简单）关于节目证明。例如，Java编译器将证明，你永远不会在你的代码中访问未初始化的变量（否则它会给你一个编译器错误）。

我没有看过所有的答案，但我看到它的方式，证明方案是没有意义的，这就是为什么没有人做的。

如果你有一个相对小型/中型项目（比如，10K行代码），则证明可能会是也10K线，如果不是很长。

想想看，如果程序有错误，证明也可以有“漏洞”。也许你所需要的证据证明！

另一个要考虑的，程序是非常非常正式和精确。你不能得到任何更加严格和正式的，因为程序代码必须由一个非常愚蠢的机器上执行。

虽然证明要由人类读取，所以它们趋向于比实际的代码那么严格。

你要证明的唯一事情是，关于特定的数据结构操作低电平算法（例如快速排序，插入到二进制树等）。

这些都有些复杂，这不是很明显，为什么他们的工作和/或他们是否会一直工作。他们也是为所有其他软件的基本构建模块。

闹得这里，但我会在风喊无论如何...

“证明正确的”具有在不同的上下文不同的含义。在形式系统时，“证明正确的”是指式可以从其他证明（或不言自明的衍生）公式。 “证明正确的”编程只显示代码等同于正式的规范。但你如何证明正式的规格是否正确？可悲的是，没有办法显示一个规范是无缺陷或解决方案不是通过测试以外的任何实际问题。

只是我的2美分，增添了有趣的东西已经存在。

这不能被证明，最常见的是那些执行IO（与世界或用户的一些unpredictible相互作用）中的所有节目。甚至自动化证明有时只是忘记，“证明”程序”在某些物理硬件，而不是由模型描述的理想之一运行。

在对方的数学证明不关心世界。用数学的重复问题是，如果它描述什么真正的。它提出的每一次新的东西像虚数或者非欧几里得空间的发明。然后，这些新的理论是这样的好工具的问题是遗忘。就像一个好的方案，它只是工作。

许可以下： CC-BY-SA 和 归因
不隶属于 StackOverflow
scroll top