来自《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;
for(int i=0; i<10; i++)
j--;
一般来说，循环终止条件一定是循环不变量，但这种循环不变量是否有用呢？比如这一小段程序，i<10或者j>-100或i+j=9都可以作为循环不变量，关键是你要证明什么？循环不变量要反映你的目的，这样终止时才能帮助你正确程序的正确性！