給定兩個變數 r 與 dd. 假設 0 ≤ r < dd，請問如何論證：經過以下兩步驟後，0 ≤ r < dd 仍成立？
dd := dd / 2;
if dd ≤ r then r := r - dd這個例子來自 Dahl, Dijkstra & Hoare 1972 年的書 Structured Programming. 書名引起我的注意：「結構化程式設計」在 70, 80 年代曾被學界、業界視為軟體危機的解方、所有人寫程式該遵守的圭臬。但每個陣營對它是什麼都各有一套解釋，而困惑的大眾能理解的只剩下「不能用 goto」。數十年過去，structured programming 卻以一種不知能否算功成而退的方式被遺忘：現在的學生們自然地把程式寫成塊狀的結構，許多人甚至已經不知有 goto 這個指令。但他們沒聽過 structured programming, 對於 Dijkstra 等人當年提倡的程式推論仍一樣地陌生。
我想知道這套概念的創始者們怎麼談它，因此好奇地想讀這本書。
這個例子出現在書中最初的幾節。我覺得很有意思，因為若不用符號、用「直覺」（所謂直覺很有可能是用語意），並不很容易看出為何前述的 pre/post conditions 會被滿足。Dijkstra 在書中大致是用這樣的文字敘述推論的（以下為簡略過的翻譯）：
「假設 0 ≤ r < dd 原已被滿足。經過第一個指令，0 ≤ r < 2×dd 成立。接下來我們分出兩個情況：如果 dd ≤ r，總合起來我們有了 dd ≤ r < 2×dd。這時 if 的第一個分支會被執行，把 r 減去 dd, 所以我們有 0 ≤ r < dd. 如果 dd ≤ r 不成立，也就是說 r < dd，由於 r 的值沒變，我們仍有 0 ≤ r < dd。」
我們可觀察到幾點：首先，Dijkstra 的推論是可在符號層次（而不是語意）上理解的。其次，「證明的結構跟著程式的結構」的想法已經在漸漸成形中，但還沒有符號化。第三，這邊用的是由前往後的推論 --- 後來會發展成由後往前。此時，ALGOL 60 已經制定完成 (Backus et al. 1960)，Hoare logic 已經誕生 (Hoare 1969)，但 Dijkstra 的 Guarded Command Language 及其程式證明/推導方法(Dijkstra 1975)還要等到三年後才會發表。
依循程式結構的形式化證明
如果用 1975 年之後的技巧，我會把程式改寫成 guarded command language:
dd := dd / 2
if dd ≤ r -> r := r - dd
| r < dd -> skip
fi如果只以執行為目的， r < dd 的那個 case 好像很累贅。但我發現如果是為了推論，把 r < dd 寫出來是有幫助的 --- 讓這個 case「看得到」了，才有東西可以操作，我的思考也因能依賴符號而比較輕鬆。
回顧：為 if 標斷言的方式是：
{ P }
if B₀ -> { P ∧ B₀ } S₀ { Q }
| B₁ -> { P ∧ B₁ } S₁ { Q }
fi
{ Q }把前述程式標上斷言，得到：
{ 0 ≤ r < dd }
dd := dd / 2
{ 0 ≤ r < 2 × dd }
if dd ≤ r -> { 0 ≤ r < 2 × dd ∧ (dd ≤ r) } r := r - dd
| r < dd -> { 0 ≤ r < 2 × dd ∧ (r < dd) } skip
fi
{ 0 ≤ r < dd }其中，{ 0 ≤ r < dd } dd := dd / 2 { 0 ≤ r < 2 × dd } 這個 Hoare triple 對應到 Dijkstra 用口語解釋的第一句話：「0 ≤ r < dd 原已被滿足。經過第一個指令，0 ≤ r < 2×dd 成立」。其證明很簡單，將後置條件的 dd 代換成 dd/2 即可。
接下來我們分別證明兩個分支。我們可看到兩個分支的初始條件恰好和 Dijkstra 以口語敘述的相同。第一個分支：
(0 ≤ r < dd) [ r 代換成 (r - dd)]
= 0 ≤ r - dd < dd
= (0 ≤ r - dd) ∧ (r - dd < dd)
= (dd ≤ r) ∧ (r < 2 × dd)
⇐ 0 ≤ r < 2 × dd ∧ (dd ≤ r)
至於另一個分支，顯然 0 ≤ r < 2 × dd ∧ (r < dd) ⇒ 0 ≤ r < dd .
以上大部分的推演都能以有系統、形式化、機械化、「用符號思考」的方式進行 --- 可以看出 Dijkstra 的方法發展到此，已比 Structured Programming 成書之時更加成熟了。
另一方面，證明的進行更明顯地依循著程式的結構。「讓程式能依據其結構被理解、被證明」，便是我心目中的「結構化編程」。而在那個時代，他們的挑戰便是設計語言、符號，使得這種編程與推論成為可能。
除數與餘數
上述程式其實是另一個程式的部分。以下的演算法在 O(log A) 的時間內計算 A 除以 D 的除數與餘數，僅使用加法、減法、和位元位移（乘以二或除以二）。Dijkstra 將這個演算法歸功於 de Bruijn.
var r, dd, q : int;
dd := D;
do dd ≤ A -> dd := 2 × dd od;
r, q := A, 0;
do dd ≠ D ->
dd, q := dd/2, 2 × q;
if dd ≤ r -> r, q := r - dd, q + 1
| r < dd -> skip
fi
od
{ A = q × D + r ∧ 0 ≤ r < D }
Dijkstra 並沒有明確給出該程式的初始條件：其實我們會需要 0 ≤ A ∧ 0 < D. 第二個迴圈是程式的核心，使用三個性質作為 invariant：A = q × dd + r, 0 ≤ r < dd, 以及 dd 是 D 乘以 2 的某個乘冪。依據這樣的了解，我們為程式加上如下的斷言：
{ 0 ≤ A ∧ 0 < D }
var r, dd, q : int;
dd := D
{ (∃ k : 0 < k : dd = D × 2^k) ∧ 0 < dd , bnd: A - dd }
; do dd ≤ A -> dd := 2 × dd od
{ (∃ k : 0 < k : dd = D × 2^k) }
; r, q := A, 0
{ A = q × dd + r ∧ 0 ≤ r < dd ∧ (∃ k : 0 < k : dd = D × 2^k),
bnd : dd }
; do dd ≠ D ->
dd, q := dd/2, 2 × q
{ A = q × dd + r ∧ 0 ≤ r < 2 × dd }
; if dd ≤ r -> r, q := r - dd, q + 1
| r < dd -> skip
fi
od
{ A = q × D + r ∧ 0 ≤ r < D }
如此一來，它的證明便不難了。要試試看嗎？
參考資料
- O. J. Dahl, E. W. Dijkstra, and C. A. R. Hoare. Structured Programming. Academic Press, 1972.
- E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 18(8), pp. 453-457, 1975.
- C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM 12(10), pp 576-583. October 1969.
- Peter Naur (Ed.). Report on the algorithmic language ALGOL 60. Communications of the ACM 3, pp. 299-314, May 1960.