來自《Writing Solid Code》的一則小故事，Donald Knuth在其著名的排版軟體TEX的封面上寫到：“I believe that the final bug in TEX was discovered and removed on November 27, 1985. But if, somehow, an error still lurks in the code, I shall gladly pay a finder 's fee of $20.48 to the first person who discovers it.”（我相信TEX的最後一個bug已經在1985年11月27日發現被移除。但是如果代碼中仍有錯誤，我将高興地支付第一個發現的人20.48美元的報酬。）
這個故事重要的一點，不是Knuth最終是否支付了誰20.48美元，而是他對自己代碼的品質的自信。你認識的程式員中有多少人能自信地說他們的程式是零bug的？又有多少能發表這樣的聲明并支付費用？
1 為何要證明代碼是正确的？
《Programming Pearls》的第四章裡講到，證明程式的正确性給了程式員表達自己對代碼深入了解的機會。而《The Science of Programming》一書則用了開篇一章來解答這個問題。下面通過一小段代碼來解釋代碼正确性的重要性。
這段代碼是在沒有整數除法運算器的環境中計算商和餘數。為了驗證程式的正确性，我們加上一些輸出語句，但這會導緻大量的輸出和人工比較工作。于是我們将輸出改為斷言，即當出錯時才會輸出并停止程式。對于這一小段程式，前置斷言是y(除數)大于0，後置斷言是x = y*q + r (q商，r餘數)。
這一小段代碼看起來沒有什麼問題，直到有一天你看到了下面這樣的運作結果，花費一整天來查找錯誤的原因：
x = 6，y = 3，q = 1，r = 3
問題就在于，餘數r應該小于除數y。也就是說我們循環的條件應該是r >= y而不是r > y。其實如果我們的後置斷言足夠強的話，我們是可以省掉這浪費掉的一整天的查錯工作的。
接着某天你又碰到了r = -2的運作結果，因為被除數是負數，也就是說我們的前置斷言也不夠強。我們本可以早些捕捉到這些錯誤并節省掉兩天的查錯時間，我們要做的隻是讓前置和後置斷言足夠強！然而我們為什麼沒考慮到這些條件？
一定要不斷地試錯才能完善嗎？我們的問題在于對代碼段要做的事沒有細心地思考，我們應該在開始編碼前就寫好0 <= x and 0 < y以及x = y*q + r and 0 <= r < y的斷言。
但是像循環條件這種錯誤有辦法在一開始就避免嗎？在循環開始前和結束後，x = y*q + r都是成立的，是以它在循環中的每次疊代前後也應該成立的，即循環不變量（loop invariant），詳見第四部分：循環與歸納法。于是我們将這個條件補充到循環開始之前以及每次疊代前後，并且也完善每條語句前後的斷言，使所有斷言都足夠強！
現在我們看下如何證明循環條件的正确性。後置斷言中有了and 0 <= r < y，很顯然循環條件應為r >= y。因為循環隻有這一個出口，隻有這樣循環終止時才會r < y。多簡單啊！
2 正确性證明
2.1 基石 - 斷言
這樣看起來，如果我們知道如何使所有斷言條件盡可能地強，如果我們學會如何推導出斷言和程式，我們就不會犯這麼多錯誤。我們知道程式是正确的，我們就根本不需要調試。花在運作測試用例，檢視輸出，查找錯誤的時間完全可以用來做其他事兒。
1） 推導出斷言條件：知道如何寫布爾表達式還不夠，還需要知道：
如何推導出它們；
如何簡化它們；
如何證明一個條件跟在另一個後面；
如何證明在某些狀态下條件，不為真；
2）“推導出”程式代碼：代碼正确性的證據将會指引我們寫出正确的代碼。但不可避免的，凡人都是會出錯的。是以盡管debug變得不必要，但還是需要測試來增加我們的信心。
2.2 數學函數與程式函數的誤解
這裡與要避免一個誤區：數學函數與程式函數是不同的！我們不可能由前置斷言和後置斷言就推導出代碼如何寫！《SICP》裡寫到數學與計算機科學的不同，前置和後置斷言隻是我們對函數功能的聲明式描述（類似于數學函數），而代碼實作是指令式的，正确性證明的難點就在于處理兩者間的轉換：
Declarative and imperative descriptions are intimately related, as indeed are mathematics and computer science. For instance, to say that the answer produced by a program is“correct” is to make a declarative statement about the program. There is a large amount of research aimed at establishing techniques for proving that programs are correct, and much of the technical difficulty of this subject has to do with negotiating the transition between imperative statements (from which programs are constructed) and declarative statements (which can be used to deduce things). In a related vein, an important current area in programming-language design is the exploration of so-called very high-level languages, in which one actually programs in terms of declarative statements. The idea is to make interpreters sophisticated enough so that, given“what is”knowledge specified by the programmer, they can generate “how to” knowledge automatically.
《Programming Pearls》裡提到過，正确性證明所處的位置是：定義問題 => 算法和資料結構設計 => 寫僞代碼 => 證明正确性 => 翻譯成具體實作 => 單元測試… 是以，我們要證明已有僞代碼或代碼的正确性，而不是推導出全部代碼實作，這是不可能的。
2.3 用斷言證明
學會了如何寫斷言，我們就能夠證明常見語句的正确性了。《Programming Pearls》裡提到了一些常見語句證明的基本原則，這些就是證明的寶石：
Ø 斷言：如前所述，輸入、程式變量、輸出描述了程式的狀态，而斷言準确地描述了這三者間的關系。
Ø 順序語句：像do this statement then that statement這種順序結構是最簡單的程式控制結構，我們通過在它們之間放置斷言并逐漸獨立分析來了解這樣的結構。
Ø 選擇語句：執行時隻有一種選擇可以執行，但我們需要分别考慮幾種選擇。當一種選擇執行時，我們可以繼續向後推導出下一個斷言。
Ø 循環語句：循環是正确性證明的重點，詳見第3部分“循環與歸納法”。
Ø 子例程：首先通過precondition和postcondition指出子例程的目的，一旦證明了子例程body的正确性，那麼之後我們就認為子例程的執行建立了從precondition到postcondition的關系，而不用再考慮其實作了。
2.4 程式設計這件小事
程式設計這件事看起來很小，甚至一些人認為正确了解了需求，有了高層設計，編碼就是體力活兒了。其實不然，即便有了各種詳盡的前期準備，在将紙面上的解決方案轉變成真正的代碼實作時還是會碰到各種各樣的問題。是以作為程式員，不管是多高的職位、多豐富的經驗，永遠都不能喪失編碼能力，“紙上得來終覺淺，絕知此事要躬行！”。言歸正傳，在開始動手前，一定要先在紙上分析思考，并注意下面幾個關鍵點，之後才能開始編碼：
Ø 循環：循環是算法設計、分析、正确性證明的關鍵點，是以對于循環一定要仔細設計好僞代碼：
n 1）初始化：需要哪些變量，變量初始化成什麼，是否需要定義在循環外；
n 2）終止條件：什麼條件下可以繼續循環，舉個例子看看會不會出現off-by-one問題；
n3）循環體：循環體裡應該做什麼，有沒有break, continue, return等其他改變循環順序的出口，疊代使用變量是否每次都清0了；
n 4）計數器：計數器怎樣累加，是否能每次疊代都變大或變小進而使循環正常終止，而不會造成死循環；body中是否修改計數器的值而for/while中又再次修改，導緻一些未處理元素被跳過；
n 5）後處理：跳出循環後，需不需要進行一些遺留處理，使計算結果變完整，例如分頁的最後一批資料。
Ø 臨界值(corner case)：與循環的終止條件類似，其他代碼處如if/else可能也有一些條件檢測，都需要進行特殊情況的測試。
Ø 前置/後置條件(pre/post-condition)：是否驗證了非法參數，進行防禦式程式設計（《Code Complete》裡提及）。參數中所指的下标确定是從0開始還是1開始。
3 循環與歸納法
我們可以利用類似于數學歸納法證明遞歸函數的方式來證明循環的正确性。首先，我們要确定循環不變量，循環不變量就是用來幫助我們證明代碼正确性的，一般選取循環中的某個變量始終滿足的布爾條件。之後，必須證明它有Initialization、Maintenance、Termination三個性質（後面會詳述）才能說是循環的不變量。最後，循環終止時，循環不變量能幫我們證明代碼的正确性。
還是以一小段代碼為例。下面計算平方的函數square，找到循環不變量，設k表示第幾次疊代，則不變量為：S = k*n，i = k*1 = k。
此時還隻是我們憑直覺來定的，暫且将S和i當做循環不變量。下面将要嚴謹地證明S和i的确是循環不變量。
1）Initialization：在循環開始前它是真的。
k = 0即循環未開始時：
S = k * n = 0 * n = 0；i = k = 0
根據代碼，循環不變量為真。
2）Maintenance：在每次疊代前都是真的。1）和2）即可引入歸納法來證明。
假設k = m時，循環不變量S = m * n和i = m為真。
那麼k = m + 1時，根據代碼：
S = m * n + n = (m + 1) * n = k * n；
i = m + 1 = k
是以，循環不變量S和i在每次疊代前都為真。
3）Termination：代碼能夠終止，這也是與數學歸納法證明的一個重要差別。
因為i每次疊代都會加1，是以循環一定能終止。
至此，我們可以确認，S和i是此循環的不變量。于是，我們就能夠證明：當循環終止時，即k = n，那麼S = k * n = n * n，即n的平方。是以此循環的确能夠正确地計算出n的平方。
附：思考如何選取循環不變量？
int j = 9;