2.3 循环不变式
对于线性查找的3个算法，我们能很容易地看到每个算法均能生成正确的结果。但是有时候生成正确的结果看起来有点难。这涉及一系列技术，在这里不能一一讲解。
证明正确性的一个常用方法是使用循环不变式证明：即证明循环的每次迭代之前循环不变式为真。循环不变式能够帮助我们证明正确性，关于循环不变式，我们必须证明以下3条性质。
初始化：循环的第一次迭代之前，它为真。
保持：如果循环的每次迭代之前它为真，那么下次迭代之前它仍为真。
终止：循环终止时，当它确实终止时，伴随循环终止的原因，循环不变式为我们提供了一个有用的性质。以BETTERLINEARSEARCH算法为例，以下是一个循环不变式：
在第1步迭代开始时，如果数组A中存在x，那么x一定在A［i］～A［n］的子数组（数组的一段连续部分）中。我们甚至不需要循环不变式来证明如果程序返回了一个索引而非NOTFOUND，则被返回的索引是正确的：在第1A步中该程序能返回索引i的唯一方式是因为x等于A［i］。下面，我们使用循环不变式来证明如果程序是在第2步中返回NOTFOUND，那么数组中一定不包含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，21所以循环不变式在下次迭代之前仍为真。终止：循环一定会终止，或者因为程序会在第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步中返回NOTFOUND是恰当的。这一系列的推理仅仅是为了说明这么一个简单的循环？每次写一个循环时，我们都必须添加上述证明吗？我不会，但是针对每一个简单的循环，依旧有几个计算机科学家坚持这样严格的推理。在实际编程时，我发现在我写一个循环的大部分时间里，我会在头脑里想出循环不变式。它可能深藏在我的头脑中以至于我甚至没有意识到我的大脑里会存在该循环不变式，但是如果要求我必须陈述该循环不变式，我能够完整地将其表述下来。虽然我们中的大多数人认为循环不变式对于理解像BETTERLINEARSEARCH这样的简单循环没有必要，但是我们想要理解复杂的循环能够执行正确的操作时使用循环不变式会很方便。