二分查找法（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，而该循环始终保证上面第１条。
经过这样的分析后，我们能对程序的正确性有更好的掌握，同时程序也更易理解。