先穿漁網襪從珠穆朗瑪峰上滾下來哭求CSDN的大大們看一下CSDN部落格插件不能自動上傳圖檔和排版的問題。人肉上傳圖檔和排版真地很痛苦呐！
2007圖靈獎和模型檢驗
不知道長達半年的瘋狂加班是否損害了自己的心理健康。回顧過去幾個月，似乎除了工作嘛都沒幹。人仿佛頹了，覺得時光了無意義地飛逝，過去半年的泰半記憶好像盛夏陽光裡的冰塊，蒸發得不剩一絲水汽。幸好不是全無亮點，比如看到好朋友幸福無比地結婚。中學好友到家裡盤桓月餘，也是一大快事。Steve McConnell在Rapid Development裡的案例分析裡提到death march之後程式員往往大批離開。想不到這次親自體會了一把，人生又完整了一點。過去幾周一系列戲劇性的事件讓我仔細思考了一下激勵團隊士氣的問題，也算小小的收獲。
跑題了。本來想說什麼來着？對了，圖靈獎和模型檢驗。2007年的圖靈獎授予Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis，表彰他們在模型驗證方面做出的開創性貢獻。前段時間白天忙項目，晚上改簡和曆準備面試，也就沒有心情八卦。劉江老師在他的部落格裡做了詳細介紹，在這裡推薦一下。關于幾位大牛，俺沒有什麼補充的，就八卦一下他們的研究方向：模型檢驗。
模型檢驗是計算機科學理論與實踐結合的經典範例，背後也有一段跌宕起伏、絕處逢生的曆史。八卦這段曆史前，我們得知道什麼是模型驗證，以及為什麼它為什麼重要到能得圖靈獎。在CS理論裡，一個模型就是一個數學結構，比如有向圖，或者狀态機。我們往往希望知道一個結構是否符合一定的性質。這些性質可以用邏輯公式表達。比如下面的有向圖G(V, E)裡，V代表所有節點的集合，{A, B, C, D, E}, 而E代表所有路徑的集合{(A, B), (B, C), (D, C), (B, D), (D, B), (E, D), (B, E)}。如果如果我們想驗證G裡沒有從A到C的直接路徑，但有經過一個節點的間接路徑，就可以驗證下面這個公式在G裡面為真。
簡單解釋一下：
- 這種式子叫Tableau。如果分數線上的式子成立，則推斷分數線下的式子也成立。
- {P . B} S {P}即Hoare三段式(Hoare Triple)，意思是如果條件P和B在程式S執行前為真，且程式S運作中止，那麼條件P在S結束運作後依然為真。
- {P} while B do S done {×B . P}的意思是如果P在執行while循環前成立，且循環while B do S done能退出，那麼循環退出後B不再為真，而P依然為真。這裡的P有坨專門稱呼：循環不變量，loop invariant。B也有個诨名，循環護衛，loop guard。
- 從這個式子可以看出，要證明一段循環的結果正确，我們隻需找出循環不變量P，然後再證明兩件事：這段循環可以結束，也就是loop guard能從真值最終變為假，而不變量P一直為真。
不過，驗證程式的思想并沒有興盛起來。原因挺簡單：用基于演繹的方法從基本的定理出發證明整個程式也忒難了。僅僅是找到合适的不變量就足以讓我等凡人抓狂。Dijkstra一輩子都呼籲程式設計應像推導數學定理一樣嚴謹，否則遺患無窮。可總不能要求人人都是戴爺爺級别的牛人吧？何況就算戴爺爺，隻怕也難證明幾千行的驅動程式沒有死鎖。一直到70年代，程式證明在工業界也沒有什麼真正的影響。當然這不是說系統驗證這門學科失去活力。事實上當時Tony Hoare，E.W., Dijkstra，E.A. Ashcroft, David Gries，Robert Floyd等一票大牛們在形式理論上突飛猛進，深入研究了程式的公理化證明，并行程式的斷言證明，程式的推導和不可确定性等一系列課題。自動定理證明也做得有聲有色。這些東西為日後花樣繁多的自動程式驗證奠定了基礎。
眼見實踐方面山窮水盡，以色列的Amir Pnueli 從澡盆裡跳出來了：解決問題之道不在完美方案，而在确定可以解決的問題，以及合适的切入角度。有時候放棄是福。好比當年Multics的老大硬要用幾十頁彙編自動解決context switching時的PC-losering問題，結果搞得代碼維護異常困難。但Dennis Ritche為了實作的簡單，幹脆放棄自動維護，把這個問題交給程式員。以後的故事就是曆史樂。驗證任意系統的正确性太難，就驗證狀态有限的reactive系統嘛。各式硬體和嵌入系統可都是reactive系統。好像用有限狀态機也能完善地描述。既然驗證整個程式太難，就驗證程式的某些特性嘛。大家都覺得測試比證明省錢，我們就專挑測試搞不定的方面嘛。關鍵資料會溢出麼？浮點計算會出錯麼？安全協定有漏洞麼？關鍵資料會被破壞麼？每條程序都能在規定時間内被執行麼？這些好像應用面挺廣，也能用邏輯公式相對容易地描述。測試單寫多讀的玩具并行程式當然比證明簡單。但是發現1962年讓Mariner I Space Probe墜毀大西洋的計算錯誤呢？1986年讓Therac-25過量輻射X射線緻死病人的錯誤呢？1995年導緻Intel大規模回收晶片的浮點錯誤呢？1996年導緻阿裡亞娜5号火箭墜毀的整數溢出錯誤呢？
系統的狀态随時間而變，更不必說并發系統的狀态同程式執行的時機緊密相連。當我們開始研究程式的行為，而不僅是程式的輸入輸出時，就不可避免同時間打交道。是以，我們需要一套全新的工具，不僅能簡潔地描述系統的時态，還不用陷入對具體時間的瑣碎處理。目光銳利的Pnuelli看上了時序邏輯。于是1977年，開創性的論文，Temporal Logics of Programs（程式的時序邏輯），問世樂。Pnuelli在論文裡提出用時序邏輯證明程式的正确性。時序邏輯曆史悠久，亞裡士多德就對一階二進制謂詞邏輯做過不少研究。它的關鍵思想是把時間看作一系列離散的狀态。狀态間的傳遞等同于時間的延續。Pnuelli提出的是線性時序邏輯(Linear Temporal Logic, LTL)。LTL在一階命題邏輯的基礎上引入了幾坨與時間有關的操作符。
抛開命題邏輯的黑話，我們每天都用到命題邏輯，無非就是把邏輯陳述用邏輯操作符連接配接起來。下面的例子是一坨命題表達式：×(i > 0 . i < 10) 其中i>0和i<10是陳述(statement)，符号×是操作符邏輯非，相當于C裡的!，中間的.是邏輯與的操作符，相當于C裡的&&。命題邏輯的局限在于它導出的真相一成不變。比如在華為這個世界裡（黑話叫model或者domain或者world，看你怎麼歸類了），陳述“加班就是好”永遠是對的，不管是項目吃緊的時候，還是項目符合進度的時候，哪怕有人累死，有人甯願跳樓也不跳槽，有人寫出2000行的函數，有人連熬幾十小時後回家睡覺也算曠工，這個陳述都為真。那我們要表達“總有某個時候，加班不好”就沒辄了。為了解決這個問題，LTL就在命題邏輯的基礎上加入了時序操作符：
- G：表示永遠為真。比如G(i < 0)表示i在任意時間都小于0。
- F：表示最終為真。比如F(i < 0)表示i在某個時間一定小于0（但現在不一定小于0）。
- X：表示下一個時刻為真。比如X(i < 0)表示時鐘跳到下一個時刻，i就必須小于0。
- U：表示直到某刻前一直為真。比如(i < 0) U (j < 0)表示i一直小于0，直到j變得小于0。
- R：表示到了某刻才為真。比如(i < 0) R (j < 0)表示j 一直小于0，直到某個時刻i變得小于0。
其實{G, F, X}中任取一個，{U，R}中任取一個，就足以構成完備的LTL操作符。有興趣的老大可以自行證明。有了這些操作符，我們就可以友善地描述系統的時态性質了。這裡列舉幾個LTL模式庫裡的例子（是滴，LTL Properties Specification Patterns, 誰說搞理論的老大們不與時俱進來着？
例1：
當系統發出打開網絡連接配接的請求後，如果遇到網絡錯誤，必須彈出一段錯誤資訊。我們用OpeningNetworkConnection表示網絡連接配接的請求已經發出，用NetworkError表示網絡錯誤被傳回，而ErrorMessage表示彈出錯誤資訊。
公式是：G(OpenNetworkConnection->G(NetworkError-> F(ErrorMessage)))
我們從内向外分析：
- NetworkError -> F(ErrorMessage)表示如果NetworError為真，那麼ErrorMessage最終一定會為真。也就是說網絡錯誤發生後，一定會在未來某個時候出現錯誤資訊。
- G(NetworkError -> F(ErrorMessage))則表示1.陳述的性質在任何時候都要成立。
- OpenNetworkConnection –> G(NetworkError-> F(ErrorMessage))進一步說明，當網絡連接配接打開後，我們可以肯定2.的陳述總是為真。
- 最後，G(OpenNetworkConnection->G(NetworkError-> F(ErrorMessage)))說明3.裡的陳述在任何時刻都為真。
例2：
很多系統裡都需要排程任務。對任意任務，我們要求把任務加入排程表前，不應該從排程表裡取消該任務。我們用register表示加入任務，用unregister表示取消任務，那麼公式可以寫作F(register) -> (!unregister U register)，意思是如果任務最終被加入排程表，我們可以推知該任務從未在加入排程表前被取消過。
雖說時序邏輯讓Pnuelli得了1996年的圖靈獎，工業界仍然波瀾不驚。這大概是因為用時序邏輯證明程式性質依然屬于從基本定理出發的演繹，難度依然太大，代價依然高昂。證明之于程式員，好比彙編之于DBA。申明式程式設計才是王道。我們希望給出系統的設計或實作，描述一些性質，剩下的便交給程式，讓程式判斷系統是否滿足這些性質。如果不滿足，則給出反例，以便排錯。而這，正是模型驗證做的事。
我們已經知道系統的性質可以用時序邏輯描述。現在還缺的，就是合适的模型，以及相配的算法。