C. A. R. Hoare（Tony Hoare）如何把程式變成可證明？Quicksort、Hoare Logic 與 CSP

C. A. R. Hoare（Tony Hoare）如何把程式變成可證明？Quicksort、Hoare Logic 與 CSP

Tony Hoare 的工作位置

C. A. R. Hoare 通常以 Tony Hoare 的名字被記住，但他的貢獻不只是一個排序演算法。讀者真正應該追問的是：程式的行為如何被精確描述，如何在不執行所有輸入的情況下推理正確性，又如何在多個程序同時活動時談論彼此的互動？Hoare 把演算法、邏輯、語言規格與並行模型放在同一條研究線上，讓軟體從一份能跑的文字變成可以提出條件、證明和反例的對象。

牛津大學人物頁稱他為 Sir Tony Hoare FRS FREng、榮休教授與 Wolfson College 榮休研究員；牛津的追悼資料則記錄他 1977 年加入牛津、建立 Programming Research Group，並在 1980 年獲 ACM Turing Award。這些頭銜不應取代技術細節，而是提醒我們他的研究橫跨大學、工業與長期方法論。把他的名字只和 Quicksort 綁在一起，會漏掉對軟體工程更持久的影響。

Hoare 的起點帶有跨學科色彩。他在牛津讀哲學、拉丁文和希臘文，對數學邏輯如何說明真理的確定性產生興趣，後來在莫斯科研究機器翻譯與機率。這段經歷有助於理解他為何重視語意和推理，但不應被寫成單一天才故事；排序需求、團隊實作、學生研究和產業合作同樣構成他的技術環境。

本文用三個尺度整理這條路線：Quicksort 關心資料如何被分割與重組，Hoare logic 關心命令前後的條件如何連接，CSP 關心程序透過事件如何互相等待。三者都使用形式結構，但答案並不相同。演算法可以在特定輸入上給出正確輸出，邏輯可以證明一段程式滿足規格，並行模型則還要處理互動順序和死結可能。

Quicksort、Hoare Logic 與 CSP 的工程工作

Quicksort 的核心是分割。先選擇一個樞紐或等價的分割基準，再把資料重新排列，使某一側的元素不大於基準、另一側的元素不小於基準，最後對兩個子範圍遞迴處理。它不必建立與輸入同樣大小的第二個排序陣列，因而在記憶體使用和快取區域性上具有吸引力；真正的實作細節則包括索引移動、相等值、空區間與遞迴結束條件。

分割正確不等於整體排序正確。每次迭代都要維持一個不變量，例如已掃描區域的元素已經落在樞紐相對應的一側；迴圈結束時，兩側邊界必須能讓遞迴子問題變小。若樞紐選得很差，子問題可能只少一個元素，時間複雜度退化；若遞迴堆疊沒有受到控制，極端輸入還可能造成堆疊耗盡。因此，分析平均效能時不能掩蓋最壞情況與輸入分布假設。

Hoare logic 以三元組表示一個局部承諾：前置條件描述程式開始時必須成立的狀態，命令是要分析的操作，後置條件則描述命令完成後保證的狀態。證明規則把賦值、順序執行、條件分支和迴圈拆成可組合的小步驟。對迴圈而言，選出一個在進入、每次迭代和離開時都能維持的不變量，是把直覺轉成可檢查論證的關鍵。

例如排序程序的前置條件可以是輸入範圍有效且元素可比較，後置條件則同時要求輸出有序、並保留原本的多重集合。若只證明每個相鄰元素有序，卻沒有證明元素沒有遺失或重複，規格仍然不完整。Hoare 式推理迫使設計者把這些隱藏承諾寫出來，讓測試、程式碼審查和自動化證明工具有共同的語言。

CSP 把焦點從單一程序的狀態移到程序之間可觀察的事件。每個程序有自己的局部控制流，透過頻道或同步事件與另一個程序交換資料；組合後的系統行為，不只是兩份程式各自正確，還包括事件是否能配對、順序是否符合協定，以及某個程序是否會永遠等待。這種模型把並行溝通從共享記憶體的偶然時序，提升成可以列舉和推理的互動結構。

用 CSP 描述服務時，可以先列出請求、回覆、取消與關閉等事件，再定義哪些事件必須先發生、哪些可並行。若兩個服務各自等待對方先傳送，模型會顯示死結；若一個錯誤路徑沒有關閉頻道，模型也能指出資源無法回收。這些結果不會自動保證網路服務安全，卻能在部署前揭露協定層的矛盾，正是形式模型的實務價值。

原始論文、標準與專案脈絡

牛津人物頁把 Quicksort 的起源放在 1959 年莫斯科的機器翻譯研究：為了更有效率地查字典，Hoare 找到這套排序方法；牛津追悼文則記錄 1961 年公開發表。這個時間線支持一個精確說法：他在特定查找問題中發現並發展了演算法，後來才成為廣泛使用的排序方法，而不是在真空中一次完成所有現代函式庫版本。

回到英國後，Hoare 在 Elliott Brothers 帶領團隊設計 Algol 60 的商用編譯器。牛津資料特別指出，團隊用 Algol 本身作為編譯器的設計語言，雖然實作最後使用十進位機器碼。這個案例把語言規格與工具鏈連在一起：一套語言若不能表達自己的編譯器需求，標準的優雅仍可能停在紙面；反過來，能自我應用也不代表所有執行期限制消失。

1968 年到 Queen’s University Belfast 後，Hoare 把研究問題轉向作業系統為何比編譯器更難，以及程式理論如何幫助並行。牛津人物頁記錄他發表以 assertions 證明程式正確性的論文，並承認這是長期研究，未必能在他的學術生涯中立即工業化。這種時間尺度值得保留，因為形式方法的價值往往先出現在規格、教學和失敗分析，數十年後才由工具和產業吸收。

1977 年加入牛津後，他建立以可證明正確性為驅動力的 Programming Research Group。研究成果包括 Z 規格語言與 CSP 並行模型，並試圖把不同語言、典範和實作技術放進較統一的理論框架。這裡的「統一」不是宣稱所有程式都能用一個公式取代，而是尋找能比較假設、語意和精確度的共同接口，讓研究者知道兩個模型究竟在哪裡相容、在哪裡衝突。

ACM 的 Turing Award 訪談是另一種原始材料，能補足官方履歷沒有呈現的研究動機與方法辯證。閱讀訪談時應把受訪者回憶、同期論文和後來的追述分開標示：回憶有助於理解決策脈絡，論文才能逐步核對定義和證明，追述則要確認是否把後來的工具成果倒灌回早期主張。這種來源分層對任何軟體史研究都適用。

對現代開發工作的影響

今天的設計契約、型別系統、靜態分析器和 model checker，都延續了把前置條件、後置條件與不變量寫明的習慣。團隊不必一開始就為全部程式建立完整形式證明，但可以先為核心 API 寫資料範圍、錯誤條件與資源生命週期，再讓測試與工具檢查最有風險的部分。這比在事故後才猜測函式原本應該保證什麼，更容易建立共同理解。

斷言也有兩種用途。原始研究中的 assertion 可是證明規則的一部分，要求設計者為每個狀態轉移提供可推導的理由；現代產品則常把斷言留在執行期，作為測試和遙測的觀測點。兩者不能混為一談，但可以互補：形式條件幫助選擇關鍵觀測點，執行期失敗則回饋規格是否漏掉真實環境的例外。

並行服務的工程設計可以借用 CSP 的事件表。先描述每個角色能做什麼，再列出握手、取消、逾時、重試和關閉的順序，最後檢查兩個角色是否可能互相等待。對訊息佇列、actor 或 async/await 系統，這種事件視角能補足單元測試看不到的交錯路徑；它也讓 code review 可以討論協定，而不是只爭論鎖放在哪一行。

Quicksort 的歷史則提醒函式庫作者不要只宣傳平均速度。現代實作會選擇不同的樞紐策略、限制遞迴深度、處理重複鍵，甚至在壞情況轉用其他排序法。每個選擇都應在文件中說明穩定性、最壞時間、記憶體和比較器要求，讓使用者依資料特性作決定。演算法名稱提供入口，並不取代對輸入、資源和失敗模式的契約。

在教育上，可以把同一個小程式分三次閱讀：先用測試觀察輸入與輸出，再寫 Hoare 三元組和迴圈不變量，最後把兩個版本放進 CSP 模型討論並行呼叫。學生會看見測試、證明與模型各自覆蓋不同的錯誤類型；教師也能指出一個通過測試的程式仍可能規格不足，一個形式證明則可能證明了錯的規格。

爭議、限制與常見誤讀

最常見的誤讀是說 Hoare logic 能證明任何程式「完全正確」。證明只對給定的前置條件、程式語意和後置條件成立；若規格忘記權限、時間、浮點誤差或外部服務失敗，形式推理也會忠實地證明一個不完整的世界。實務上需要先審查規格，再檢查模型是否涵蓋環境，最後才談證明工具的覆蓋率。

第二個限制出現在 Quicksort。它的平均效率很有吸引力，但排序資料若接近已排序、樞紐策略固定，或比較器行為不一致，最壞情況便可能出現。原地分割也會讓除錯和穩定排序變得更複雜。把 Quicksort 叫作「最快排序」而不列出輸入假設，是把一個有條件的演算法結論誇大成普遍承諾。

CSP 同樣不是實際並行硬體的完整鏡像。模型通常抽象掉快取一致性、排程延遲、網路分割、時鐘漂移與故障恢復；一個無死結的事件系統，仍可能在部署後因逾時或資源耗盡而失效。正確的用法是把 CSP 當成協定層的檢查，再與負載測試、故障注入、監控和部署策略接起來，而不是以模型結果取代所有工程證據。

「Hoare 發明了程式驗證」也需要縮小範圍。形式邏輯、程式語意、抽象解釋和自動定理證明都有更長的共同歷史；Hoare 的獨特貢獻在於提供可組合的程式斷言規則，並把它帶進語言方法與並行研究。清楚標示前人基礎、同期合作和後續發展，並不會削弱他的地位，反而使技術因果更可信。

牛津追悼資料記載 Hoare 1999 年從牛津退休後加入 Microsoft Research，也記錄他長期關注 legacy code。這不代表學術證明已經普遍解決舊系統維護；遺留程式通常缺少規格、測試和可重現環境，補上斷言仍需判斷哪些行為是契約、哪些只是歷史偶然。把研究方法移植到產品時，必須承認資料與人力限制，逐步選擇高風險邊界。

本文的原創技術圖只把 Quicksort、前後置條件、程式證明與 CSP 的關係整理成閱讀路線，不是 Tony Hoare 的肖像、手稿或 ACM 原件。若要確認年份、獎項、出版物或訪談內容，應回到 Oxford 人物頁、Oxford 追悼文章與 ACM Turing transcript 的原文。圖像的功能是幫助讀者定位概念，不能取代原始來源，也不應把推論畫成已證明的歷史事實。

一個適合團隊的最小實驗，是選一個含重複值的排序函式，先測試輸出順序，再寫出保留多重集合的不變量，最後把兩個並行呼叫者的請求與回覆畫成事件序列。若測試通過但不變量無法成立，表示實作或規格仍有缺口；若單執行緒證明成立而事件模型出現死結，則問題不在排序，而在整合協定。這種逐層比較正是 Hoare 方法對現代開發最可操作的遺產。

Tony Hoare 的重要貢獻：把程式行為變成可推理的工程對象

C. A. R. Hoare 常以 Tony Hoare 的名字被記住，但他的歷史位置不只是一個排序演算法，而是把演算法、程式邏輯、語言規格與並行溝通接成一條方法論。Oxford 官方人物頁與追悼資料適合核對他的研究位置和學術脈絡，ACM Turing transcript 則讓讀者回到他如何描述程式語言與形式方法。人物頁、回憶文章和技術文本用途不同，不能用一張照片或一個獎項代替原始論證。

Hoare 的第一項貢獻，是讓「程式正確」不再只靠執行幾個例子來判斷。Quicksort 提供演算法層的問題：分割後資料是否仍保留、遞迴是否終止、重複值如何處理、最壞情況的成本如何分析。Hoare logic 再把這些問題寫成前置條件、程式與後置條件之間的推理。CSP 則把視線推向多個程序的互動：哪些事件可以發生、何時必須同步、如何描述死結與通訊協定。

Quicksort：排序演算法也是規格問題

Quicksort 常被簡化成「選 pivot、分左右、遞迴」，但真正的工程問題在於每一步都要保留可推理的性質。分割完成後，左側和右側的元素關係要符合規格；重複值不能因比較條件不慎而造成無限迴圈；遞迴範圍要縮小，才能證明終止；原地交換則要說明哪些元素被保留、哪些位置正在改變。

這個例子顯示演算法的正確性不是測幾組輸入就結束。測試可以發現反例，卻不能單獨證明所有排列都會被正確處理。Hoare 的研究傳統把資料結構、迴圈不變量、終止度量與後置條件連在一起，讓實作者能先寫出「應該一直成立什麼」，再選擇交換和遞迴步驟。效能分析也必須保留：平均行為、最壞分割、堆疊深度和記憶體成本並不會因證明正確而自動消失。

Hoare Logic：把程式與證明放進同一個括號

Hoare logic 常用三元組表示：前置條件、程式、後置條件。它不是替程式貼上一個「已驗證」標籤，而是提供規則，讓人可以逐步說明一段指令如何改變狀態。對賦值、順序、條件與迴圈，各有不同推理方式；迴圈尤其需要不變量和終止條件，否則證明可能只描述一個理想狀態而沒有說明程式會不會停。

這種方法要求規格先寫對。若前置條件漏掉輸入範圍、資源限制、例外或並行干擾，證明即使形式上成立，也可能只代表一個過度簡化的模型。因此形式驗證不是測試的替代品，而是讓測試案例、規格、實作與反例更容易彼此對照。對安全或高成本系統而言，這種可追蹤性比一句「程式很可靠」更有用。

CSP：把並行系統從執行緒清單提升到事件關係

Communicating Sequential Processes（CSP）把程序之間的溝通當作一等問題。並行系統不是多開幾條執行緒就完成，還要說明哪些事件可以同步、哪些通道必須依序使用、兩個程序等待彼此時會發生什麼，以及觀察者能看到哪些行為。用事件與程序描述互動，能讓設計者在實作前先檢查協定和死結。

CSP 的力量也來自它的限制：模型要選擇狀態、事件和抽象邊界，選錯就可能證明一個與真實系統不相干的東西。網路延遲、排程器、故障、資源耗盡和第三方服務若沒有納入假設，形式模型的結論便不能直接外推。Hoare 的遺產不是「所有並行程式都能輕易證明」，而是要求團隊明確說出互動規則和未知範圍。

從學術方法到軟體團隊工作

Hoare 的方法可轉成一套團隊檢查順序：先為功能寫可觀察規格，再列出資料不變量與錯誤條件，接著用測試找反例，用形式推理檢查關鍵路徑，最後把證明假設和實際部署環境對照。這樣做不代表每段程式都要完整形式化；更實際的做法是把高風險、難以回溯或並行互動密集的部分優先納入。

這條路線也補足只談測試的盲點。測試告訴團隊某些輸入發生了什麼，規格告訴團隊哪些行為應該被允許，證明則在假設成立時說明一類行為為何符合規格。三者互相制約，任何一項都不能被神化。規格錯誤、模型過大、工具限制、證明維護成本和團隊理解落差，都必須在工程計畫裡留下位置。

人物、團隊與形式化的歷史界線

把 Hoare 描述成單人發明者，會遮蔽 Oxford Programming Research Group、學生、共同作者、產業合作和後續工具社群。Quicksort、Hoare logic、CSP 和語言規格各自有不同的研究與傳播歷史；他是關鍵提出者和領導者，但後續可用性來自多人推進、批評與實作。

同樣不能把 1980 年 ACM Turing Award 當成所有技術主張的證明。獎項說明公共歷史地位，技術論文才支持演算法、邏輯和並行模型的具體內容。Oxford 官方肖像只用於人物辨識與來源 attribution，不是排序流程、形式證明或 CSP 圖表的證據。

比較閱讀與今日可用的研究方法

可以把 Hoare 與John Backus 把高階語言與 BNF 接到可翻譯工具鏈並讀：一邊處理表達與編譯，一邊處理規格與正確性，兩者都要求抽象能被實作檢查。也可與Niklaus Wirth 以簡潔語言、編譯器和教育建立心智模型比較，觀察語言小型化與形式化推理如何互相補強，也如何產生新的成本。

資料來源與編輯界線

本文以Oxford Tony Hoare 官方人物頁核對他的學術位置與研究入口，以Oxford 官方追悼資料補充研究團隊與公開脈絡，以ACM Turing transcript回到他對程式語言與形式方法的原始談話，並以Oxford 官方原始圖檔核對文中照片。照片只用於人物辨識與 attribution；文章對現代軟體團隊的延伸是編輯分析，不是 Oxford 或 ACM 對今日產品的背書。

Tony Hoare 的重要貢獻可以濃縮成三件事：用 Quicksort 展示演算法必須保留可推理的不變量；用 Hoare logic 建立程式與規格之間的推理規則；用 CSP 把並行程序的事件、同步與死結變成可討論的模型。他留下的不是「形式化就不會出錯」的口號，而是一種要求團隊把假設、規格、反例、工具限制與部署邊界說清楚的工作方式。