除二、相減,大小不變?來自《結構化編程》中的一個小例子

給定兩個變數 rdd. 假設 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, 以及 ddD 乘以 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 }

如此一來,它的證明便不難了。要試試看嗎?

參考資料

Leave a Comment

發佈留言必須填寫的電子郵件地址不會公開。