1969 年 Hoare 邏輯：給程式戴上斷言手銬#
案件編號：No.1969-A — 報案人：會出錯的程式。偵探：Floyd、Hoare、Dijkstra。兇器：三元組。
案發現場#
1967 年，Robert Floyd 在紐約的 IFIP 會議上拋出一張流程圖，上面貼滿了斷言。聽眾多半沒聽懂：程式不是跑起來看結果就行了嗎？為何要在每個箭頭上寫數學？
背景是軟體危機初現。作業系統越來越大，Algol 60 編譯器 bug 頻傳，NASA 與銀行都開始怕程式半夜叛變。 圖靈機與程式 只管可計算，不管正確； 自動證明 只證數學定理，不證程式； 歸結 再強，也沒說如何談「賦值」與「迴圈」。
Floyd 的洞見是：把程式的每個切點貼上斷言 \(P\) 、 \(Q\) ，程式正確即「若進入時 \(P\) 成立且程式終止，則離開時 \(Q\) 成立」。兩年後 C. A. R. Hoare 在 An Axiomatic Basis for Computer Programming 中把流程圖改成結構化語言，發明三元組，Dijkstra 再補上最弱前條件。一樁懸案，三位偵探接力。
偵查過程#
Hoare 邏輯的案卷格式只有一種：
讀作：若前條件 \(P\) 成立且程式 \(C\) 終止，則後條件 \(Q\) 成立。這是部分正確性，不保證終止。若要保證終止，需另加變體函數，此為全正確性。
線索一：Floyd 斷言法#
Floyd 把流程圖每條邊標上斷言，驗證條件即「邊的斷言經語句保持」。例如邊上為 \(x = a\) ，經 \(x := x + 1\) 後應為 \(x = a + 1\) 。這是 Hoare 賦值公理的雛形，只是當時還依附於圖形。
Hoare 的改良是拋開流程圖，用 while 語言： \(C ::= skip \mid x := E \mid C_1 ; C_2 \mid if \, B \, then \, C_1 \, else \, C_2 \mid while \, B \, do \, C\) 。結構化之後，推理可按語法歸納，這正是 Gentzen 結構證明 精神在程式界的投射。
線索二：Hoare 規則表#
| 規則 | 形式 | 偵探解讀 |
|---|---|---|
| 賦值 | \(\{ P[x := E] \} \, x := E \, \{ P \}\) | 倒帶推理：先想結果 \(P\) 對 \(x\) 代入 \(E\) 即得前提 |
| 序列 | 由 \(\{ P \} \, C_1 \, \{ R \}\) 與 \(\{ R \} \, C_2 \, \{ Q \}\) 得 \(\{ P \} \, C_1 ; C_2 \, \{ Q \}\) | 兩段筆錄串連，中間證詞 \(R\) 吻合 |
| 條件 | 由 \(\{ P \land B \} \, C_1 \, \{ Q \}\) 與 \(\{ P \land \lnot B \} \, C_2 \, \{ Q \}\) 得 \(\{ P \} \, if \, B \, then \, C_1 \, else \, C_2 \, \{ Q \}\) | 分案偵辦，兩路皆抵 \(Q\) |
| 迴圈 | 由 \(\{ I \land B \} \, C \, \{ I \}\) 得 \(\{ I \} \, while \, B \, do \, C \, \{ I \land \lnot B \}\) ，其中 \(I\) 為不變式 | 守住不變式 \(I\) ，出圈時 \(B\) 已死 |
| 推論 | 若 \(P \Rightarrow P'\) 、 \(\{ P' \} \, C \, \{ Q' \}\) 、 \(Q' \Rightarrow Q\) 則 \(\{ P \} \, C \, \{ Q \}\) | 補強前提、放弱結論，前後加固 |
其中 \(P[x := E]\) 表將 \(P\) 中自由 \(x\) 以 \(E\) 代入。例如欲證 \(\{ True \} \, x := x + 1 \, \{ x > 0 \}\) 不成立，但 \(\{ x \ge 0 \} \, x := x + 1 \, \{ x > 0 \}\) 成立，因 \((x > 0)[x := x + 1]\) 即 \(x + 1 > 0\) 等價於 \(x \ge 0\) 在整數域成立。
線索三：迴圈不變式實戰#
經典：計算 \(s = \sum_{i=1}^{n} i\) 的程式：
s := 0; k := 1;
while k <= n do { s := s + k; k := k + 1 }
取不變式 \(I\) 為 \(s = sum(k-1) \land 1 \le k \le n+1\) ，其中 \(sum(m)\) 表前 \(m\) 項和。證明 \(I \land k \le n\) 經循環體保持 \(I\) ，出圈時 \(k = n+1\) 故 \(s = sum(n)\) 。後條件 \(Q\) 為 \(s = n(n+1)/2\) ，得證。不變式即迴圈的「不在場證明」：無論繞幾圈，它都成立。
線索四：Dijkstra 最弱前條件#
Dijkstra 把三元組函數化：定義 \(wp(C, Q)\) 為保證終止且達 \(Q\) 的最弱前提，則 \(\{ P \} \, C \, \{ Q \}\) 全正確當且僅當 \(P \Rightarrow wp(C, Q)\) 。例如：
- \(wp(skip, Q) = Q\)
- \(wp(x := E, Q) = Q[x := E]\)
- \(wp(C_1 ; C_2, Q) = wp(C_1, wp(C_2, Q))\)
- \(wp(if \, B \, then \, C_1 \, else \, C_2, Q) = (B \Rightarrow wp(C_1, Q)) \land (\lnot B \Rightarrow wp(C_2, Q))\)
\(while\) 的 \(wp\) 需不動點構造，實務上仍靠不變式加變體。這套演算讓驗證可機械倒推，後世 Dafny、Why3 皆據此實作。
結案報告#
Hoare 邏輯把「程式正確」變成可證明的數學對象：
- 從流程圖到公理系：Floyd 貼斷言，Hoare 給規則，Dijkstra 給演算，三步把程式驗證變成結構歸納證明。
- 不變式典範：迴圈不變式成為此後半世紀驗證的核心，迴圈有多難，不變式就有多難找——這仍是今日自動驗證的瓶頸。
- 工業血脈：Boyer Moore 證明器、ACL2、PCC、CompCert、seL4 的程式正確性證明，骨子裡都是 Hoare 三元組加 \(wp\) 。分離邏輯更是其處理指標的直系續集。
局限是：原始 Hoare 邏輯不處理別名、指標、併發，完備性需表達力足夠的斷言語言（Cook 1978 相對完備性）。但 1969 年這一案，偵探終於給程式戴上了手銬：跑得動還不夠，要能證明跑得對。
證據與工具#
證明樹示例：欲證 \(\{ x = a \} \, x := x + 1 ; x := x * 2 \, \{ x = 2a + 2 \}\) 。倒推：第二句需前提 \(x * 2 = 2a + 2\) 即 \(x = a + 1\) ，第一句由 \(x = a\) 經 \(x := x + 1\) 恰得 \(x = a + 1\) ，以序列規則串連即得證。
陣列賦值補充：若涉及 \(a[i] := E\) ，需以 \(a\{i \leftarrow E\}\) 表示更新後的陣列函數，避免直接代入 \(a\) 造成混淆。這是後來分離邏輯處理堆的起點：把記憶體視為可分離的資源，每塊堆各有斷言。
終止性備註：部分正確加變體函數 \(V\) 即得全正確。若能找到 \(V : State \to Nat\) 使每次迴圈 \(V\) 嚴格遞減，則迴圈必終止。例如上例取 \(V = n - k + 1\) ，初值有限且每圈減一，終止得證。這正是 Floyd 的良基關係思想。
習題：給定 \(\{ P \} \, while \, x > 0 \, do \, x := x - 1 \, \{ x = 0 \}\) ，找不變式 \(I\) 與變體 \(V\) 。提示：取 \(I\) 為 \(x \ge 0\) ， \(V\) 為 \(x\) 本身，每圈減一且有下界，故終止且正確。
延伸閱讀：Hoare 1969 原文、Floyd 1967 Assigning Meanings to Programs 、Dijkstra 1975 Guarded Commands 。數學證明如何變成程式？請見姊妹案 Howard 公式即型別 ；機器如何檢查這種證明？請回顧 Automath 。