不會(huì)出錯(cuò)的程序 是怎樣煉成的
相信每個(gè)人都見識(shí)過Windows那令人憂郁的藍(lán)屏吧。有時(shí)因?yàn)樗芏嗵斓墓ぷ鳉в谝坏?，在這個(gè)時(shí) 候，你是否會(huì)在心中大罵那幫不細(xì)心的程序員呢?程序員不是上帝，他們也會(huì)犯錯(cuò)誤。對(duì)于商業(yè)軟件來說，在上市之前會(huì)進(jìn)行大量的測試，即使有程序錯(cuò)誤溜過去 了，大多也可以通過打補(bǔ)丁來修復(fù)。但是對(duì)于某些軟件來說，情況就麻煩得多。
程序錯(cuò)誤導(dǎo)致的無妄之災(zāi)
在1996年的一個(gè)日子，歐洲航天局***次發(fā)射了新研制的Ariane 5運(yùn)載火箭。在起飛37秒之后，新火箭很想不開地開花了。這令砸了幾億歐元進(jìn)去的歐洲航天局非常不爽。經(jīng)過調(diào)查，專家組發(fā)現(xiàn)，事故的罪魁禍?zhǔn)拙谷皇嵌潭痰囊欢未a。
在Ariane 5的軟件中，有一部分代碼是直接從它的前輩Ariane 4上扒下來的。正是這行代碼，在Ariane 4上沒有問題，在Ariane 5上卻發(fā)生了溢出錯(cuò)誤。更為諷刺的是，這行代碼所在的函數(shù)，對(duì)于Ariane 5來說是不必要的。這場事故完全就是人禍。
經(jīng)過這場事故之后，歐洲航天局怒了，決定要一勞永逸地解決Ariane 5的問題。他們的要求相當(dāng)大膽：Ariane 5的軟件代碼，正式使用前要證明它們不會(huì)出現(xiàn)毀滅性的錯(cuò)誤，比如不會(huì)溢出，不會(huì)死循環(huán)等等。
但問題是，這其實(shí)不是一件容易的事情。
停機(jī)定理意味著神奇的檢驗(yàn)程序不可能存在
假設(shè)有一個(gè)程序R，可以正確判定任意別的程序P在某個(gè)輸入I上會(huì)不會(huì)死循環(huán)，而且它本身總是會(huì)停止的。那么，我寫一個(gè)程序P1，它從6開始，逐一驗(yàn) 證每個(gè)偶數(shù)是不是可以分成兩個(gè)素?cái)?shù)的和，如果遇到某一個(gè)偶數(shù)不可以這樣分解的話就返回退出。那么，當(dāng)這個(gè)程序出現(xiàn)死循環(huán)，就能說明哥德巴赫猜想是對(duì)的。而 死循環(huán)我們只要用程序R就可以驗(yàn)證。同樣道理，所有數(shù)學(xué)命題，只要能寫一個(gè)程序驗(yàn)證，都可以用R來判斷這些命題是對(duì)是錯(cuò)，我們的神奇程序R蘊(yùn)含了一切數(shù)學(xué) 的秘密。
不過，世上不會(huì)有這么好的事情，因?yàn)檫@個(gè)程序R是不可能存在的。我們可以用反證法：假設(shè)R存在，我們來寫一個(gè)程序RR，它接受一個(gè)輸入I，這個(gè)I既 能看成程序，也能看成輸入，然后用R去判斷程序I在輸入I上會(huì)不會(huì)停止。如果會(huì)停止的話，就進(jìn)入死循環(huán)，否則就停止。簡單的代碼如下：
- RR(I){
- if(R(I,I)=stop)
- while(1);
- else
- return;
- }
所以，RR(I)停止當(dāng)且僅當(dāng)I(I)死循環(huán)。
那么，R(RR,RR)的結(jié)果會(huì)是怎么樣呢?它判斷的是RR(RR)是否會(huì)停止。但由上面結(jié)論可知，RR(RR)停止當(dāng)且僅當(dāng)RR(RR)死循環(huán)，這明顯是矛盾的!所以，這樣的神奇程序R并不存在。
這就是著名的停機(jī)定理。也就是說，不存在這樣一個(gè)程序，自己總會(huì)停止，又可以判定別的程序會(huì)不會(huì)停止。這就說明了，要證明程序不會(huì)出錯(cuò)，不是一件看上去那么容易的事情。
那么歐洲航天局的任務(wù)是否完全不可能完成呢?也不是。停機(jī)定理只是說明了不存在程序能正確判定所有程序是否會(huì)停止，但歐洲航天局只需要證明Ariane 5的軟件代碼這個(gè)程序不會(huì)出錯(cuò)，所以這條路也沒有完全被堵死。
那么，有什么辦法呢?
用抽象釋義方法吧
雖然我們不能判定所有程序是否不會(huì)出錯(cuò)，但我們能有效判定某些程序不會(huì)出錯(cuò)。
比如說如果一個(gè)程序沒有任何循環(huán)語句或者跳轉(zhuǎn)語句，那么這個(gè)程序是肯定會(huì)停止的，因?yàn)橹荒軓念^到尾順序執(zhí)行。那么，如果程序有循環(huán)語句，我們?cè)撛趺崔k呢?單靠這個(gè)信息，我們并不能確定程序會(huì)不會(huì)停止，那么最保險(xiǎn)的辦法就是說“我不知道”。
這就是抽象釋義(Abstract Interpretation)方法的根本：我們抽象出程序的某些信息，對(duì)這些信息進(jìn)行自動(dòng)分析，來嘗試確定程序是否有著我們想要的性質(zhì)，比如不會(huì)死循 環(huán)、不會(huì)溢出等等。我們不強(qiáng)求這種分析能識(shí)別出所有符合我們要求的程序，但我們要求這種分析是可靠的，也就是說，如果分析的結(jié)果認(rèn)為程序有我們想要的性 質(zhì)，那么事實(shí)就確實(shí)是這樣。正是因?yàn)檫@樣的權(quán)衡取舍，抽象釋義方法才能正確有效地實(shí)行。
根據(jù)抽象出來的信息多少，不同的抽象釋義方法判斷同一種性質(zhì)的效果也不一樣。一般來說，抽象出的信息越詳細(xì)，能識(shí)別的擁有某種性質(zhì)的程序就越多，相應(yīng)地計(jì)算時(shí)間也越長。如何在性能和識(shí)別率之間做取舍，也是一門復(fù)雜的學(xué)問，需要開發(fā)不同的抽象方法和自動(dòng)分析算法。
如果我們感覺某個(gè)程序有著我們想要的性質(zhì)，但是手頭上的抽象釋義方法又不能確定這一點(diǎn)，那么我們可以換用別的更精細(xì)的、利用更多信息的抽象方法進(jìn)行 分析。另一種途徑就是直接改寫程序本身。比如說我們想要證明某段代碼不會(huì)溢出，但手頭上的抽象釋義方法指示在某句代碼上可能會(huì)有溢出，那么我們可以通過修 改代碼，換用更加謹(jǐn)慎的處理方法，來保證抽象釋義方法能確認(rèn)新的代碼不會(huì)溢出。
抽象釋義方法的奠基者是法國的Patrick Cousot和Radhia Cousot。這對(duì)夫妻檔總結(jié)了一些對(duì)程序進(jìn)行自動(dòng)形式證明的方法，在此之上提出了抽象釋義方法，將其形式化嚴(yán)格化。抽象釋義方法的一個(gè)實(shí)際應(yīng)用例子是空 中客車A380的控制代碼，經(jīng)過Patrick Cousot的一個(gè)小組開發(fā)的抽象釋義軟件Astrée驗(yàn)證，證明了這些控制代碼運(yùn)行時(shí)，不會(huì)產(chǎn)生像死循環(huán)、溢出或者被零除之類的一些軟件問題，從而也給 安全系數(shù)多加了一層保險(xiǎn)。
不過，抽象釋義方法只能證明程序有著某種我們想要的性質(zhì)，不能說明程序是否完成了我們希望的任務(wù)。有沒有辦法做到這一點(diǎn)呢?
用形式證明吧
有一種激進(jìn)的做法：讓程序員在編寫代碼的同時(shí)，給出這段代碼確實(shí)完成了給定任務(wù)的數(shù)學(xué)證明。
要給出這種證明，首先要解決的就是如何將“代碼完成了給定任務(wù)”轉(zhuǎn)換成數(shù)學(xué)命題。程序代碼可以相當(dāng)容易用邏輯表達(dá)，而且也有軟件可以自動(dòng)地將代碼翻 譯成要處理的數(shù)學(xué)對(duì)象。但我們要代碼完成什么任務(wù)，這個(gè)就只有我們才知道，這就是為什么要讓程序員在編寫代碼的同時(shí)給出證明，這就是為了程序員能用邏輯的 形式確定這個(gè)函數(shù)的功能，這樣才能得到要證明的命題。
但是，現(xiàn)在的程序動(dòng)輒幾十萬行，要是用人力來證明的話，那恐怕要幾個(gè)數(shù)學(xué)家花幾個(gè)月的時(shí)間才能完成，那成本就很高了。能不能用電腦來幫我們做這個(gè)證明呢?
看起來不太可能，但的確有人在干這種事情。在法國的一幫計(jì)算機(jī)學(xué)者搞出來了一個(gè)數(shù)學(xué)證明輔助程序，叫Coq，在法語里邊是公雞的意思。本來他們開發(fā) 這個(gè)程序的本意，正是嘗試用它來幫助程序員完成某些機(jī)械的證明過程。因?yàn)樽C明某個(gè)程序不會(huì)出錯(cuò)的過程也相當(dāng)機(jī)械的，所以用它也沒問題。Coq中有很多自動(dòng) 證明的策略，可以在很大程度上幫助程序員快速完成這類證明。
貫徹這種設(shè)計(jì)理念的是由法國計(jì)算機(jī)科學(xué)家Xavier Leroy帶頭編寫的，一個(gè)叫CompCert的C編譯器。
編譯器是將一種代碼翻譯成另一種代碼的工具，它的任務(wù)就是進(jìn)行忠實(shí)的代碼翻譯，確保源代碼和目標(biāo)代碼的行為一致。但是編譯器未必可靠，錯(cuò)誤編譯的情況時(shí)有發(fā)生，如果關(guān)鍵的系統(tǒng)出現(xiàn)問題，那么像Ariane 5那樣的事故可能又會(huì)再次發(fā)生，而且問題更加隱蔽不易察覺。
而CompCert就解決了這個(gè)問題。在編寫CompCert的時(shí)候，Xavier Leroy他們對(duì)于編譯程序的每一步操作，都利用Coq給出了一個(gè)數(shù)學(xué)證明，確保代碼的語義(也就是說代碼應(yīng)該干什么)在每一步都是不變的。合起來，他們 就證明了CompCert編譯器在整個(gè)編譯過程中保持了代碼的語義，會(huì)將代碼忠實(shí)地翻譯成程序。
如果所有程序都有這樣的數(shù)學(xué)保障的話，那么我們大概就再也不用受軟件錯(cuò)誤之苦了。但是，Coq的表達(dá)能力還相當(dāng)有限，比如說C語言中的指針等概念，Coq還不能很好地表達(dá)出來。要想完全擺脫軟件錯(cuò)誤，我們還有很長的一段路要走。
有興趣的同學(xué)可以去Astrée和Coq看看：
Astrée的官網(wǎng)是http://www.astree.ens.fr/ ，Coq的官網(wǎng)是http://coq.inria.fr/
原文鏈接：http://www.guokr.com/article/47868/
【編輯推薦】
