不会出错的程序

计算无处不在。

进入计算机房，听着服务器排成一排的墙之间风扇的噪音，你似乎可以闻到0和1在*处理器和内存之间的连续流动。从计数和计数到今天的计算机，我们用来计算的工具终于开始有质的飞跃。电脑可以做越来越多的事情，甚至超过它们的制造商。上世纪末，深蓝凭借其前所未有的搜索和判断国际象棋的能力，成为第一台击败国际象棋世界冠军的计算机，但它的胜利仍然依赖于人类大师丰富的国际象棋知识。然而，仅仅过了10年，沃森已经能够用自己的算法“理解”这个问题，然后有针对性地在大量数据库中找到相关答案。从长远来看，这种工具将在更多方面超越它的制造者。所有这些都来自越来越复杂的计算。

计算似乎无所不能，就像一个新的上帝。但即使是这个“上帝”也无法逃脱逻辑设定的界限。

图灵是第一个发现这个的人。

我相信每个人都见过蓝色或黑色的窗户。有时因为它，一个上午的工作在一瞬间就被破坏了，这不仅令人沮丧，而且令人抓狂。此时，你会在心里大声诅咒那些不小心让蓝屏一次又一次出现的程序员吗？但是程序员不是铁打的。他们也会犯错。此外，对于商业软件，大量的测试将在上市前进行。即使一些程序错误漏掉了，大部分都可以通过修补来修复。

但是对于一些软件来说，情况要麻烦得多。

1996年一个难以形容的日子，欧洲航天局首次发射了新研制的阿丽亚娜5号运载火箭。起飞后37秒，新的火箭正在盛开。这让欧洲航天局非常不高兴，该机构在这个项目上花费了数亿欧元。经过调查，专家组发现事故的罪魁祸首实际上是一个短代码。

阿丽亚娜5爆炸现场

在阿丽亚娜5的软件中，部分代码直接来自其前身阿丽亚娜4。由于阿丽亚娜4号当时非常成功，每个人都觉得这样做没有问题。只需根据新参数稍微修改代码。问题是修改没有完成。有一行代码需要将64位浮点数转换成16位整数。他们认为不会有任何问题，所以他们没有做任何改变。这段代码也没有经过测试。

这是同一行代码，因为Ariane 5比其前身Ariane 4强大得多，所以在Ariane 4上没有问题的这一行代码在Ariane 5上有一个溢出错误:64位浮点数表示的值超出了16位整数可以表示的范围。出错后，备用代码系统启动，其中包含同一行代码。结果是整个系统被锁住了。更讽刺的是，这一行代码所在的函数对于Ariane 5来说是不必要的。这场事故完全是人为的。

事故发生后，欧洲航天局非常愤怒，决定一劳永逸地解决阿丽亚娜5号的问题。他们的要求相当大胆:Ariane 5软件代码在正式使用之前应该被证明没有破坏性错误，比如没有溢出，没有死循环等等。

这实际上并不容易。

关机定理让我们回顾一下关机问题:有没有一种算法可以确定在给定任何程序和输入的情况下，程序是否会在给定的输入下在有限的时间内停止？是图灵证明了这是不可能的。因此，不可能编写一个算法来判断程序是否会进入死循环。但是我们能使用算法来判断其他类型的程序错误吗？

不幸的是，这也是不可能的。事实上，我们可以将停机时间问题减少到检测错误问题。假设我们有一个程序P，它可以检测某段代码是否会被零除，我们想用这个程序来判断图灵机是否会在给定的输入下停止。我们能做什么？首先，对于给定的图灵机和输入，我们可以机械地将它们转换成不需要除法但可以模拟图灵机的代码。然后，模拟完成后，我们可以强制计算1/0。我们称之为代码T。代码T在执行时将被零除，当且仅当图灵机停止时。然后，我们将代码t输入到程序P中。因此，由于程序P可以确定任何代码是否会出错，这相当于确定任何图灵机会不会停止，这是不可能的。关机问题没有通用算法，也就是说，没有通用算法来证明代码是正确的。

然而，欧洲航天局的任务完全不可能吗？不完全是。关机定理只表明没有程序能正确判断所有程序是否会停止，但欧洲航天局只需要证明阿丽亚娜5的软件代码是无错的，所以道路没有完全堵塞。

那么，我们能做什么呢？

虽然我们不能判断所有的程序是否都会出错，但我们可以有效地判断一些程序是否不会出错。例如，如果程序没有任何循环语句或跳转语句，那么程序最终肯定会停止。但是如果程序有循环语句呢？此时，我们不确定程序是否会停止，最安全的方法是说“我不知道”。

这就是抽象解释方法的本质:首先抽象出程序的一些信息，然后自动分析这些信息，试图确定程序是否具有预期的属性，如无死循环、无溢出等。我们不坚持对所有无错程序进行完美的分析或识别。然而，为了安全起见，我们要求这种分析是可靠的，也就是说，如果分析结果认为程序具有期望的属性，那么这个结论就不会出错。正是因为这种权衡，抽象解释方法才能被正确而有效地实施。

伽罗瓦连接，来自Cousot课件

根据抽象的信息量，不同的抽象解释方法在判断同一属性时有不同的效果。一般来说，提取的信息越详细，可以识别的具有特定属性的程序就越多，相应的计算时间就越长。如何在表现和识别率之间进行选择也是一门复杂的科学。对于不同的应用和数据结构，需要开发不同的抽象方法和自动分析算法。

许多抽象方法还有另一个优点。如果一个程序有我们想要的性质，但是手头的抽象解释方法是不确定的，我们可以转换到一个更精细和更有信息的抽象方法。直接重写代码也是避免分析失败的一种方法。例如，我们想要证明某个代码不会出错，但是某些抽象解释方法表明某个代码可能有问题，因此我们可以通过修改代码并切换到更谨慎的处理方法来确保抽象解释方法可以确认新代码不会出错。

抽象解释方法的创始人是法国的帕特里克·库索特和拉迪亚·库索特。这对夫妇的档案总结了一些程序自动正式证明的方法。在此基础上，他们提出了一种抽象的解释方法来形式化和紧缩它。他们还促进了抽象解释方法的推广。除了Ariane 5代码之外，其他关键应用中的代码也通过抽象解释方法进行了验证。一个例子是空中客车A380的控制代码，该代码已经过阿斯特赖公司的验证，阿斯特赖公司是一个由帕特里克·库绍特团队开发的抽象解释软件。实践证明，这些控制代码在运行时不会造成死循环、溢出或被零除等软件问题，从而增加了一层额外的安全系数。

库索特夫妇，*上的照片

然而，抽象解释方法只能证明程序具有我们想要的某些属性，而不能解释程序是否完成了我们想要的任务。有什么办法吗？

形式证明有一种激进的方法:让程序员编写代码，同时给出数学证明，证明代码确实完成了给定的任务。

要给出这种证明，首先要解决的是如何将“代码已经完成了给定的任务”转化为一个数学命题。程序代码可以很容易地用逻辑表达，但是只有程序员知道代码需要完成什么任务。因此，程序员在编写代码时有必要给出证明，这样程序员就可以用逻辑的形式确定这个函数的功能，从而得到要证明的命题。这种想法不仅仅是一种数学理论。对于一些关键系统，即使是微小的错误也会导致极其严重的后果。人们愿意不惜任何代价防止错误。对于计算机程序来说，有什么比数学更坚实的基础？

为了实现这个想法，在编写程序之前，必须首先选择一个逻辑系统和一种正式的语言来描述它。这种形式语言必须贯穿整个代码编写过程:首先，用形式语言描述程序的输入、输出、功能和限制，然后用类似于形式语言的编程语言编写代码，最后由形式语言给出书面代码能够完美实现所需功能的数学证明。这种方法也被称为演绎验证，是所谓的“形式验证”方法之一。

然而，数理逻辑毕竟不是一门容易的学科。对许多人来说，数学证明可能比编写代码要困难得多。因此，演绎验证将主要应用于那些不能容忍错误的关键系统，例如涉及大量人员的公共交通设施。例如，1998年开始运营的巴黎地铁14号线是一条全自动地铁。火车上没有司机，安全驾驶取决于传感器和软件。调度可以通过点击控制室中的鼠标来增加或减少投入运行的列车数量。因此，安全性在很大程度上取决于软件的可靠性。在控制列车的计算机中，一些与乘客安全密切相关的关键代码是通过演绎验证编写的。2012年，巴黎最古老的地铁1号线也从人工操作转向了与14号线相同系列的全自动系统。目前，两条地铁线路每天接收100多万人，但自动化系统从未造成人员伤亡。根据作者的经验，它们可以被认为是巴黎最可靠的地铁线路。

巴黎地铁14号线，*上的照片

然而，仅仅代码的正确性可能不足以保证程序也是正确的，因为代码毕竟不是程序，并且计算机不能直接执行代码。我们需要另一个叫做“编译器”的程序。编译器将程序员编写的代码翻译成计算机可读的程序，并用机器语言编写。即使代码是正确的，如果编译器有问题，产生的程序仍然可能出错。为了避免这个问题，我们还需要使用数学方法来加强编译器。

实现这一设计概念的一个例子是一个名为CompCert的C编译器，它是由法国计算机科学家Xavier Leroy和他的团队编写的。编译器的任务是执行忠实的代码翻译，以确保源代码和目标代码以相同的方式运行。这非常重要，否则，即使代码正确，也不能保证编译后的程序不会出错。然而，现代编译器不能确保在优化模式下的忠实编译。计算机证书必须解决这个问题。当编写CompCert时，编译器的每一步都附有数学证明，以确保代码的语义保持不变。因此，数学证明的正确性确保了CompCert编译器将代码忠实地翻译成机器语言。

然而，即使机器语言是正确的，最终执行结果的正确性也不能完全保证，因为程序总是需要输入和输出，而这些功能是由操作系统保证的。如果操作系统本身有错误，即使程序本身是正确的，也不能保证我们看到的结果是正确的，因为操作系统的问题。如果你想把数学证明的保证贯彻到底，你还需要在操作系统上努力工作。这就是seL4所做的。SeL4是一个微内核，可以看作是操作系统的核心。它的每一个功能都附有数学证明。在对硬件做出某些假设后，数学证明的正确性可以确保它所提供的功能会产生我们预设的行为。只要没有硬件错误，SeL4就会正常工作。

当然，一个自然的问题是，如果硬件出了问题怎么办？硬件错误可分为逻辑错误和物理错误。前者，如英特尔芯片上的除法错误，早已被主流硬件制造商所了解，他们的硬件设计也通过演绎验证得到了加强。后者，例如，宇宙射线使硬盘数据出错，这是不可避免的，即使它是复杂的证明，一个人只能从自己寻求幸福。虽然数学方法不能保证错误不存在，但至少可以避免所有可以避免的问题，这本身就很有价值。

(或者你能使用宇宙射线吗...？(来自xkcd的图片)