程式設計的公設基礎：四十年後

1969 年，C.A.R. Hoare 在 Communication of the ACM (12(10):576–580) 發表論文 An Axiomatic Basis for Computer Programming，在文中提出後來被稱作 Hoare 邏輯 (Hoare Logic) 的一套公設系統, 被認為是計算科學史上最重要的幾篇論文之一。時間轉眼間過去了，今年已經是這篇論文的四十歲生日。最近 Hoare 應 Communications 之邀，回顧後來的發展。有哪些是他預期的，哪些是他沒料到的？

1960-68 年間，Hoare 仍在業界工作，帶領一個實作 ALGOL 60 編譯器的團隊。ALGOL 的語法用 context-free language 定義得相當精簡優雅，語意卻仍以非形式的方式定義。Hoare 希望有個方式能一方面嚴格描述 ALGOL 的語意，一方面又不限制到編譯器製作者使用各種最佳化方法的自由。這是 Hoare 邏輯的由來。

Hoare 漸漸發現這題目大概可以研究一輩子。而且大概直到他退休，這東西也不會在業界得到廣泛應用。這使他在 1968 年從業界進入學界，而到他 1999 年退休為止，看來這兩個預測都蠻準確的。

令他意外的事情呢？Hoare 說他可以預期程式會越來越大，測試這種大程式也會越來越困難。他沒想到的是測試不僅是用在程式上，更是對人的考驗。通過這種考驗的工程師所培養出的直覺和經驗也是讓軟體可靠的重要因素。形式方法應該去支持程式員的直覺判斷，而非壓抑它。況且開發中的軟體若在測試中表現得很差，剛好可讓開發部門作為說服管理部門延長開發時間的依據。

把測試和證明對立起來的看法也許是個基本錯誤 — 工程師本來就要使用各種有用的工具。形式方法能做的貢獻是盡量提供更好的工具。在他退休並加入微軟劍橋研究中心後，他驚訝地發現 Hoare 邏輯斷言並不是用來證明程式正確性，而是用在測試並發現錯誤上。形式方法在除錯上的應用反倒比證明來得早。

Hoare 的邏輯斷言使用的是標準的邏輯與離散數學。我想後來許多程式語言學者的想法也是盡量設計符合數學模型的程式語言。Hoare 卻說近年來的發展剛好相反：許多數學概念為了分析程式語言的新功能（如物件、classes, heap, 指標等）而發展出來；大家開發新種類的代數，用來描述分散系統、並行系統等等。新的邏輯，如線性邏輯、分離邏輯等為了分析程式的行為而發明，有些還在其他的領域，如計算生物學、基因學、甚至社會學派上用場。

學者們一度相信要等到軟體錯誤造成了大災害，大家才會了解形式方法與軟體驗證的重要。事實卻不然。1996 年 Ariane V 火箭測試發射因軟體故障而失敗後，管理階層的策略是跑更多更嚴密的測試。越嚇他們，他們越會抱緊熟悉的方法不放。對軟體驗證的興趣反倒是從利潤出發：有效地使用形式方法會比較省錢。

而使軟體驗證流行的助力卻來自大家都沒想到的地方：駭客們。駭客攻擊造成大量的金錢損失，而駭客使用的軟體漏洞通常無法經由測試找到。唯一的可能是自動分析並驗證程式碼。這使得資訊安全成為軟體驗證的一大賣點，也由此漸漸推廣到汽車、電子產品、和航太產業中。

Hoare 接著談到業界與學界的不同使命。業界自然是使用最成熟的技術、解決最容易而迫切的問題。但學界的天職是完全相反的：建構最泛用的理論、解釋最多的現象、尋求可長可久的知識。不論哪種科學研究都嘗試回答這一系列的問題：這個東西做什麼？怎麼運作？為什麼能這麼運作？而有什麼證據顯示我們提出的答案是對的？在電腦科學中我們已經大致知道怎麼回答這些問題。一個程式的規格告訴我們它做什麼，斷言和其他內部模組、界面間的約定告訴我們他怎麼運作，程式語言語意解釋它為什麼能這麼運作，數學與邏輯證明增強我們的信心，而現在這些證明可以用電腦和工具產生和檢查。現在電腦科學家的舞台與使命是從事有說服力的實驗，檢驗這些工具和理論是否足以涵蓋今日大部分的程式、設計模式、語言、和應用。「實驗」在此的意義可能是現有應用程式的重新設計，從這些實驗得到的經驗將繼續推動理論與工具的進步。