别想轻松读懂，但保证值得读懂。
拿出你的笔记本，坐下，深呼吸，开始阅读。
程序猿看完请留步，很想知道你们是否喜欢这样的文章，欢迎通过评论反馈。
相信每个人都见识过Windows那令人忧郁的蓝屏或者黑屏吧。有时因为它，一个上午的工作一瞬间毁于一旦，这就不仅是令人忧郁而是令人抓狂了。在这个时候，你是否会在心中大声咒骂那帮写程序不小心让蓝屏一而再再而三出现的程序员呢？但程序员也不是铁打的，他们也会犯错误。而且对于商业软件来说，在上市之前会进行大量的测试，即使有程序错误溜过去了，大多也可以通过打补丁来修复。
但是对于某些软件来说，情况就麻烦得多了。
在1996年的一个不能说的日子，欧洲航天局第一次发射了新研制的Ariane 5运载火箭。在起飞37秒之后，新火箭很想不开地开花了。这令砸了几亿欧元进去的欧洲航天局非常不爽。经过调查，专家组发现，事故的罪魁祸首竟然是短短的一段代码。
Ariane 5爆炸场景
在Ariane 5的软件中，有一部分代码是直接来自它的前辈Ariane 4。由于Ariane 4当时非常成功，所以大家觉得这样做没什么问题，根据新的参数稍微修改一下代码就好了。问题是，修改并不完全。有一行代码需要将64位浮点数转换成16位整数，他们认为不会出现什么问题，所以没有进行修改。也没有测试这段代码。
就是这行代码，因为Ariane 5比前辈Ariane 4强力得多，于是在Ariane 4上没有问题的这行代码，在Ariane 5上发生了溢出错误：那个64位的浮点数代表的数值超出了16位整数可以表达的范围。在出错后，备用代码系统被启动，其中包含着同样的一行代码。结果就是整个系统被锁死了。更为讽刺的是，这行代码所在的函数，对于Ariane 5来说是不必要的。这场事故完全就是人祸。
经过这场事故之后，欧洲航天局大为震怒，决定要一劳永逸地解决Ariane 5的问题。他们的要求相当大胆：Ariane 5的软件代码，正式使用前要证明它们不会出现毁灭性的错误，比如不会溢出，不会死循环等等。
这其实并非易事。
我们复习一下停机问题：是否存在一种算法，给定任意的程序和输入，都能在有限的时间内判断该程序在给定的输入下是否会停止？正是图灵，证明了这一点是不可能做到的。于是，要编写一个能判断程序会不会进入死循环的算法，这是不可能的。但对于其他类型的程序错误，能否用算法判定呢？
很可惜，这也是不可能的。实际上，我们可以将检测错误的问题转化为停机问题。比如说，我们希望检测程序中有没有除以零的错误。那么，我们可以先在程序结尾添加一个死循环，让它永远不能停止运行，然后在程序中每一处除法前，先检测除数是否为零，在除数为零时，强行停止程序。那么，原本的程序不会出现错误，当且仅当改动后的程序不会停机。于是，我们就将证明某段代码不存在某种错误，规约为停机问题。停机问题不存在普遍的算法，也就是说证明代码无误同样没有普遍算法。
但是，欧洲航天局的任务是否完全不可能完成呢？那倒也不是。停机定理只是说明了不存在程序能正确判定所有程序是否会停止，但欧洲航天局只需要证明Ariane 5的软件代码这一个程序不会出错，所以这条路也没有完全被堵死。
那么，有什么办法呢？
虽然我们不能判定所有程序是否不会出错，但我们能有效判定某些程序不会出错。比如说，如果一个程序没有任何循环语句或者跳转语句，那么这个程序最终肯定停止。但如果程序有循环语句又怎么办？这时，我们并不能确定程序会不会停止，而最保险的办法就是说“我不知道”。
这就是抽象释义（Abstract Interpretation）方法的根本：先抽象出程序的某些信息，再对这些信息进行自动分析，来尝试确定程序是否有着我们想要的性质，比如说不会死循环、不会溢出等等。我们不强求完美的分析，不强求能够识别出所有不出错程序。但为了安全起见，我们要求这种分析是可靠的，也就是说，如果分析的结果认为程序有着我们想要的性质，那么这个结论就不会出错。正是因为这样的权衡取舍，抽象释义方法才能正确有效地实行。
Galois connection，来自Cousot课件
根据抽象出来的信息多少，不同的抽象释义方法判断同一种性质的效果也不一样。一般来说，抽象出的信息越详细，能识别的拥有某种性质的程序就越多，相应地计算时间也越长。如何在性能和识别率之间做取舍，也是一门复杂的学问，对于不同的应用和数据结构，需要开发不同的抽象方法和自动分析算法。
多种抽象方法还有另一个优点。如果某个程序有着我们想要的性质，但是手头上的抽象释义方法又不能确定时，我们可以换用更精细的、利用更多信息的抽象方法。直接改写代码也是一种规避分析失败的方法。例如，我们想要证明某段代码不会出错，但某种抽象释义方法指示在某句代码上可能会有问题，那么我们可以通过修改代码，换用更加谨慎的处理方法，来保证抽象释义方法能确认新的代码不出问题。
抽象释义方法的奠基者是法国的Patrick Cousot和Radhia Cousot。这对夫妻档总结了一些对程序进行自动形式证明的方法，在此之上提出了抽象释义方法，将其形式化严格化。他们对抽象释义方法的推广也功不可没。除了Ariane 5的代码之外，在别的一些关键应用处的代码也利用抽象释义方法进行了至关重要的验证。一个例子是空中客车A380的控制代码，经过Patrick Cousot的一个小组开发的抽象释义软件Astrée验证，证明了这些控制代码运行时，不会产生像死循环、溢出或者被零除之类的一些软件问题，从而也给安全系数多加了一层保险。
Cousot夫妇，图片来自Wikipedia
不过，抽象释义方法只能证明程序有着某种我们想要的性质，不能说明程序是否完成了我们希望的任务。有没有办法做到这一点呢？
有一种激进的做法：让程序员在编写代码的同时，给出这段代码确实完成了给定任务的数学证明。
要给出这种证明，首先要解决的就是如何将“代码完成了给定任务”转换成数学命题。程序代码可以相当容易用逻辑表达，但代码需要完成什么任务，这只有程序员才知道。所以，要让程序员在编写代码的同时给出证明，为的是让程序员能用逻辑的形式确定这个函数的功能，如此才能得到要证明的命题。这种想法不仅仅是数学家的纸上谈兵。对于某些关键系统，多么微小的疏失都会导致极其严重的后果，人们愿意几乎不惜一切代价防止错误的发生，而对于计算机程序而言，又有什么比数学更坚实的基础呢？
要贯彻这种想法，在编写程序之前，必须先选择一种逻辑体系以及描述它的一种形式语言。这种形式语言必须贯穿整个代码编写的过程：先用形式语言描述程序的输入、输出、功能与限制，然后利用这种与形式语言相近的编程语言去具体编写代码，最后还要利用形式语言给出编写的代码能完美无瑕疵地实现所需功能的数学证明。这种做法又被称为演绎验证，是所谓的“形式化验证”的手段之一。
但数理逻辑毕竟不是一门容易的学科，数学证明对于很多人来说大概比编写代码要困难得多。所以，演绎验证多数也只会用在那些不容有失的关键系统，比如说牵涉人数众多的公共交通设施。例如，在1998年开始运营的巴黎地铁14号线，就是一条全自动的地铁，列车上没有司机，安全行驶也全靠传感器和软件，调度也只需要在控制室点点鼠标就能增加或减少投入运营的列车数量。于是，安全在很大程度上在于软件的可靠性。在控制列车的计算机中，某些与乘客安全休戚相关的关键代码是利用演绎验证编写的。在2012年，巴黎历史最悠久的地铁1号线也从人工运营转到与14号线同系列的全自动化系统。现在，这两条地铁线每天接待的人数加起来超过一百万，但从未因为自动化系统的错误导致乘客伤亡。从笔者的经验来说，它们可以算是巴黎最可靠的地铁线。
巴黎地铁14号线，图片来自Wikipedia
但仅有代码的正确性可能还不足以保证程序同样正确，因为代码毕竟不是程序，计算机不能直接执行代码。我们需要另一种名为“编译器”的程序。编译器是将程序员写的代码翻译成计算机能读懂的、用机器语言写就的程序。即使代码是正确的，如果编译器有问题，得出的程序还是可能出错。要避免这个问题，我们同样需要利用数学方法加固编译器这一环。
贯彻这种设计理念的一个例子是一个叫CompCert的C编译器，它由法国计算机科学家Xavier Leroy和他的小组编写。编译器的任务就是进行忠实的代码翻译，确保源代码和目标代码的行为一致。这一点至关重要，否则即使代码是正确的，也不能保证编译生成的程序不出问题。然而，现代的编译器在优化模式下，其实并不能确保忠实的编译。CompCert要解决的就是这个问题。在编写CompCert的时候，对于编译程序的每一步操作，都附带一个数学证明，确保代码的语义不变。因此，数学证明的正确性保证了CompCert编译器会完全忠实地将代码翻译成机器语言。
但即使机器语言是正确的，也还不能完全保证最后执行结果的正确性，因为程序总需要输入输出，而这些功能是由操作系统保证的。如果操作系统本身有错误，即使执行的程序本身是正确的，由于操作系统的问题，也不能保证我们看到的结果是正确的。如果想将数学证明的保证贯彻到底，还需要对操作系统下工夫。这就是seL4所做的事情。seL4是一个微内核，可以看成操作系统的核心。它的每一个功能都附带一个数学证明，在对硬件做一定的假设之后，数学证明的正确性可以保证它提供的功能都会产生我们预先设定的行为。只要硬件不出错，seL4就会正确运行。
当然，一个自然的问题是，如果硬件出错怎么办？硬件的错误可以分为逻辑性错误和物理性错误。前者例如Intel当年在芯片上除法的错误，现在主流硬件厂商早已吸取教训，用演绎验证的方法加固他们的硬件设计；后者例如宇宙射线令硬盘数据出错，这即使是多复杂的证明也避免不了，只能自求多福。尽管数学方法不能保证错误不存在，但至少将可以避免的问题全数避免，这本身就有着莫大的价值。
（或者可以利用宇宙射线……？）（图片来自xkcd）
联系客服
