不會出錯的程序 是這樣煉成的

Liming

相信每個人都見識過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/

thunderccx

軟件技術又向前走了一步