2019-20 年的程式語言課中，我出了這麼一個題目給同學：給定一個含數字的陣列 A [0.. N), 0 ≤ N. 其中任一個連續區段 [p..q) 的「信用」是其中正數的個數減去負數的個數：
credit p q =〈# i : p ≤ i < q : A i > 0〉-
〈# i : p ≤ i < q : A i < 0〉
此處以 # 開頭的 quantifier 表示個數，其定義是
〈# i : R i : S i〉=〈Σ i : R i : if S i then 1 else 0)〉請推導出一個程式，計算該陣列中「信用最高的區段」的信用，也就是
〈↑ p q : 0 ≤ p ≤ q ≤ N : credit p q〉這個問題出自 Kaldewaij (1990)。這裏想談談改考卷時常看到的一些錯誤。
信用
為了讓後面的作答順利些，我先給了一個（自己覺得是送分題的）送分題：假設 p ≤ n, 請用 credit p n 表達出 credit p (n+1)。答案是：
credit p (n+1) = credit p n + 1, if A n > 0
| credit p n , if A n = 0
| credit p n - 1, if A n < 0
常見的錯誤之一是把 A n 誤植為 A (n+1), 而這可能是因為仍不習慣「左閉右開」的區段表示法，忽略了 credit p q 之中並不包括 A q.
如果要給個推導，可以論證如下（將 if P then 1 else 0 簡寫為 # P)：
credit p (n+1)
=〈# i : p ≤ i < n+1 : A i > 0〉-〈# i : p ≤ i < n+1 : A i < 0〉
= { 因為 p ≤ n, split off i = n+1 }
〈# i : p ≤ i < n : A i > 0〉+ #(A n > 0) -
〈# i : p ≤ i < n : A i < 0〉- #(A n < 0)
= credit p n + #(A n > 0) - #(A n < 0)
接下來分別討論 A n > 0, A n = 0, A n < 0 的狀況便可以得到上面的定義。接下來的計算中我們也可能直接用 # 函數，以節省一些空間。
Strengthening the Invariant
回來試著解問題。依據課程的理路，大家應該可猜到我們會把常數 N 代換成變數 n, 用一個迴圈把 n 遞增，並試圖更新 r:
....
{ r = 〈↑ p q : 0 ≤ p ≤ q ≤ n : credit p q〉∧ ... }
do n ≠ N -> r := ....;
n := n + 1
od
{ r = 〈↑ p q : 0 ≤ p ≤ q ≤ N : credit p q〉 }
為讓式子簡潔些，我們定義
msc n = 〈↑ p q : 0 ≤ p ≤ q ≤ n : credit p q〉其中 msc 為 maximum segment credit 的縮寫。因此，程式的初始與後置條件分別為 r = msc n （以及一些其他條件），和 r = msc N.
接下來的工作便是找出如何更新 r. 大家也可能預期光靠 r 自己無法有效率地更新，我們會需要增強 invariant, 多使用幾個變數。這些變數該存什麼值？可從演算的過程中發現。以下假設 0 ≤ n:
(msc n) [n+1/n]
=〈↑ p q : 0 ≤ p ≤ q ≤ n : credit p q 〉[n+1/n]
=〈↑ p q : 0 ≤ p ≤ q ≤ n+1 : credit p q 〉
= { split off q = n+1 }
〈↑ p q : 0 ≤ p ≤ q ≤ n : credit p q 〉 ↑
〈↑ p q : 0 ≤ p ≤ n+1 : credit p (n+1) 〉
= msc n ↑〈↑ p q : 0 ≤ p ≤ n+1 : credit p (n+1) 〉
由此啟發，我們也許可以新造一個變數 s，存放〈↑ p q : 0 ≤ p ≤ n : credit p n 〉 --- 目前為止提供最大信用的「後段」（suffix 或 tail, 即右界已經固定為 n 的區段）的信用。我們定義
mtc n = 〈↑ p q : 0 ≤ p ≤ n : credit p n 〉並加上一個 invariant: s = mtc n. 剛剛的推導證明了當 0 ≤ n 時， msc (n+1) = msc n ↑ mtc (n+1).
這階段有幾點可討論：首先，注意第二步之中被分出來的是 n+1 而不是 n, 因為此處 q 與 n+1 的關係是 q ≤ n+1 --- q 最大的值可以是 n+1! 其次，如果我們這樣選 s, 我們得先把 s 更新，才能用新的 s 更新 r. 下述的平行賦值是不對的！
s, r := ... , r ↑ s
因為此處 r 會用到 s 的舊值！s 與r 的更新應該分兩步：s := ... ; r := r ↑ s. 如果我們把前後條件標上，會是如此 --- 注意 n 與 n+1 的變化：
{ r = msc n ∧ s = mtc n }
s := ...
{ r = msc n ∧ s = mtc (n+1) }
; r := r ↑ s
{ r = msc (n+1) ∧ s = mtc (n+1) 〉}
接下來我們該看看怎麼更新s.
更新最大後段信用
關於 s 的更新，許多人這麼推論：
〈↑ p q : 0 ≤ p ≤ n : credit p n 〉[n+1 / n]
=〈↑ p q : 0 ≤ p ≤ n+1 : credit p (n+1) 〉
= { 依照前述計算展開 credit p (n+1) }
〈↑ p q : 0 ≤ p ≤ n+1 : credit p n + #(A n > 0) - #(A n < 0)〉
= { 提出常數項 }
〈↑ p q : 0 ≤ p ≤ n+1 : credit p n 〉+ #(A n > 0) - #(A n < 0)
= { 分三個狀況討論 }
〈↑ p q : 0 ≤ p ≤ n+1 : credit p n 〉+ 1, if A n > 0;
〈↑ p q : 0 ≤ p ≤ n+1 : credit p n 〉 , if A n = 0;
〈↑ p q : 0 ≤ p ≤ n+1 : credit p n 〉- 1, if A n < 0
因此 s 與 r 似乎可以這麼更新：
if A n > 0 -> s := s + 1; r = r ↑ s
| A n = 0 -> skip
| A n < 0 -> s := s - 1; r = r ↑ s
fi
但這麼做是不對的！
回顧 credit p (n+1) 的定義：
credit p (n+1) =
〈# i : p ≤ i < n+1 : A i > 0〉-〈# i : p ≤ i < n+1 : A i < 0〉我們之前推導過：credit p (n+1) = credit p n + #(A n > 0) - #(A n < 0), 但過程中用了一個 splitting-off 規則把 i = n 取出來，並有個附加條件 --- 這只在 p ≤ n 時成立。否則這個 i 可能不存在，沒東西可分出來！
使用 splitting-off 規則時一定得先檢查：要確定 range 內總是有東西可分得出來！
而回顧上面的演算，其中對 p 的限制比較寬鬆 --- 我們只得知 0 ≤ p ≤ n+1. 此時 p 還有可能等於 n+1, 這時 credit (n+1) (n+1) 的 range 中是沒有東西可分出來的！因此現在還不能把 credit p (n+1) 拆開。
（此外，上述演算的另一個錯誤是：最後的 quantification 內的 range 是 0 ≤ p ≤ n+1, 因此無法收回成為 mtc。）
我原本以為讓大家先把 credit p (n+1) 算好，能讓後面的演算簡單一些。也許這反倒誤導了大家，使大家一看到 credit p (n+1) 就想拆開。雖然原題中也有提到 p ≤ n 的條件，但許多學生沒注意到。
（回顧起來，我們之前推論 r 的更新時，偷偷放了一句「以下假設 0 ≤ n」，也是為了同樣的原因 --- 確定有東西可分出。這些附加條件都得放在 loop invariant 之中。）
所以，正確的推導是 -- 假設0 ≤ n：
〈↑ p q : 0 ≤ p ≤ n : credit p n 〉[n+1 / n]
=〈↑ p q : 0 ≤ p ≤ n+1 : credit p (n+1) 〉
= { 因 0 ≤ n, split off p = n+1 }
〈↑ p q : 0 ≤ p ≤ n : credit p (n+1) 〉↑ credit (n+1) (n+1)
= { credit (n+1) (n+1) = 0 }
〈↑ p q : 0 ≤ p ≤ n : credit p (n+1) 〉↑ 0
= { 現在可以展開 credit p (n+1) 了！ }
〈↑ p q : 0 ≤ p ≤ n : credit p n + #(A n > 0) - #(A n < 0)〉↑ 0
= { 提出常數項 }
(〈↑ p q : 0 ≤ p ≤ n : credit p n 〉+
#(A n > 0) - #(A n < 0)) ↑ 0
= { mtc 之定義 }
(mtc n + #(A n > 0) - #(A n < 0)) ↑ 0
= { 分三個狀況討論 }
(mtc n + 1) ↑ 0, if A n > 0;
mtc n ↑ 0 , if A n = 0;
(mtc n - 1) ↑ 0, if A n < 0
我們不能立刻把 credit p (n+1) 拆開，而必須先 split off 外層的 p = n+1. 這會在式子的最外面做出一個 (↑ 0) , 其中 0 是空區段的信用 --- 這是這類問題的常見特徵！這之後，內側的 range 變成 0 ≤ p ≤ n, 然後我們才可以安全地展開 credit p (n+1)！
經由上述推導，我們可得到這樣的程式：
r, s, n := 0, 0, n;
{ (r = msc n) ∧ (s = mtc n) ∧ (0 ≤ s) ∧ (0 ≤ n ≤ N), bnd: n }
do n ≠ N ->
if A n > 0 -> s := s + 1
| A n = 0 -> skip
| A n < 0 -> s := (s - 1) ↑ 0
fi;
r := r ↑ s;
n := n + 1
od
{ r = 〈↑ p q : 0 ≤ p ≤ q ≤ N : credit p q〉 }
我們在 invariant 中多放了一個 0 ≤ s，使得 A n > 0 與 A n = 0 之中的 (↑ 0) 都可以不用做。條件 0 ≤ n ≤ N 看來囉唆又累贅，常常在計算中被放在一邊不提及，但它相當重要：有了 0 ≤ n, 許多 splitting off 的動作才是被允許的。
後記
這個問題是 Kaldewaij (1990)中的一個習題。熟悉演算法的讀者可能早已發現此問題可以縮減成最大區段和 (maximum segment sum) 問題 --- 把正數都變成 1, 負數都變成 -1, 然後算最大區段和，就是最大信用了。確實，導出的程式和最大區段和問題相當像。
關於最大區段和，我只在英文 blog 上有一個函數語言版的推導。也許改天再寫寫。
讀者一定覺得：處理陣列的 index 怎麼這麼麻煩，這麼容易出錯？有時是 n, 有時是 n+1, (≤) 和 (<) 很容易搞錯。我也這麼覺得。這類問題先天上就很難 --- 寫處理陣列的程式最容易弄錯的就是這些事情。也因此，我們希望用這些符號訓練自己如何小心翼翼地推導出正確的程式。掌握這些技巧，使得最後的程式是對的。這會比寫出錯誤的程式然後除錯來得容易。
另一方面，也正是因為陣列 index 如此難用，才使我們考慮使用比較高階的資料結構，例如串列、代數資料結構... 以至於函數語言。
參考資料
Anne Kaldewaij. Programming: the derivation of algorithms. Prentice-Hall, 1990.