二分查找法（Binary search algorithm）是一個很常見的算法，從＜編程珠玑＞裡再次看到時又有新的收獲。
直接看代碼吧，下面是常見的實現代碼：
int binary_search(int *a, int num, int t)
{
int start = 0, end = num - 1;
while(end >= start){
int middle = (start + end) / 2;
int tmp = a[middle];
if(tmp < t){
start = middle + 1;
}else if(tmp > t){
end = middle - 1;
}else{
return middle;
}
}
return -1;
}
優化後的代碼為（這個優化的思想也挺好的，不知道有沒有一套系統的方法來思考出這個優化思路）：
int binary_search(int *a, int num, int t)
{
int low = -1, high = num - 1;
while(low + 1 != high){
int middle = (low + high) / 2;
if(a[middle] < t){
low = middle;
}else{
high = middle;
}
}
if(a[high] != t)
return -1;
else
return high;
}
如果直接看這段代碼，有可能不知道是怎麼回事。但是運用書中提到的“程序驗證”的方法後，原理就顯而易見了，修改後的代碼為：
1 int binary_search(int *a, int num, int t)
2 {
3 int low = -1, high = num - 1;
4
5 //invariant: low < high && a[low] < t && a[high] >= t
6 while(low + 1 != high){
7 int middle = (low + high) / 2;
8 if(a[middle] < t){
9 low = middle;
10 }else{
11 high = middle;
12 }
13 }
14 //assert： low +1 = high && a[low] < t && a[high] >= t
15
16 if(a[high] != t)
17 return -1;
18 else
19 return high;
20 }
21
“程序驗證” 的思想可以簡述為：不管是驗證一個函數，還是一條語句，一個控制結構（循環，if分支等），都可以采用兩個斷言（前置條件和後置條件）來達到這個目的。前置條件是在執行該處代碼之前就應該成立的條件，後置條件的正確性在執行完該處代碼後必須得到保證。（ps: 斷言也算是一種驗證的手段）
上面這段代碼的原理是給定一段區間 (low, high] ，如果満足 a[low] < t && a[high] >=t && high = low + 1，那麼有兩種情況存在：1. a[high] = t ; 2.與t相等的元素不存在。由於數組a 肯定滿足條件a[low] < t && a[high] >=t，所以該算法要做的就是把區間 (-1, num -1] 縮小到(low, low+1]。
1. 在執行代碼6~17行時，始終保證low < high && a[low] < t && a[high] >= t 成立。
2. 在執行完6~17行後，肯定滿足條件a[low] < t && a[high] >=t && high = low + 1，因為循環退出的條件是 high = low + 1，而該循環始終保證上面第１條。
經過這樣的分析後，我們能對程序的正確性有更好的掌握，同時程序也更易理解。
