1980 C.A.R. Hoare —— 公理讓程式學會證明自己#

「他寫出 quicksort 時只有 26 歲；他定義的 {P} C {Q} 成為 半世紀來所有程式驗證的起點。」

案件檔案#

前因#

Floyd（1978 案）已提出斷言法，但停留在「方法」。待解之謎： 能否把程式語言的每個結構配上公理，使驗證成為形式系統？

線索與推理#

案一：quicksort（1961，莫斯科交流時發明）#

1. 取基準 pivot（首元素）
2. 劃分：小於 pivot 的放左、大者放右（原地交換）
3. 遞迴兩側

平均 O(n log n)、空間 O(log n)、最壞 O(n²)（已排序輸入！）
期望比較次數精確值：2n ln n ≈ 1.39 n log₂ n

實踐最強的排序演算法：快 + 原地 + 快取友善。因「原地劃分」 的巧思，成為程式設計史的技藝典範。

案二：Hoare 邏輯（1969）#

把 Floyd 的斷言法公理化：

賦值公理：  {P[x/E]} x := E {P}
組合律：    {P} A {R}, {R} B {Q} ⟹ {P} A;B {Q}
條件律：    {P∧B} A {Q}, {P∧¬B} C {Q} ⟹ {P} if B then A else C {Q}
推論律：    P→P', {P'}A{Q'} , Q'→Q ⟹ {P} A {Q}

partial correctness（部分正確性）：此系統不含終止性。 終止需另證（rank function / 變異量）。整個學科自此有了 演繹基礎——證明助手（Coq、Dafny）至今沿用此框架。

案三：CSP（1978）#

併發程式的正確性更難。Hoare 選擇通訊而非共享記憶體：

P :: do  producer?x → consumer!x  od
通訊 = 同步的原語；死結可被數學分析

CSP 的操作語義與 trace 理論催生 occam 語言，並直接啟發 Go 語言的 channel（「Don't communicate by sharing memory; share memory by communicating」）。

理論評析#

Hoare 的三案一體：quicksort 是手工藝巔峰，Hoare 邏輯是 科學化，CSP 是擴張疆域（從順序到併發）。他自省的名言 《Null References: The Billion Dollar Mistake》——1965 年在 ALGOL W 引入 null 參照，後來的除錯成本以十億美元計。 偵探的教訓：設計者最後悔的，往往是最不起眼的那個方便。

後果#

• 軟體驗證工業化：SPARK Ada、seL4 微核心（形式化驗證的 OS）、 CompCert 編譯器。
• null 問題在 Rust（Option 型別）、Kotlin（? 型別）被以 型別系統治療——遲到半世紀的修正。

關聯案件#

→ 1978-Robert-Floyd與演算法分析方法論、1996-Amir-Pnueli與時態邏輯、2007-Clarke-Emerson-Sifakis與模型檢查