|
|
|
相信每个人都见识过Windows那令人忧郁的蓝屏吧。有时因为它，很多天的工作毁于一旦，在这个时候，你是否会在心中大骂那帮不细心的程序员呢？程序员不是上帝，他们也会犯错误。对于商业软件来说，在上市之前会进行大量的测试，即使有程序错误溜过去了，大多也可以通过打补丁来修复。但是对于某些软件来说，情况就麻烦得多。
程序错误导致的无妄之灾
在1996年的一个日子，欧洲航天局第一次发射了新研制的Ariane 5运载火箭。在起飞37秒之后，新火箭很想不开地开花了。这令砸了几亿欧元进去的欧洲航天局非常不爽。经过调查，专家组发现，事故的罪魁祸首竟然是短短的一段代码。
在Ariane 5的软件中，有一部分代码是直接从它的前辈Ariane 4上扒下来的。正是这行代码，在Ariane 4上没有问题，在Ariane 5上却发生了溢出错误。更为讽刺的是，这行代码所在的函数，对于Ariane 5来说是不必要的。这场事故完全就是人祸。
经过这场事故之后，欧洲航天局怒了，决定要一劳永逸地解决Ariane 5的问题。他们的要求相当大胆：Ariane 5的软件代码，正式使用前要证明它们不会出现毁灭性的错误，比如不会溢出，不会死循环等等。
但问题是，这其实不是一件容易的事情。
停机定理意味着神奇的检验程序不可能存在
假设有一个程序R，可以正确判定任意别的程序P在某个输入I上会不会死循环，而且它本身总是会停止的。那么，我写一个程序P1，它从6开始，逐一验证每个偶数是不是可以分成两个素数的和，如果遇到某一个偶数不可以这样分解的话就返回退出。那么，当这个程序出现死循环，就能说明哥德巴赫猜想是对的。而死循环我们只要用程序R就可以验证。同样道理，所有数学命题，只要能写一个程序验证，都可以用R来判断这些命题是对是错，我们的神奇程序R蕴含了一切数学的秘密。
不过，世上不会有这么好的事情，因为这个程序R是不可能存在的。我们可以用反证法：假设R存在，我们来写一个程序RR，它接受一个输入I，这个I既能看成程序，也能看成输入，然后用R去判断程序I在输入I上会不会停止。如果会停止的话，就进入死循环，否则就停止。简单的代码如下：
RR(I){
if(R(I,I)=stop)
while(1);
else
return;
}
所以，RR(I)停止当且仅当I(I)死循环。
那么，R(RR,RR)的结果会是怎么样呢？它判断的是RR(RR)是否会停止。但由上面结论可知，RR(RR)停止当且仅当RR(RR)死循环，这明显是矛盾的！所以，这样的神奇程序R并不存在。
这就是著名的停机定理。也就是说，不存在这样一个程序，自己总会停止，又可以判定别的程序会不会停止。这就说明了，要证明程序不会出错，不是一件看上去那么容易的事情。
那么欧洲航天局的任务是否完全不可能完成呢？也不是。停机定理只是说明了不存在程序能正确判定所有程序是否会停止，但欧洲航天局只需要证明Ariane 5的软件代码这个程序不会出错，所以这条路也没有完全被堵死。
那么，有什么办法呢？
用抽象释义方法吧
虽然我们不能判定所有程序是否不会出错，但我们能有效判定某些程序不会出错。
比如说如果一个程序没有任何循环语句或者跳转语句，那么这个程序是肯定会停止的，因为只能从头到尾顺序执行。那么，如果程序有循环语句，我们该怎么办呢？单靠这个信息，我们并不能确定程序会不会停止，那么最保险的办法就是说“我不知道”。
这就是抽象释义（Abstract Interpretation）方法的根本：我们抽象出程序的某些信息，对这些信息进行自动分析，来尝试确定程序是否有着我们想要的性质，比如不会死循环、不会溢出等等。我们不强求这种分析能识别出所有符合我们要求的程序，但我们要求这种分析是可靠的，也就是说，如果分析的结果认为程序有我们想要的性质，那么事实就确实是这样。正是因为这样的权衡取舍，抽象释义方法才能正确有效地实行。
根据抽象出来的信息多少，不同的抽象释义方法判断同一种性质的效果也不一样。一般来说，抽象出的信息越详细，能识别的拥有某种性质的程序就越多，相应地计算时间也越长。如何在性能和识别率之间做取舍，也是一门复杂的学问，需要开发不同的抽象方法和自动分析算法。
如果我们感觉某个程序有着我们想要的性质，但是手头上的抽象释义方法又不能确定这一点，那么我们可以换用别的更精细的、利用更多信息的抽象方法进行分析。另一种途径就是直接改写程序本身。比如说我们想要证明某段代码不会溢出，但手头上的抽象释义方法指示在某句代码上可能会有溢出，那么我们可以通过修改代码，换用更加谨慎的处理方法，来保证抽象释义方法能确认新的代码不会溢出。
抽象释义方法的奠基者是法国的Patrick Cousot和Radhia Cousot。这对夫妻档总结了一些对程序进行自动形式证明的方法，在此之上提出了抽象释义方法，将其形式化严格化。抽象释义方法的一个实际应用例子是空中客车A380的控制代码，经过Patrick Cousot的一个小组开发的抽象释义软件Astrée验证，证明了这些控制代码运行时，不会产生像死循环、溢出或者被零除之类的一些软件问题，从而也给安全系数多加了一层保险。
不过，抽象释义方法只能证明程序有着某种我们想要的性质，不能说明程序是否完成了我们希望的任务。有没有办法做到这一点呢？
用形式证明吧
有一种激进的做法：让程序员在编写代码的同时，给出这段代码确实完成了给定任务的数学证明。
要给出这种证明，首先要解决的就是如何将“代码完成了给定任务”转换成数学命题。程序代码可以相当容易用逻辑表达，而且也有软件可以自动地将代码翻译成要处理的数学对象。但我们要代码完成什么任务，这个就只有我们才知道，这就是为什么要让程序员在编写代码的同时给出证明，这就是为了程序员能用逻辑的形式确定这个函数的功能，这样才能得到要证明的命题。
但是，现在的程序动辄几十万行，要是用人力来证明的话，那恐怕要几个数学家花几个月的时间才能完成，那成本就很高了。能不能用电脑来帮我们做这个证明呢？
看起来不太可能，但的确有人在干这种事情。在法国的一帮计算机学者搞出来了一个数学证明辅助程序，叫Coq，在法语里边是公鸡的意思。本来他们开发这个程序的本意，正是尝试用它来帮助程序员完成某些机械的证明过程。因为证明某个程序不会出错的过程也相当机械的，所以用它也没问题。Coq中有很多自动证明的策略，可以在很大程度上帮助程序员快速完成这类证明。
贯彻这种设计理念的是由法国计算机科学家Xavier Leroy带头编写的，一个叫CompCert的C编译器。
编译器是将一种代码翻译成另一种代码的工具，它的任务就是进行忠实的代码翻译，确保源代码和目标代码的行为一致。但是编译器未必可靠，错误编译的情况时有发生，如果关键的系统出现问题，那么像Ariane 5那样的事故可能又会再次发生，而且问题更加隐蔽不易察觉。
而CompCert就解决了这个问题。在编写CompCert的时候，Xavier Leroy他们对于编译程序的每一步操作，都利用Coq给出了一个数学证明，确保代码的语义（也就是说代码应该干什么）在每一步都是不变的。合起来，他们就证明了CompCert编译器在整个编译过程中保持了代码的语义，会将代码忠实地翻译成程序。
如果所有程序都有这样的数学保障的话，那么我们大概就再也不用受软件错误之苦了。但是，Coq的表达能力还相当有限，比如说C语言中的指针等概念，Coq还不能很好地表达出来。要想完全摆脱软件错误，我们还有很长的一段路要走。
有兴趣的同学可以去Astrée和Coq看看：
Astrée的官网是http://www.astree.ens.fr/ ，Coq的官网是http://coq.inria.fr/
|
|
发表于 2011-6-30 23:13:13
