Keith Braithwaite

函式的「大小」#

我們希望寫出正確的程式碼並有證據證明它是正確的。思考函式的**「大小」（size）對這兩個目標都有幫助——但這裡的大小不是指程式碼行數，而是函式所代表的數學函式的大小**。

圍棋的例子#

在圍棋（Go）中，有一個叫做 atari 的狀態：當一顆棋子只剩兩個或更多相鄰的空位（稱為 liberties）時，它不在 atari 狀態。我們可以寫一個函式：

boolean atari(int libertyCount)
    libertyCount < 2

這個函式看起來比實際上大。int 的定義域和 boolean 的值域組成的集合是 int x boolean，如果兩者大小相同，集合會有約 85 億個成員。要完整驗證函式的正確性，我們需要檢查約 43 億個範例。

這正是「測試無法證明沒有 bug」這一主張的本質。測試可以展示功能的存在，但我們仍面臨大小的問題。

用領域型別縮小函式#

問題領域幫了我們。圍棋的特性決定了一顆棋子的 liberties 數量不是任意的 int，而是 {1, 2, 3, 4} 中的一個。我們可以改寫為：

LibertyCount = {1,2,3,4}
boolean atari(LibertyCount libertyCount)
    libertyCount == 1

現在這個函式所計算的集合最多只有八個成員，只需要四個範例就能完整驗證其正確性。

啟示#

使用與問題領域（problem domain）緊密相關的型別來編寫程式，而不是使用原生型別（native types），能讓函式大幅縮小。確定這些型別的方法之一，是在撰寫函式之前，先用問題領域的術語找出需要檢查的範例。

這也是為什麼使用**領域導向型別（domain-inspired types）**是個好主意——它們能讓函式更小、更容易驗證正確性。