1978 Robert Floyd —— 把演算法從手藝變成數學#

「演算法的正確性以前靠『看起來對』，Floyd 主張：證明它。而且他在 1960 年代就預言了『程式驗證』這門學科。」

案件檔案#

1962 年前後，Knuth（1974 案）正在建立演算法分析，但正確性 仍靠測試。Floyd 的謎題：能否像幾何定理一樣證明程式正確？

《Assigning Meanings to Programs》：在程式切點標註斷言，以邏輯推演證明：

1. 選切點，標斷言 P_i
2. 證明每條路徑使斷言成立
3. 全部成立 ⟹ 程式正確

此思想被 Hoare 發展為 Hoare 邏輯三元組 {P} C {Q}（1980 案）

迴圈不變式成為演算法設計的核心紀律：寫迴圈前先寫不變式，程式自然正確。Dijkstra（1972 案）的構造性方法論與此互為表裡。

三重迴圈、O(n³)，優雅到近乎魔術：

for k, i, j:
  d[i][j] = min(d[i][j], d[i][k] + d[k][j])
不變式：第 k 輪後 d[i][j] = 只經過中繼點 ∈ {1..k} 的最短距離

以允許的中繼點集合為歸納參數——不變式思維的完美示範。

將完全二元樹壓進陣列（i 的子女在 2i、2i+1），建堆 O(n)、每次取最大並修復 O(log n)，總 O(n log n) 最壞保證—— 與快速排序（平均快但最壞 O(n²)）形成理論上的對照組。

提出 nondeterministic algorithms 概念：先「猜」再「驗」。此思想成為 NP 完全理論（Cook 1982 案、Karp 1985 案）的概念先聲。

Floyd 的元貢獻是方法論的自覺：演算法不是靈感，而是「不變式 → 構造 → 證明」的機械化流程。他與 Hoare、Knuth、 Dijkstra 四人構成 1960s「程式驗證學派」的軸心。