标签：
我个人曾经在大二的时候读过《算法导论》这本书，虽然我在之后的学习中很少再看这本书了，但是《算法导论》带给我的启蒙意义远超过其他我看到过的书籍，哪怕是如今研究一些比较深入的程序语言理论，也少有书籍能做到《算法导论》对我个人的影响，我认为唯一可以媲美它的就是Dan Friedman的《the little schemer》，关于《the little schemer》的内容我以后会讲，但是无论你是不是函数式编程的爱好者，我都推荐你来看《the little schemer》。
为什么讲《算法导论》对于我个人有如此之大的影响呢？我认为是它彻底改变了我对于写代码这件事的认识，以及写代码的方式的改变。
它让我认识到代码是可以证明其正确性的。
用在证明代码正确性的思想有两点，一个是分类讨论，另一个是数学归纳法，而其中的关键就是通过将情况的划归，和缩小问题的大小去构造子问题，再通过假设子问题的成立，构造关于当前问题的证明，从而证明函数的正确性，一个很好的类比就是数学归纳法，我们首先证明i=1时成立(基本情况成立)，然后假设i=n-1时成立(构造子问题成立)，证明i=n时成立（证明函数成立）。
我用一个红黑树插入的例子来说明我的思想。
首先红黑树的插入是进行一个与平衡二叉树插入同样的操作，然后将新插入的节点赋为红色，赋为红色的意义是确保插入该节点后，不会破坏该节点所在子树的黑高度，从而使破坏的性质只为其父节点为红色，保证只有这个性质被破坏了。
然后进行的是对红黑树被破坏性质的修补工作，首先我们知道的是只有在其父节点为红色时，红黑树性质才有被破坏的可能性，而父节点为红色，那么爷爷节点只可能为黑色，不确定的是父节点的兄弟节点（我把它叫做叔叔节点）的颜色，以及插入子节点（我把它叫做孙子节点）的位置（是父节点的左子节点还是右子节点）。
我们现在使用分类讨论的思想：
情况 1：叔叔节点为红色，这样我们可以把爷爷节点的黑色传递给父亲节点和叔叔节点，这样修补了在孙子节点处发生的冲突，同时保持了爷爷节点处所在子树黑高度不变，然而爷爷节点变为红色，爷爷节点处可能与太爷爷节点处的红色发生冲突，问题转移到爷爷节点处。
在情况1中最后就是把问题进行了缩小，原先要处理孙子节点以上的红黑树冲突，现在只需要处理爷爷节点以上的冲突了。
情况2：叔叔节点为黑色，这时候我们首先要考虑孙子节点是父节点的左子节点还是右子节点，现在我们假设是右节点，这样我们对父节点进行一个左旋操作，这样父节点变为孙子节点，孙子节点变为父节点，实际上此时孙子节点为父节点的左子节点，该情况被我们转化为情况3.
在情况2中我们使用的思想是通过将一种情况转移为另一种情况，来减少情况。
情况3：叔叔节点为黑色，孙子节点为父节点左子节点，这时，我们把爷爷节点的黑色与父节点的红色调换，这样父节点所在子树黑高度比叔叔节点所在黑高度多1，我们对爷爷节点使用一个右旋操作，这样父节点黑高度减1，叔叔节点黑高度不变，红黑性质修复完成。
这里只是举了红黑树插入操作的例子来说明算法证明，实际上算法导论中大部分算法都可以用这几个简单的想法（分类讨论，情况转移，数学归纳证明）进行解释和证明。
标签：
原文地址：http://www.cnblogs.com/zhangfann/p/4355389.html
