無錯誤程式設計
 |
 | 注意：請帶著批判的眼光看待下面的文章。編寫無錯誤的程式碼是不可能的。最好的開發者專注於編寫可靠且可維護的程式碼，但任何聲稱一段程式碼是無錯誤的人都沒有做好功課。 |
研究表明，最優秀程式設計師和最差程式設計師的生產力之間存在 20 倍的差距。也就是說，頂級程式設計師的工作效率是差勁程式設計師的 20 倍，大約是平均程式設計師的 5 到 10 倍。這意味著一個非常優秀的開發者可以在一天內完成其他人可能需要一個月才能完成的工作。提高生產力有幾種方法，但最重要的因素是準確性。
準確性與開發速度密切相關。最優秀的開發者從一開始就透過編寫無錯誤的程式碼來脫穎而出。如果您能夠編寫不包含任何錯誤的程式碼，您就不必浪費時間尋找錯誤。曾經想過為什麼隔壁桌那個悠閒工作的人做事比你快得多？那是因為他第一次就做對了。當然，完全防止錯誤是不可能的，但是
快速工作意味著準確工作，而不是努力工作。
那麼如何編寫無錯誤的程式碼？您可能會認為大多數錯誤是由粗心大意造成的，但實際上，大多數錯誤是由程式設計師沒有完全理解自己的程式碼造成的。如果您在 Java 中遇到 NullPointerException，這通常不是因為您忘記考慮空引用，而是因為您沒有真正理解空引用的變數的作用。
無錯誤程式設計的關鍵是牢固理解您編寫的程式碼。
要編寫無錯誤的程式碼，您首先必須學習如何證明一段程式碼有效。許多開發者在大學裡學習這些技術，但他們從來沒有真正學會在實際編碼中應用這些技術。其他開發者（尤其是那些沒有學位的人）一開始就沒有學習形式化方法，所以這是一個很好的起點。乍一看它可能過於理論化，但這是無錯誤程式設計的關鍵。
讓我們從一個非常簡單的程式開始。這裡目標是當程式終止時，型別為int的變數x包含值 10。我們將使用 C++ 在整本書中進行演示。
int x; x = 10;
這段程式碼顯然是無錯誤的。為了證明這一點，讓我們在程式碼的每一行前後新增用大括號括起來的條件。條件是邏輯語句，在執行時間條件所在的點上是正確的無論執行如何到達那裡。
{true}
int x;
{true}
x = 10;
{x == 10}
前兩個條件為真，因為我們在這兩個點上沒有任何資訊（注意，C++ 不預先初始化變數）。我們唯一知道的是那裡是true本身。但是，在執行完x = 10這一行之後，我們知道x的值是10，因為這是賦值的定義。我們可以用更通用的術語來表達這一點
{true} x = a {x == a}
這意味著，無論之前是什麼，在將a賦值給x之後，x==a將為真，即x的值將是a。我們將把它視為常量賦值的公理。
下面的程式也為x賦值10，但它採用了不同的方式。
int x, y; y = 10; x = y;
為了證明它是正確的，用條件再次對其進行註釋
{true}
int x, y;
{true}
y = 10;
{y == 10}
x = y;
{x == 10}
在對y賦值之後，我們可以說它的值是10。好吧，如果y是10，我們將其賦值給x，x也會是10。這將導致賦值的完整公理
{y == a} x = y {x == a}
類似的規則適用於賦值右側有表示式的情況。另一個重要的公理是，賦值不會改變任何未賦值的變數。
{y == a} x = b {y == a}
這仍然非常微不足道，只需要圍繞它構建其他部分。
您可能已經意識到，關於每個賦值，有兩個條件需要考慮：一個是它之前成立的條件，另一個是它之後成立的條件。前者稱為前置條件，後者稱為後置條件。我們將透過將它們連結來證明程式的正確性：一個語句的後置條件是下一個語句的前置條件。
if {P} S1 {R} and {R} S2 {Q} then {P} S1; S2 {Q}
這裡S1; S2表示兩個語句一個接一個地執行，即按順序執行。還有另外兩種型別的控制結構：條件語句和迴圈語句。我們將在後面學習如何推理它們。
我們開始正式的正確性證明所需要的最後一個公理是
if P => R and {R} S {T} and T => Q then {P} S {Q}
A => B表示A在邏輯意義上蘊含B。
如果這一切對你來說都是天書，不要驚慌。我們將涵蓋足夠的示例，讓這些東西開始變得有意義。
現在讓我們進行第一個正式的正確性證明。證明以下程式將10賦值給x。
int x, y, z; z = 1; y = 2 * z; x = y * 5;
對其進行註釋
{true}
int x, y, z;
{true}
z = 1;
{z == 1}
y = 2 * z;
{y == 2}
x = y * 5;
{x == 10}
我們有了註釋，但我們必須證明它們確實在它們被寫到的點上成立。
{true} int x, y, z {true}
這很簡單，因為變數定義從正確性的角度來看沒有任何作用。現在我們必須證明
{true} z = 1 {z == 1}
這是因為賦值的公理。由於它是一個公理，我們不需要進一步證明它。我們現在可以使用它作為下一個語句的前置條件
{z == 1} y = 2 * z {y == 2}
再進行一次
{y == 2} x = y * 5 {x == 10}
為什麼這證明了原始語句？如果我們像這樣命名語句和條件
{Q1: true}
S1: int x, y, z;
{Q2: true}
S2: z = 1;
{Q3: z == 1}
S3: y = 2 * z;
{Q4: y == 2}
S4: x = y * 5;
{Q5: x == 10}
並使用順序公理三次，我們得到
{Q1} S1 {Q2} and {Q2} S2 {Q3} => {Q1} S1; S2 {Q3}
{Q1} S1; S2 {Q3} and {Q3} S3 {Q4} => {Q1} S1; S2; S3 {Q4}
{Q1} S1; S2; S3 {Q4} and {Q4} S5 {Q5} => {Q1} S1; S2; S3; S4 {Q5}
我們本質上證明了整個程式從{true}（無論是什麼）到{x == 10}（x的值為10）。
這就是我們必須證明的，才能 100% 絕對確定程式碼是無錯誤的。請注意，現在毫無疑問，這段程式碼是正確的（當然，除非我們在證明中犯了錯誤）。這之所以成為可能，是因為我們對程式碼在每個可能的執行點上所發生的事情有非常清楚的理解。用條件對程式碼進行註釋使我們的期望變得明確，並且不得不以正式的方式來證明它們讓我們思考了為什麼這些期望是正確的。
在現實生活中，沒有人有時間進行正式的正確性證明，但瞭解如何進行這些證明對建立無錯誤的程式碼有很大幫助。關鍵是要明確期望。這可以防止您忘記null引用，以及其他一些事情。
讓我們繼續討論條件語句。
int x, y;
if (x % 2 != 0)
{
y = x + 1;
}
else
{
y = x;
}
我們想在這裡證明y在最後是偶數。條件語句的公理如下
given {P && R} S1 {Q} and {P && !R} S2 {Q} => {P} if R S1; else S2 {Q}
要證明條件語句是正確的，您必須證明兩件事。首先，您必須證明當條件為真時，“then”子句會給出正確的結果。其次，您必須證明當條件為假時，“else”子句會給出正確的結果。對前面的示例進行註釋
{true}
int x, y;
{true}
if (x % 2 != 0)
{
y = x + 1;
}
else
{
y = x;
}
{y % 2 == 0}
As for the variable definitions:
{true} int x, y {true}
檢查。我們沒有明確地為x賦值，但我們將證明使用其值的程式的正確性。C++ 不預先初始化區域性變數。變數的值是某些記憶體垃圾。我們這裡有一個條件語句，所以我們必須分別檢查then和else子句。
{Q1: true && x % 2 != 0} y = x + 1 {R1: true && y == x + 1 && x % 2 != 0}
顯然
true && y == x + 1 && x % 2 != 0 => (y - 1) % 2 != 0 => y % 2 == 0
現在，如果您使用鬆弛公理
{Q1} y = x + 1 {R1} and R1 => y % 2 == 0
----------------------------------------
{Q1} y = x + 1 {y % 2 == 0}
現在讓我們來處理else子句
{Q2: true && !(x % 2 != 0)} y = x {R1: true && y == x && !(x % 2 != 0)}
顯然
true && y == x && !(x % 2 != 0) => y == x && x % 2 == 0 => y % 2 == 0
同樣，使用鬆弛公理
{Q2} y = x {R2} and R2 => y % 2 == 0
------------------------------------
{Q2} y = x {y % 2 == 0}
現在將結果與條件語句的公理結合起來
{true && R} y = x + 1 {y % 2 == 0} and {true && !R} y = x {y % 2 == 0}
----------------------------------------------------------------------
{true} if R y = x + 1; else y = x {y % 2 == 0}
我知道您不相信它在現實生活中真的有用，但請繼續閱讀。我們最終將放棄數學，只使用證明的核心概念來生成無錯誤的程式碼。
讓我們編寫第一個包含一些實際值的程式。假設我們有一個int陣列，我們想將它的元素之和放入一個名為sum的變數中。我們將在本示例中學習如何推理迴圈，這將是您第一次看到它如何幫助您立即編寫正確的程式碼。我們將從一個預先製作的程式開始，但稍後我們將研究如何將正確性證明中使用的技術轉換為程式碼設計。
int[] array;
int length;
// Fill the array.
{Q: array has been created and has at least length elements and length >= 0}
int i, sum;
i = 0;
sum = 0;
while (i != length)
{
sum = sum + array[i];
i = i + 1;
}
{R: sum = array[0] + array[1] + ... + array[length-1]}
前置條件Q的宣告是為了確保我們不會嘗試讀取未分配的記憶體。在本示例中，我們不關心陣列是如何分配的或如何填充數字的。
迴圈是三種控制結構中最複雜的，也是最容易出錯的。困難在於迴圈是偽裝的條件語句序列，您甚至不知道它是多少個條件語句，因為它取決於執行時評估的條件。如果您嘗試透過視覺化迴圈的執行方式來推理迴圈，那麼您將遇到麻煩，尤其是當您擁有比上一個迴圈更復雜的迴圈時。視覺化是瞭解如何編碼某件事的一個重要步驟，但是如果您不想在截止日期前花時間除錯沒有視覺化的邊緣情況，那麼您最好靜態地推理您的程式碼。這並不一定意味著數學上。我們最終將完全放棄數學。
關鍵是將迴圈的動態特性轉換為靜態條件。如果我們能夠證明一個在每次評估條件之前都成立的條件，那麼我們就可以推理迴圈，而不依賴於視覺化。這個條件稱為迴圈的不變式。
{Q: array has been created and has at least length elements and length >= 0}
int i, sum;
{Q}
i = 0;
{Q && i == 0}
sum = 0;
{Q && i == 0 && sum == 0}
while (i != length)
{
sum = sum + array[i];
i = i + 1;
}
{R: sum = array[0] + array[1] + ... + array[length-1]}
在本示例中，我們只關心迴圈，因為其餘部分很簡單。不變式是sum包含從索引1到索引i-1的元素之和每次在評估條件之前，包括第一次執行到達迴圈時。
{I: sum == array[0] + ... + array[i-1]}
當執行到達迴圈時
{Q && i == 0 && sum == 0}
成立。它是否蘊含I？當然
Q && i == 0 && sum == 0 => sum = 'sum of elements from 0 to -1'
這是真的，因為索引0和索引-1之間沒有元素，而0個數字的總和為0。也就是說，空陣列所有元素的總和為0。如果陣列不為空，則迴圈體將執行，並且條件將再次評估。此時I為真（我們不考慮具有副作用的迴圈條件，稍後將詳細介紹）。迴圈條件也為真，因為否則我們不會進入迴圈體。我們要證明的是
{I && i != length}
sum = sum + array[i];
i = i + 1;
{I}
也就是說，不變數在迭代之間保持不變。語句之間使用什麼條件？sum已更新，但i未更新。試試
{Q1: sum == array[0] + ... + array[i-1] && i != length}
sum = sum + array[i];
{Q2: sum == array[0] + ... + array[i-1] + array[i] && i != length}
i = i + 1;
{I}
我們能證明
{Q1} sum = sum + array[i] {Q2}
嗎？我們這裡有一個小問題，因為我們無法證明array[i]是一個有效的表示式。i必須小於length且至少為0才能有效。此外，我們需要將陣列分配為至少具有length個元素的陣列（為了節省空間，我們將此條件表示為T）。因此，我們必須修改我們的不變數以包含此資訊。
{I: T && 0 <= i && i <= length && sum == array[0] + ... + array[i-1]}
請注意理解我們編寫的程式碼中的這一重要步驟。我們沒有將所有期望明確化。這就是錯誤潛入的方式。使用這個新的不變數，我們必須從頭開始。當執行命中迴圈時，它是真的嗎？
T && length >= 0 && i == 0 && sum == 0 => T && 0 <= i && i <= length && sum = 'sum of elements from 0 to -1'
這是真的。例如，我們知道i <= length，因為i == 0且length >= 0。它在迭代之間保持不變嗎？
{Q1: T && 0 <= i && i <= length && sum == array[0] + ... + array[i-1] && i != length}
sum = sum + array[i];
i = i + 1;
{I}
更新sum後找到正確的條件
{Q1: T && 0 <= i && i <= length && sum == array[0] + ... + array[i-1] && i != length}
sum = sum + array[i];
{Q2: T && 0 <= i && i <= length && sum == array[0] + ... + array[i-1] + array[i] && i != length}
i = i + 1;
{I}
我們知道array[i]是有效的，因為i上的約束包含在條件中。關於
{Q2} i = i + 1 {I}
?
{Q2: T && 0 <= i && i <= length && sum == array[0] + ... + array[i-1] + array[i] && i != length}
i = i + 1;
{Q3: T && 0 <= i-1 && i-1 <= length && sum == array[0] + ... + array[i-1] && i-1 != length}
我們將i更改為i-1，因為它是在執行語句之前i的原始值。
Q3 => I
因為
T && 0 <= i-1 && i-1 <= length && sum == array[0] + ... + array[i-1] && i-1 != length => T && 0 <= i && i <= length && sum == array[0] + ... + array[i-1]
例如，0 <= i-1意味著1 <= i，進而意味著0 <= i。i-1 <= length和i-1 != length一起意味著i-1 < length，進而意味著i <= length。
當迴圈終止時，其條件為假。此外，不變數為真。這是因為它每次在評估條件之前都為真。如果我們能證明
I && !(i != length) => R
我們就證明了當迴圈終止時R為真。這是微不足道的
T && 0 <= i && i <= length && sum == array[0] + ... + array[i-1] && i == length => sum = array[0] + array[1] + ... + array[length-1]
我們已經證明，如果程式終止，它將給出正確的結果。但是請注意，我們尚未證明它實際上會終止。這稱為部分正確性。完全正確性意味著還要證明程式會終止。我們將在後面詳細討論。
確保您理解以上內容。我只給出了幾個例子，因為這不是關於形式正確性證明的書。如果您覺得需要更深入地瞭解它，請查閱一些關於 Hoare 方法的書籍。如果您不理解它，本書的其餘部分將毫無意義。
那麼這如何幫助您更快地工作呢？您沒有時間一直進行程式碼的形式證明，但瞭解如何進行形式證明將有助於您，即使您沒有使用它。對先決條件、後置條件和不變數的充分理解將幫助您編寫更好的程式碼。現在，我們將介紹大量示例來說明這一點。