讨厌算法的程序员 2 - 证明算法的正确性

本文主要是介绍讨厌算法的程序员 2 - 证明算法的正确性，希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！

讨厌算法的程序员系列入口

第1篇介绍了插入排序算法，这里要提出一个问题：学习算法仅仅是积累一个又一个的算法实现吗？

当然不是。比算法本身更重要也更基础的，是对算法的分析：能够证明其正确性，能够理解其效率。这也是自行设计新算法的基础。如果学了一堆算法的实现，而不能判断算法的优劣，或者靠死记硬背记住了各个算法的复杂度等性能指标，那么随着时间的流逝，这一切都是要还给课本的。

算法的正确性

正确性

当我们设计或者实现完成一个算法后，如何证明它是正确的呢？

对于程序员来说，司空见惯的做法是，我们会找几个测试用例，也就是事先定义好的输入输出，然后把输入送进程序里跑一下。如果算法能自动结束，且输出和预期一致，我们就认为算法是ok的。

可是我们无法穷举输入，如何能确定未来的某一输入就一定会有正确的输出呢？靠测试用例是无法保障算法的正确性的。

循环不变式

下面介绍能够证明算法正确性的“循环不变式”。

它的英文名是loop invariant，就是正确的算法在循环的各个阶段，总是存在一个固定不变的特性。找出这个特性并证明其固定不变，从而推断出算法是正确的。

具体的说，必须证明循环不变式满足下面三个性质：

初始化：循环的第一次迭代之前，不变式为真；
保持：循环的某次迭代之前不变式为真，下次迭代之前其仍然为真；
终止：循环终止时，不变式依然成立。

这个过程类似于数学归纳法，为了证明某条性质成立，需要证明一个基本情况和一个归纳步。第一步“初始化”可以对应“基本情况”，第二步“保持”对应于“归纳步”。而第三步“终止”也许是最重要的，因为我们将用终止时循环不变式来证明算法的正确性。

这里定义循环不变式的窍门就是：结合导致循环终止的条件一起定义循环不变式。

证明插入排序的正确性

利用上一节的“循环不变式”，我们证明第1篇中介绍的插入排序的正确性。

对于插入排序，一开始我们就注意到其在玩扑克牌中的应用，这里面有一个关键的认知：我们手中已经摸到的牌始终是排好序的，也就是我们找到的循环不变式：A[1 ‥ j-1]在循环的三个阶段均为有序。无论在循环前，循环中，还是循环后，它都是不变的。

INSERTION-SORT(A)
1 for j = 2 to A.length
2   key = A[j]
3   // Insert A[j] into the sorted sequence A[1..j-1].
4   i = j - 1
5   while i > 0 and A[i] > key
6       A[i + 1] = A[i]
7       i = i - 1
8   A[i + 1] = key

插入排序

证明如下：

初始化：首先证明在第一次循环迭代之前（当j = 2时），循环不变式成立。此时，A[1 ‥ j-1]中仅由一个元素A[1]组成，“有序性”当然是成立的。从上图中(a)中，有序数组中只有5一个元素；
保持：其次处理第二条性质：证明每次迭代保持循环不变式。在循环的每次迭代过程中，A[1 ‥ j-1]的“有序性”仍然保持。上图中所有的黑色块左侧子数组永远都是有序的；
终止：最后研究在循环终止时发生了什么。导致外层for循环终止的条件是j > A.length=n，此时j = n + 1。在循环不变式的表述中将j用n+1代替，那么A[1 ‥ j-1]的“有序性”，就是A[1 ‥ n]有序，这就证明了最终的整个数组是排序好的。上图中(f)表明整个数组已经排好序。

以后，我们还会用到循环不变式来证明其他算法的正确性。