20世紀60年代末，人們就在討論驗證其他程序正確性的那些驗證程序的前景了。不幸的是，到今天這幾十年間，除了屈指可數的幾個例外，自動驗證系統依然還是紙上談兵。儘管以前的預期落空了，對程序驗證所進行的研究還是給我們提供了很有價值的東西——對計算機編程的基本理解，這比一個吞入程序，然後閃現「好」或「壞」的黑匣子要好得多。
本章的目的是闡述這些基本理解如何幫助實際程式設計師編寫正確的程序。一位讀者將大多數程式設計師習以為常的方法形象地歸納為「編寫代碼，然後丟給另一個部門，由QA（質量保證）或QT（質量測試）來處理錯誤」。本章描述一種不同的方法。在開始討論之前，我們必須正確地認識到：編程技巧僅僅是編寫正確程序的很小一部分，大部分內容還是前面三章討論過的主題：問題定義、算法設計以及數據結構選擇。如果這些步驟都完成得很好，那麼編寫正確的程序通常是很容易的。
4.1 二分搜索的挑戰
即使有了最好的程序設計，程式設計師也常常要編寫巧妙的代碼。本章討論一個需要特別仔細地編寫代碼的問題：二分搜索。在回顧這個問題並簡介其算法之後，我們將使用驗證原則來編寫程序。
我們首次遇到這個問題是在2.2節。我們需要確定排序後的數組
中是否包含目標元素t。[1]準確地說，已知
且
，當n=0時數組為空。t與x中元素的數據類型相同。無論是整型、浮點型還是字符串型，偽代碼都必須同樣地正確運行。答案存儲在整數p中（記錄位置）：當p為-1時，目標t不在數組
中；否則
，且
。
二分搜索通過持續跟蹤數組中包含元素t的範圍（如果t存在於數組的話）來解決問題。一開始，這個範圍是整個數組；然後通過將t與數組的中間項進行比較並拋棄一半的範圍來縮小範圍。該過程持續進行，直到在數組中找到t或確定包含t的範圍為空時為止。在有n個元素的表中，二分搜索大約需要執行
次比較操作。
多數程式設計師都認為有了上述描述在手，編寫代碼是輕而易舉的事。但是他們錯了。相信這一點的唯一辦法就是馬上放下書，然後自己編寫這段程序。試試看。
我在給專業程式設計師上課時布置過該問題。學生們有數小時的時間將上面的描述轉換成程序。可以使用任何一種程式語言，高級偽代碼也可以。規定的時間到了的時候，幾乎所有的程式設計師都報告說自己完成了該任務的正確代碼。然後，我們用30分鐘時間來檢查這些程式設計師已經用測試實例檢驗過了的代碼。在幾個課堂里對一百多名程式設計師的檢查結果大同小異：90%的程式設計師都在他們的程序中發現了錯誤（並且我不相信那些沒有發現錯誤的程序就一定是正確的）。
我很驚詫：提供充足的時間，竟然僅有約10%的專業程式設計師能夠將這個小程序編寫正確。但是他們不是唯一一批發現這個任務困難的人：Knuth在其The Art of Computer Programming, Volume 3: Sorting and Searching的6.2.1節的歷史部分中指出，雖然第一篇二分搜索論文在1946年就發表了，但是第一個沒有錯誤的二分搜索程序卻直到1962年才出現。
4.2 編寫程序
二分搜索的關鍵思想是如果t在
中，那麼它就一定存在於x的某個特定範圍之內。這裡使用mustbe(range)來表示：如果t在數組中，那麼它一定在range中。使用這個定義可以將上面描述的二分搜索轉換成下面的程序框架：
initialize range to 0..n-1
loop
{ invariant: mustbe(range) }
if range is empty,
break and report that t is not in the array
compute m, the middle of the range
use m as a probe to shrink the range
if t is found during the shrinking process,
break and report its position
該程序的最重要部分是大括號內的循環不變式（loop invariant）。之所以把這種關於程序狀態的斷言（assertion）稱為不變式（invariant），是因為在每次循環疊代之前和之後，該斷言都為真。這個名稱將前面已有的直觀概念形式化了。
現在進一步完善程序，並確保所有的操作都遵循該不變式。我們面對的第一個問題就是範圍（range）的表示方式：這裡使用兩個下標l和u（對應下限lower和上限upper）來表示範圍l..u。（9.3節的二分搜索函數使用起始位置和長度來表示範圍）。邏輯函數mustbe(l, u)是說：如果t在數組中，t就一定在（閉區間）範圍x[l..u]之內。
下一步的工作是初始化。l和u應該為何值，才能使mustbe(l, u)為真？顯而易見的選擇是0和n-1：mustbe(0, n-1)是說如果t在x中，那麼t就一定在x[0..n-1]中；而這恰好就是我們在程序一開始就知道的事實。於是，初始化由賦值語句l=0和u=n-1組成。
下一步的任務是檢查空範圍並計算新的中間點m。當l > u時範圍l..u為空，在這種情況下，將特殊值-1賦給p並終止循環，程序如下：
if l > u
p = -1; break
break語句終止了外層的loop。下面的語句計算範圍的中間點m：
m = (l + u) / 2
「/」運算符實現整數除法：6/2等於3，7/2也等於3。至此，擴展的程序如下：
l = 0; u = n-1
loop
{ invariant; mustbe(l, u) }
if l > u
p=-1; break
m = (l + u) / 2
use m as a probe to shrink the range l..u
if t is found during the shrinking process,
break and note its position
為了完善循環體中的後三行，需要比較t和x[m]，並採取合適的操作來保持不變式成立。因此代碼的一般形式為：
case
x[m] < t: action a
x[m] == t: action b
x[m] > t: action c
對於操作b，由於t在位置m，所以將p設為m並終止循環。由於另外兩種情況是對稱的，這裡集中討論第一種情況並認為對最後一種情況的討論可以根據對稱性得到（這也是在下一節中我們必須精確驗證代碼正確性的一部分原因）。
如果x[m]<t,那麼x[0]
x[1]
…
x[m]<t。因此，t不可能存在於x[0..m]中的任何位置。將該結論與已知條件「t不在x[l..u]之外」相結合，可知t一定在x[m+1..u]之內，記為mustbe(m+1, u)。然後，通過將l設為m+1可以再次確立不變式mustbe(l, u)。將這些情況放入前面的代碼框架中，就獲得了最終的函數。
l = 0; u = n-1
loop
{ mustbe(l, u) }
if l > u
p = -1; break
m = (l + u) / 2
case
x[m] < t: l = m+1
x[m] == t: P = m; break
x[m] > t: u = m-1
這是一個簡短的程序：只有9行代碼和一個不變式斷言。程序驗證的基本技術（精確定義不變式並在編寫每一行代碼時隨時保持不變式的成立）在我們將算法框架轉化成偽代碼時起到了很大的作用。該過程使我們對程序的正確性樹立了一些信心。但是這並不意味著該程序就一定是正確的。在繼續往下閱讀之前，請花幾分鐘時間確定該代碼的功能是否與所描述的一致。
4.3 理解程序
當面對複雜的編程問題的時候，我總是試圖得到如同上面那樣詳細的程序代碼，然後使用驗證方法來增強自己對程序正確性的信心。本書中的第9章、第11章和第14章也將在這個層面上使用驗證技術。
本節我們將在近乎吹毛求疵的細節層面上研究對二分搜索程序所進行的驗證分析，實踐中我很少做這麼多正式的分析。下一頁的程序大量使用斷言進行注釋，從而形式化了最初編寫代碼時所用的直觀概念。
代碼的開發是自上而下進行的（從一般思想開始，將其完善為獨立的代碼行），該正確性分析則是自下而上進行的：從每個獨立的代碼行開始，檢查它們是如何協同運作並解決問題的。
我們從第1行至第3行開始討論。mustbe的定義如下：如果t在數組中，那麼它一定在x[0..n-1]中。由此可知，第1行的斷言mustbe(0, n-1)為真。於是，根據第2行的賦值語句l=0和u=n-1可以得到第3行的斷言：mustbe(l, u)。
下面討論困難的部分：第4行至第27行的循環。關於其正確性的討論分為3個部分，每部分都與循環不變式密切相關。
- 初始化。循環初次執行的時候不變式為真。
- 保持。如果在某次疊代開始的時候以及循環體執行的時候，不變式都為真，那麼，循環體執行完畢的時候不變式依然為真。
- 終止。循環能夠終止，並且可以得到期望的結果（在本例中，期望的結果是p得到正確的值）。為說明這一點需要用到不變式所確立的事實。
對於初始化，我們注意到第3行的斷言與第5行的相同。為確立其他兩條性質，對第5行至第27行進行分析。討論第9行和第21行（break語句）時，將確立終止性質。如果持續下去，直至第27行，就可以得到保持性質，因為這又與第5行相同。
1． { mustbe(0, n-1) }
2． l = 0; u= n-1
3． { mustbe(l, u) }
4． loop
5． { mustbe(l, u) }
6． if l > u
7． { l > u && mustbe(l, u) }
8． { t is not in the array }
9． p = -1; break
10． { mustbe(l, u) && l <= u }
11． m = (l + u) / 2
12． { mustbe(l, u) && l <= m <= u }
13． case
14． x[m] < t:
15． { mustbe(l, u) && cantbe(0, m) }
16． { mustbe(m+l, u) }
17． l = m+1
18． { mustbe(l, u) }
19． x[m] == t:
20． { x[m] == t }
21． p = m; break
22． x[m] > t:
23． { mustbe(l, u) && cantbe(m, n-1) }
24． { mustbe(l, m-1) }
25． u = m-1
26． { mustbe(l, u) }
27． { mustbe(l, u) }
第6行的成功測試將得到第7行的斷言：如果t在數組中，那麼它就必定在位置l和u之間，且l > u。這些事實就意味著第8行的斷言成立：t不在數組中。於是在第9行設定p為-1後，就可以正確地終止循環。
如果第6行的測試失敗，就進入到第10行。不變式依然為真（我們沒有對其做任何改動），並且由於測試失敗，可得l
u。第11行將m設為l和u的平均值，向下取整為最接近的整數。由於平均值總是位於兩個值之間並且取整不會使之小於l，所以得到第12行的斷言。
從第13行至第27行的case語句考慮到了所有3種可能。最容易分析的一個分支是位於第19行的第二個分支。由第20行的斷言，我們將p設定為m並終止循環是正確的。這是第二處終止循環的地方（一共兩處），由於兩次對循環的終止都是正確的，於是我們確立了循環終止的正確性。
下面討論case語句中的兩個對稱分支。由於在編寫代碼的時候，我們把精力集中在第一個分支上，現在我們將注意力轉移到第22行～第26行。考慮第23行的斷言。第一個子句是不變式，循環並沒有對其進行改變。由於t < x[m]
x[m+1]
…
x[n-1]，第二個子句亦為真，於是我們可以知道t不在數組中任何高於m-1的位置，使用簡短記法表示為cantbe(m, n-1)。邏輯告訴我們，如果t一定在l和u之間，而且不等於或高於m，那麼t就一定在l和m-1之間（前提是t在x中），於是得到第24行。第24行為真時執行第25行可得第26行為真——這是賦值的定義。case語句的這個分支也就再次確立了第27行的不變式。
第14行至第18行的討論具有完全相同的形式，至此，我們完成了對case語句所有三個分支的分析。一個正確地終止了循環，其他兩個則保持了不變式。
該代碼分析表明，如果循環能夠終止，那麼就可以得到正確的p值。但是，程序中仍有可能包含死循環；事實上，這正是那些專業程式設計師編寫該程序時所犯的最常見的錯誤。
我們的停機證明從另一個角度對範圍l..u進行了考慮。初始範圍為某一有限大小（n），第6行至第9行確保當範圍中的元素少於一個時終止循環。因此，要證明終止，我們必須證明在循環的每次疊代後範圍都縮小了。第12行告訴我們，m總處於當前範圍內。case語句中不終止循環的兩個分支（第14行和第22行）都排除了範圍中位置m處的值，由此將範圍大小至少縮小1。因此，程序必會終止。
有了這些背景分析，我對我們進一步討論這個函數更有信心了。下一章涵蓋了以下主題：用C來實現該函數，然後進行測試以確保程序正確而且高效。
4.4 原理
本章的練習展示了程序驗證的諸多優勢：問題很重要，需要認真地編寫代碼；程序的開發需要遵循驗證思想；可以使用一般性的工具進行程序的正確性分析。該練習的主要缺點在於其細節層面：在實踐中不需要這么正式。幸運的是，這些細節闡述了許多一般性的原理，包括以下原理。
斷言。輸入、程序變量和輸出之間的關係勾勒出了程序的「狀態」，斷言使得程式設計師可以準確闡述這些關係。這些斷言在程序生命周期中的角色在下一節中論述。
順序控制結構。控制程序的最簡單的結構莫過於採用「執行這條語句然後執行下一條語句」的形式。可以通過在語句之間添加斷言並分別分析程序執行的每一步來理解這樣的結構。
選擇控制結構。這些結構包括不同形式的if和case語句；在程序運行過程中，多個分支中的一個被選擇執行。我們通過分別分析每一個分支說明了該結構的正確性。一定會選擇某個分支的事實允許我們使用斷言來證明。例如，如果執行了語句if i >j，那麼我們就可以斷言i >j並且使用這個事實來推導出下一個相關的斷言。
疊代控制結構。要證明循環的正確性就必須為其確立3個性質：
我們首先討論由初始化確立的循環不變式，然後證明每次疊代都保持該不變式為真。由數學歸納法可知這兩步就證明了在循環的每次疊代之前和之後該不變式都為真。第三步是證明無論循環在何時終止執行，所得到的結果都是正確的。綜合這些步驟可知：只要循環能停止運行，那麼其結果就是正確的。因此我們還必須用其他方法證明循環一定能終止（二分搜索的停機證明所使用的方法是比較常見的）。
函數。要驗證一個函數，首先需要使用兩個斷言來陳述其目的。前置條件（precon- dition）是在調用該函數之前就應該成立的狀態，後置條件（postcondition）的正確性由函數在終止執行時保證。如此可以得到C語言二分搜索函數如下：
int bsearch(int t, int x[], int n)
/* precondition: x[0] <= x[1] <= ... <= x[n-1]
postcondition:
result == -1 => t not present in x
0 <= result < n => x[result] == t
*/
這些條件與其說是事實陳述不如說是一個契約：如果在前置條件滿足的情況下調用函數，那麼函數的執行將確立後置條件。一旦證明函數體具有該性質，在以後的應用中就可以直接使用前置條件和後置條件之間的關係而不再需要考慮其實現。該方法在軟體開發中通常稱為「契約編程」。
4.5 程序驗證的角色
當一個程式設計師想要讓別人相信某段代碼正確的時候，首選的工具通常就是使用測試用例：運行程序並手動輸入數據。這是很有效的：適用於檢測程序的錯誤、易於使用並且很容易理解。然而，程式設計師明顯對程序有更深的理解——如果他們做不到這一點的話，就不可能編寫出第一手程序。程序驗證的一個主要好處就是為程式設計師提供一種語言，用來表達他們對程序的理解。
本書的後續部分（特別是第9章、第11章和第14章）將會使用驗證技術進行複雜程序的開發。在編寫每一行代碼的時候都使用驗證語言來解釋，這對概括每個循環的不變式特別有用。程序文本中重要的解釋以斷言的形式結束；而確定在實際軟體中應包含哪些斷言則是一門藝術，只能在實踐中學習。
驗證語言常用於程序代碼初次編寫完成以後，在進行初次模擬的時候開始使用。測試過程中，違反斷言語句的那些情況指明了程序的錯誤所在，而對相應情況形式的分析則指出了在不引入新錯誤的情況下如何修正程序中的錯誤。調試過程中，需要同時修正錯誤代碼和錯誤的斷言：總是保持對代碼的正確理解，不要理會那種「只要能讓程序工作，怎麼改都行」的催促。第5章將介紹程序驗證在程序的測試和調試過程中所扮演的幾種重要角色。斷言在程序維護過程中至關重要：當你拿到一段你從未見過而且多年來也沒有其他人見過的代碼時，有關該程序狀態的斷言對於理解程序是很有幫助的。
這些僅是編寫正確程序的很小一部分技術。編寫簡單的代碼通常是得到正確程序的關鍵。另一方面，幾個熟悉這些驗證技術的專業程式設計師曾經對我講述了一段在我自己編程時也常遇到的經歷：當他們編寫程序的時候，「困難」的部分第一次就可以正確運行，而那些「容易」的部分往往會出毛病。當開始編寫困難的部分時，他們會坐下來仔細編程並成功地使用強大的正規技術。在編寫容易的部分時，他們又返回到自己的編程老路上來了，結果當然是舊病復發了。在親身經歷之前，我也並不相信會有這種現象，這種尷尬的現象是經常使用驗證技術的良好動力。
本文摘自：《編程珠璣》第2版。[美] 喬恩·本特利（Jon Bentley） 著，黃倩，錢麗艷 譯。
- 經典算法和數據結構習題精粹，計算機科學領域20餘年暢銷不衰的不朽經典
- 程式設計師案頭常備，融深邃思想、實戰技術與趣味軼事於一爐的奇書
- 帶你真正領略計算機科學之美
多年以來，當讓程式設計師推選喜愛的計算機圖書時，《編程珠璣》總是位於前列。正如自然界裡珍珠出自細沙對牡蠣的磨礪，計算機科學大師喬恩·本特利以其獨有的洞察力和創造力，從磨礪程式設計師的實際問題中凝結出一篇篇編程「珠璣」，成為世界計算機界名刊《ACM通訊》歷史上*受歡迎的專欄，*終結集為兩部計算機科學經典名著，影響和激勵著一代又一代程式設計師和計算機科學工作者。本書為第一卷，主要討論計算機科學中*本質的問題：如何正確選擇和高效地實現算法。
在書中，作者選取許多具有典型意義的複雜編程和算法問題，生動描繪了歷史上大師們在探索解決方案中發生的軼事、走過的彎路和不斷精益求精的歷程，引導讀者像真正的程式設計師和軟體工程師那樣富於創新性地思考，並透徹闡述和總結了許多獨特而精妙的設計原則、思考和解決問題的方法以及實用程序設計技巧。解決方案的代碼均以C/C++語言編寫，不僅有趣，而且有很大的實戰示範意義。每章後所附習題極具挑戰性和啟發性，書末給出了簡潔的解答。