下载掌阅APP，畅读海量书库
立即打开
对于线性查找的3个算法，我们能很容易地看到每个算法均能生成正确的结果。但是有时候生成正确的结果看起来有点难。这涉及一系列技术，在这里不能一一讲解。
证明正确性的一个常用方法是使用 循环不变式 证明：即证明循环的每次迭代之前循环不变式为真。循环不变式能够帮助我们证明正确性，关于循环不变式，我们必须证明以下3条性质。
初始化： 循环的第一次迭代之前，它为真。
保持： 如果循环的每次迭代之前它为真，那么下次迭代之前它仍为真。
终止： 循环终止时，当它确实终止时，伴随循环终止的原因，循环不变式为我们提供了一个有用的性质。
以BETTER-LINEAR-SEARCH算法为例，以下是一个循环不变式：
在第 1 步迭代开始时 ， 如果数组 A 中存在 x ， 那么 x 一定在 A [ i ]～ A [ n ] 的 子数组 （ 数组的一段连续部分 ） 中 。
我们甚至不需要循环不变式来证明如果程序返回了一个索引而非NOT-FOUND，则被返回的索引是正确的：在第1A步中该程序能返回索引 i 的唯一方式是因为 x 等于 A [ i ]。下面，我们使用循环不变式来证明如果程序是在第2步中返回NOT-FOUND，那么数组中一定不包含 x 。
初始化： 初始时， i =1，因此循环不变式的子数组是 A [1]～ A [ n ]，此时代表整个数组。
保持： 假定当前循环变量是 i ，在迭代开始时，如果数组 A 中包含 x ，那么它一定在从 A [ i ]到 A [ n ]的子数组中。如果执行这次循环迭代而没有返回值，我们能得出 A [ i ]≠ x ，因此能确定地说如果 x 在数组 A 内，那么它一定出现在 A [ i +1]～ A [ n ]的子数组内。因为 i 在下次迭代之前会自增1，所以循环不变式在下次迭代之前仍为真。
终止： 循环一定会终止，或者因为程序会在第1A步返回，或者由于 i > n 。我们已经对程序因在第1A步返回而导致循环终止的情况进行了验证。
为了处理因 i > n 而导致循环终止的情况，我们依据循环不变式的等价性来证明。命题“如果 A 那么 B ”的 逆否命题 是“如果非 B 那么非 A ”。一个命题为真当且仅当与它等价的命题也为真。该循环不变式的等价命题为“如果 x 没有出现在 A [ i ]～ A [ n ]的子数组中，那么数组 A 中就不存在 x ”。
现在，当 i > n 时， A [ i ]～ A [ n ]这个子数组为空。因此这个子数组中不可能包含 x 。因此，根据循环不变式的等价式， x 不可能出现在数组 A 的任意位置上，因此第2步中返回NOT-FOUND是恰当的。
这一系列的推理仅仅是为了说明这么一个简单的循环？每次写一个循环时，我们都必须添加上述证明吗？我不会，但是针对每一个简单的循环，依旧有几个计算机科学家坚持这样严格的推理。在实际编程时，我发现在我写一个循环的大部分时间里，我会在头脑里想出循环不变式。它可能深藏在我的头脑中以至于我甚至没有意识到我的大脑里会存在该循环不变式，但是如果要求我必须陈述该循环不变式，我能够完整地将其表述下来。虽然我们中的大多数人认为循环不变式对于理解像BETTER-LINEAR-SEARCH这样的简单循环没有必要，但是我们想要理解复杂的循环能够执行正确的操作时使用循环不变式会很方便。