国产毛片a精品毛-国产毛片黄片-国产毛片久久国产-国产毛片久久精品-青娱乐极品在线-青娱乐精品

電子工程網(wǎng)

標題: 不會出錯的程序是這樣煉成的 [打印本頁]

作者: Liming 時間: 2011-6-30 23:13
標題: 不會出錯的程序是這樣煉成的
相信每個人都見識過Windows那令人憂郁的藍屏吧。有時因為它，很多天的工作毀于一旦，在這個時候，你是否會在心中大罵那幫不細心的程序員呢？程序員不是上帝，他們也會犯錯誤。對于商業(yè)軟件來說，在上市之前會進行大量的測試，即使有程序錯誤溜過去了，大多也可以通過打補丁來修復(fù)。但是對于某些軟件來說，情況就麻煩得多。
程序錯誤導(dǎo)致的無妄之災(zāi)
在1996年的一個日子，歐洲航天局第一次發(fā)射了新研制的Ariane 5運載火箭。在起飛37秒之后，新火箭很想不開地開花了。這令砸了幾億歐元進去的歐洲航天局非常不爽。經(jīng)過調(diào)查，專家組發(fā)現(xiàn)，事故的罪魁禍首竟然是短短的一段代碼。

在Ariane 5的軟件中，有一部分代碼是直接從它的前輩Ariane 4上扒下來的。正是這行代碼，在Ariane 4上沒有問題，在Ariane 5上卻發(fā)生了溢出錯誤。更為諷刺的是，這行代碼所在的函數(shù)，對于Ariane 5來說是不必要的。這場事故完全就是人禍。

經(jīng)過這場事故之后，歐洲航天局怒了，決定要一勞永逸地解決Ariane 5的問題。他們的要求相當大膽：Ariane 5的軟件代碼，正式使用前要證明它們不會出現(xiàn)毀滅性的錯誤，比如不會溢出，不會死循環(huán)等等。

但問題是，這其實不是一件容易的事情。

停機定理意味著神奇的檢驗程序不可能存在
假設(shè)有一個程序R，可以正確判定任意別的程序P在某個輸入I上會不會死循環(huán)，而且它本身總是會停止的。那么，我寫一個程序P1，它從6開始，逐一驗證每個偶數(shù)是不是可以分成兩個素數(shù)的和，如果遇到某一個偶數(shù)不可以這樣分解的話就返回退出。那么，當這個程序出現(xiàn)死循環(huán)，就能說明哥德巴赫猜想是對的。而死循環(huán)我們只要用程序R就可以驗證。同樣道理，所有數(shù)學(xué)命題，只要能寫一個程序驗證，都可以用R來判斷這些命題是對是錯，我們的神奇程序R蘊含了一切數(shù)學(xué)的秘密。

不過，世上不會有這么好的事情，因為這個程序R是不可能存在的。我們可以用反證法：假設(shè)R存在，我們來寫一個程序RR，它接受一個輸入I，這個I既能看成程序，也能看成輸入，然后用R去判斷程序I在輸入I上會不會停止。如果會停止的話，就進入死循環(huán)，否則就停止。簡單的代碼如下：

RR(I){
if(R(I,I)=stop)
while(1);
else
return;
}

所以，RR(I)停止當且僅當I(I)死循環(huán)。

那么，R(RR,RR)的結(jié)果會是怎么樣呢？它判斷的是RR(RR)是否會停止。但由上面結(jié)論可知，RR(RR)停止當且僅當RR(RR)死循環(huán)，這明顯是矛盾的！所以，這樣的神奇程序R并不存在。

這就是著名的停機定理。也就是說，不存在這樣一個程序，自己總會停止，又可以判定別的程序會不會停止。這就說明了，要證明程序不會出錯，不是一件看上去那么容易的事情。

那么歐洲航天局的任務(wù)是否完全不可能完成呢？也不是。停機定理只是說明了不存在程序能正確判定所有程序是否會停止，但歐洲航天局只需要證明Ariane 5的軟件代碼這個程序不會出錯，所以這條路也沒有完全被堵死。

那么，有什么辦法呢？

用抽象釋義方法吧
雖然我們不能判定所有程序是否不會出錯，但我們能有效判定某些程序不會出錯。

比如說如果一個程序沒有任何循環(huán)語句或者跳轉(zhuǎn)語句，那么這個程序是肯定會停止的，因為只能從頭到尾順序執(zhí)行。那么，如果程序有循環(huán)語句，我們該怎么辦呢？單靠這個信息，我們并不能確定程序會不會停止，那么最保險的辦法就是說“我不知道”。

這就是抽象釋義（Abstract Interpretation）方法的根本：我們抽象出程序的某些信息，對這些信息進行自動分析，來嘗試確定程序是否有著我們想要的性質(zhì)，比如不會死循環(huán)、不會溢出等等。我們不強求這種分析能識別出所有符合我們要求的程序，但我們要求這種分析是可靠的，也就是說，如果分析的結(jié)果認為程序有我們想要的性質(zhì)，那么事實就確實是這樣。正是因為這樣的權(quán)衡取舍，抽象釋義方法才能正確有效地實行。

根據(jù)抽象出來的信息多少，不同的抽象釋義方法判斷同一種性質(zhì)的效果也不一樣。一般來說，抽象出的信息越詳細，能識別的擁有某種性質(zhì)的程序就越多，相應(yīng)地計算時間也越長。如何在性能和識別率之間做取舍，也是一門復(fù)雜的學(xué)問，需要開發(fā)不同的抽象方法和自動分析算法。

如果我們感覺某個程序有著我們想要的性質(zhì)，但是手頭上的抽象釋義方法又不能確定這一點，那么我們可以換用別的更精細的、利用更多信息的抽象方法進行分析。另一種途徑就是直接改寫程序本身。比如說我們想要證明某段代碼不會溢出，但手頭上的抽象釋義方法指示在某句代碼上可能會有溢出，那么我們可以通過修改代碼，換用更加謹慎的處理方法，來保證抽象釋義方法能確認新的代碼不會溢出。

抽象釋義方法的奠基者是法國的Patrick Cousot和Radhia Cousot。這對夫妻檔總結(jié)了一些對程序進行自動形式證明的方法，在此之上提出了抽象釋義方法，將其形式化嚴格化。抽象釋義方法的一個實際應(yīng)用例子是空中客車A380的控制代碼，經(jīng)過Patrick Cousot的一個小組開發(fā)的抽象釋義軟件Astrée驗證，證明了這些控制代碼運行時，不會產(chǎn)生像死循環(huán)、溢出或者被零除之類的一些軟件問題，從而也給安全系數(shù)多加了一層保險。

不過，抽象釋義方法只能證明程序有著某種我們想要的性質(zhì)，不能說明程序是否完成了我們希望的任務(wù)。有沒有辦法做到這一點呢？

用形式證明吧
有一種激進的做法：讓程序員在編寫代碼的同時，給出這段代碼確實完成了給定任務(wù)的數(shù)學(xué)證明。

要給出這種證明，首先要解決的就是如何將“代碼完成了給定任務(wù)”轉(zhuǎn)換成數(shù)學(xué)命題。程序代碼可以相當容易用邏輯表達，而且也有軟件可以自動地將代碼翻譯成要處理的數(shù)學(xué)對象。但我們要代碼完成什么任務(wù)，這個就只有我們才知道，這就是為什么要讓程序員在編寫代碼的同時給出證明，這就是為了程序員能用邏輯的形式確定這個函數(shù)的功能，這樣才能得到要證明的命題。

但是，現(xiàn)在的程序動輒幾十萬行，要是用人力來證明的話，那恐怕要幾個數(shù)學(xué)家花幾個月的時間才能完成，那成本就很高了。能不能用電腦來幫我們做這個證明呢？

看起來不太可能，但的確有人在干這種事情。在法國的一幫計算機學(xué)者搞出來了一個數(shù)學(xué)證明輔助程序，叫Coq，在法語里邊是公雞的意思。本來他們開發(fā)這個程序的本意，正是嘗試用它來幫助程序員完成某些機械的證明過程。因為證明某個程序不會出錯的過程也相當機械的，所以用它也沒問題。Coq中有很多自動證明的策略，可以在很大程度上幫助程序員快速完成這類證明。

貫徹這種設(shè)計理念的是由法國計算機科學(xué)家Xavier Leroy帶頭編寫的，一個叫CompCert的C編譯器。

編譯器是將一種代碼翻譯成另一種代碼的工具，它的任務(wù)就是進行忠實的代碼翻譯，確保源代碼和目標代碼的行為一致。但是編譯器未必可靠，錯誤編譯的情況時有發(fā)生，如果關(guān)鍵的系統(tǒng)出現(xiàn)問題，那么像Ariane 5那樣的事故可能又會再次發(fā)生，而且問題更加隱蔽不易察覺。
而CompCert就解決了這個問題。在編寫CompCert的時候，Xavier Leroy他們對于編譯程序的每一步操作，都利用Coq給出了一個數(shù)學(xué)證明，確保代碼的語義（也就是說代碼應(yīng)該干什么）在每一步都是不變的。合起來，他們就證明了CompCert編譯器在整個編譯過程中保持了代碼的語義，會將代碼忠實地翻譯成程序。

如果所有程序都有這樣的數(shù)學(xué)保障的話，那么我們大概就再也不用受軟件錯誤之苦了。但是，Coq的表達能力還相當有限，比如說C語言中的指針等概念，Coq還不能很好地表達出來。要想完全擺脫軟件錯誤，我們還有很長的一段路要走。

有興趣的同學(xué)可以去Astrée和Coq看看：

Astrée的官網(wǎng)是http://www.astree.ens.fr/ ，Coq的官網(wǎng)是http://coq.inria.fr/

作者: thunderccx 時間: 2011-7-11 17:34
軟件技術(shù)又向前走了一步

歡迎光臨電子工程網(wǎng) (http://m.qingdxww.cn/)