编程珠玑第四章探讨

首先，本章中再次提及了TAOCP，可以说已经是一章提一次的节奏了，作者这么热衷于提到本书还是有一定道理的，详尽的数学证明让我们有值得一读的必要。第四章的主题是如何证明自己的程序是正确的，这是一个比较困难的问题，尤其是逻辑复杂的代码，对于不同的程序周期作者都针对性的提出了不同的方法和原理。比如二分搜索的停机证明，然后对于函数，作者介绍了重要的「契约编程」。其中还谈到了心理问题：「困难」的部分第一次就可以正确运行，而那些「容易」的部分往往会出毛病。所以呢，作者也鼓励使用验证技术开发。觉得本章最重要的应当就是对循环不变式的理解。

问题探讨

2.因为返回的是第一个位置，所以思路是如果找到并且尚有未检查的区间，那么要再次深入迭代。

left = -1;
right = n; // 数组长度为n
while(left + 1 != right){
    mid = (left + right) / 2;
    if(num[mid] < target)
        left = mid;
    else
        right = mid; // ‘<=‘ 只要 left + 1 != right 会一直迭代 
}

4.只要可以验证计时程序运行是正确的，那么就可以证明运行时间确实是对数的。参考第五章。

6.每次都会减少一颗豆子，所以只要证明程序是正确运行的，则一定会终止。第二问的意思是每次减少的豆子因为不是两个白就是0个白，所以白色的豆子在初始时是偶数的，那么最后一定是个黑色的豆子；反之，是白色的。

7.线段已经有序，利用习题2的思路，我们可以先找到一条线段，判断其是上面、下面还是线段上。

9.(1)首先应当证明每一次的操作能够得到当前一步想要的结果，然后因为i是递增的，且每次都加1，所以从0开始直到最后计算结束，n个维度都得到了相加。且i每次都递增，所以一定会结束。

(2)一开始max是数组第一个数字，在循环中，数组中第i个数字会与max比较，如果比max大就更新，另一方面0到i-1也已经比较完了。i从1开始，每次比较后i都会增加1，所以循环会结束，数组中的数字也都会与max比较，从而得到正确的最大值。

(3)循环中每次i都会自增1，所以循环一定会终止。如果i超过了范围会终止，如果找到了也会终止。因为i是从0开始顺序递增的，所以如果找到了，那么一定是第一个，程序因此是正确的。

(4)每次如果满足条件递归下去，那么递归的定义域会一直缩小。要么减一，要么除以2，而且程序中给定了边界条件。每次递归的结果都是上一层需要的，所以程序可以结束且能得到正确答案。

摘录

• 初始化。循环初次执行的时候不变式为真。
• 保持。如果在某次迭代开始的时候以及循环体执行的时候，不变式都为真，那么，循环体执行完毕的时候不变时依然为真。
• 终止。循环能够终止，并且可以得到期望的结果(在本例中，期望的结果是p得到正确的值)。为说明这一点需要用到不变时所确立的事实。

……

如果在前置条件满足的情况下调用函数，那么函数的执行将确立后置条件。一旦证明函数体具有该性质，在以后的应用中就可以直接使用前置条件和后置条件之间的关系而不再需要考虑其实现。该方法在软件开发中通常称为「契约编程」。