0.5 正確性

程式語言是設計者選擇用來看待世界的抽象方式。這樣的選擇必然是基於一些考量：如果設計者希望程式能很容易分割、重用，他可能選擇易於將大問題分解成小問題的觀點。如果設計者希望該語言能有效率很高的實作，這語言看待世界的方式可能就和機器的世界觀很接近。

本書選擇的方向則是「程式語言應能幫助我們確保程式的正確性。」

但什麼是「正確」？直觀說來，一個程式「正確」的意思是該程式「做到了我們要它做的事。」但，電腦本來不就只能一個指令一個動作地做我們要它做的事嗎？那麼「正確」的意思到底是什麼？

我們考慮一下這個問題：

這是經典的「最大區段和」問題。如前面的章節所述，面對一個問題，我們先把它描述成符號。如果 a 是給定的那串數字，N 是其長度，a[i] 是數字中的地 i 個，而 m 是我們想求出的、最大的那個和，最大區段和問題可以描述成這樣：

其中 sum (i,j) 代表 a[i]..a[j-1] 的和，而 max S 找出集合 S 中最大的那個。

但（許多讀者可能也知道）這個問題其實有個線性時間內可執行完畢的解：將這串數字 a 從頭到尾看過一遍，維持兩個變數 s 和 m。每看到一個新數字 a[j], 將 s 更新為 0 與 s + a[k] 中較大的那個，並把 m 更新為 s 與 m 中較大的那個。寫成程式的話，可能是這樣：

   s, m = 0, 0
   for k in range(0,n-1)
     s = max (0, s + a[k])
     m = max (s, m)

那麼，明顯的問題來了。上面的程式和問題描述([RefUndefined])一點也不像。我們怎麼知道程式真正實作了([RefUndefined])的要求？

由此談「正確性」，相信清楚多了。數學式([RefUndefined])給的是一個規格(specification)，談的是我們要的結果(what), 而程式描述的則是怎麼做(how). 「正確性」總是相對於一個規格而言的：描述「怎麼做」的程式是否真做到了規格的要求？

「最大區段和」的例子可以給我們幾個啟示。首先，把「要什麼」和「怎麼做」牽上關聯，有時是很困難的。當我們說一個程式「很難懂」，其中一個意思是很難看出「為什麼這個程式實作出了這個規格？」（也就是說「為什麼這個程式是正確的？」）看懂一個程式，也就是了解他為何是正確的。

「最大區段和」的例子也告訴我們，「難懂」的程式不一定要很長。上面的程式短短四行，但若沒有輔助解釋，一般人可能很難「看懂」它。(註7) 理解這個程式的關鍵是：m永遠是a[0]..a[k]中所有連續區段最大的和，而s永遠是a[0]..a[k]中{\em 最右端為a[k]}的連續區段中最大的和。這兩個條件是該迴圈的恆式(loop invariant)。恆式是了解一個迴圈最重要的資訊。

如果規格已經不見了呢？這樣的情形更糟。當我們在沒有規格的情況下問一個程式「是做什麼的」，我們真正問的是「這個程式符合的規格是什麼？」這可能是個難題。回頭看看上面的程式，如果沒有給([RefUndefined])，你能說得出這個程式在做什麼嗎？