使用循环不变式证明算法的正确性，常用于分析带有循环的算法。这种方法的核心是通过构造一个在循环执行过程中始终成立的性质（即循环不变式），来证明算法在结束时能够正确地解决问题。
使用循环不变式方法。我们需要定义一个不变式，并通过三个步骤（初始化、保持性、终止性）证明算法在任何输入下都能正确地运行。
定义循环不变式：
找出一个性质，它在每次进入循环迭代时都应为真。这一性质通常与算法的部分正确性（partial correctness）相关。
验证循环不变式：
- 初始化：证明循环的第一次循环迭代之前，循环不变式成立
- 保持：假设循环不变式在循环的某次迭代之前成立，证明在这一迭代结束后（下次迭代之前）它仍然成立
- 终止：在循环终止时，结合循环不变式和终止条件，证明算法达到了预期的正确结果。
例子
数组求和算法的正确性 CLRS 2.1-2
题目
Consider the procedure SUM-ARRAY on the facing page. It computes the sum of the n numbers in array A[1 : n]. State a loop invariant for this procedure, and use its initialization, maintenance, and termination properties to show that the SUM-ARRAY procedure returns the sum of the numbers in A[1 : n].
考虑对面页的过程 SUM-ARRAY。它用于计算数组 A[1 : n] 中 n 个数的总和。为该过程陈述一个循环不变式，并利用循环不变式的初始化、保持和终止性质，证明 SUM-ARRAY 过程返回的是 A[1 : n] 中数的总和。
伪代码
SUM-ARRAY(A, n)
sum = 0
for i = 1 to n
sum = sum + A[i]
return sum
输入：数组 A 和 正整数 n（表示数组的元素个数）
输出：数组前 n 个元素的总和，即 $$ \sum_{i=1}^{n} A[i] $$
证明
循环不变式：在循环的每次迭代开始时，变量 sum 的值等于数组前 i - 1 个元素的总和，即：
验证循环不变式：
初始化：首先证明在第一次循环迭代之前（当 i = 1 时），循环不变式成立。
在循环的第一次迭代之前，i = 1，此时 sum 被初始化为 0，而数组前 i - 1 = 0 个元素的总和也是 0。因此，循环不变式成立。
保持性：证明每次迭代保持循环不变式。
假设在某次迭代开始时，循环不变式成立，即 。
在这一迭代中，代码执行 sum = sum + A[j]。
更新后，sum 的值变为：
此时，变量 sum 等于数组前 i 个元素的总和。
下一次迭代开始时，i 增加1，循环不变式依然成立。
终止性：结合循环不变式和终止条件，证明算法达到了预期的正确结果。
当循环终止时，i = n + 1，此时变量 sum 包含了数组前 n 个元素的总和：
算法返回 sum，其值等于 ，是问题的正确结果。
总结：
- 部分正确性：循环不变式确保在每次迭代中，sum始终等于数组已处理部分的元素和。
- 终止性：当循环终止时，sum 包含数组前 n 个元素的总和，算法返回正确值。
因此，伪代码是正确的。
线性查找算法的正确性 CLRS 2.1-4
题目
Consider the searching problem:
Input: A sequence of n numbers <a1, a2, … , an> stored in array A[1 : n] and a value x.
Output: An index i such that x equals A[i] or the special value NIL if x does not appear in A.
Write pseudocode for linear search, which scans through the array from beginning to end, looking for x. Using a loop invariant, prove that your algorithm is correct. Make sure that your loop invariant fulfills the three necessary properties.
考虑以下查找问题：
输入：n 个数的一个序列 A = <a_1, a_2, ..., a_n> 和一个值 x。
输出：下标 i 使得 x = A[i] 或者当 v 不在 A 中出现时，x为特殊值 NIL。
写出线性查找的伪代码，它扫描整个序列来查找 x。使用一个循环不变式来证明你的算法是正确的。确保你的循环不变式满足三条必要的性质。
伪代码
// 线性查找的伪代码
LINEAR_SEARCH(A, x):
for i = 1 to A.length
if A[i] == x
return i
return NIL
// 输入：一个数组 A 和一个值 x。
// 输出：如果 x 存在于 A 中，返回其第一个匹配元素的索引；否则，返回 NIL。
证明
循环不变式：在循环的每次迭代开始时，在数组 A 的前 i - 1 个元素中，若 x 存在，则其索引已经被找到并返回；否则，x 不在前 i - 1 个元素中。
初始化：首先证明在第一次循环迭代之前（当 i = 1 时），循环不变式成立。
在第一次迭代之前（即 i = 1），算法还未检查任何元素，前 i - 1 = 0 个元素为空集。显然，空集中不存在 x，循环不变式成立。
保持性：证明每次迭代保持循环不变式。
假设在某次迭代开始时，循环不变式成立，即前 i - 1 个元素已经被正确检查。在本次迭代结束后：
- 如果
A[i] == x，算法立即返回 i，说明找到了 x 的索引，算法正确结束。 - 如果
A[i] != x，则说明 x 不在第 i 个元素处，算法进入下一次迭代。在此时，前 i 个元素已经被正确检查，循环不变式仍然成立。
终止性：结合循环不变式和终止条件，证明算法达到了预期的正确结果。
循环终止有两种情况：
- 找到目标值 x：如果 x 存在于 A 中，算法会在某次迭代中返回其索引 i。根据“保持性”所述，此时 x 在 i 位置，且算法正确结束。
- 未找到目标值 x：如果 x 不存在于 A 中，算法会检查到 i = A.length + 1 时退出循环并返回 NIL。结合循环不变式，可以推断 x 不在数组 A 中，因此返回 NIL 是正确的。
总结：
通过循环不变式和终止性分析，线性查找算法的正确性得到证明。
- 若 x 存在于数组 A 中，算法能返回 x 的第一个匹配位置。
- 若 x 不存在于数组 A 中，算法正确返回 NIL。
因此，代码是正确的。
插入排序算法的正确性
伪代码
// 插入排序的伪代码
INSERTION-SORT(A):
for j = 2 to A.length
key = A[j]
// Insert A[j] into the sorted sequence A[1..j-1].
i = j - 1
while i > 0 and A[i] > key
A[i + 1] = A[i]
i = i - 1
A[i + 1] = key
// 输入：一个数组 A。
// 输出：按升序排列的数组 A。
证明
循环不变式：在每次主循环迭代开始时，子数组 A[1 .. j-1] 是已排序的，且包含数组 A[1 .. j - 1] 的原始元素。
初始化：首先证明在第一次循环迭代之前（当 j = 2 时），循环不变式成立。
当 j = 2 时，子数组 A[1.. j-1]，也就是 A[1 .. 1] 只有一个元素，实际上就是 A[1] 原来的元素，而且该子数组可以认为是有序的，因此它是平凡（trivially）有序的。循环不变式成立。
保持性：证明每次迭代保持循环不变式。
假设在第 j 次迭代开始时，子数组 A[1..j-1]是有序的。
- 目标：将元素 A[j] 插入到 A[1..j-1] 的正确位置，使得 A[1..j] 也有序。
- 在内层循环中，i 从 j - 1 开始递减，将比 key 大的元素依次向右移动，腾出插入 key 的位置。
- 当 i ⇐ 0 或 A[i] ⇐ key 时，算法退出循环并将 key 插入到正确位置 A[i + 1]。
- 插入完成后，子数组 A[1..j] 成为有序的。
因此，循环不变式在每次迭代中被保持。
终止性：结合循环不变式和终止条件，证明算法达到了预期的正确结果。
当主循环结束时，j = A.length + 1，子数组 A[1 .. j-1] 指的是整个数组 A[1 .. A.length]，整个数组经过完整的插入过程，根据循环不变式，此时它是有序的。
总结：
- 部分正确性：循环不变式保证了在每次迭代结束时，子数组 A[1 .. j-1] 是有序的。
- 终止性：当循环终止时，j = A.length + 1，整个数组 A 被完全排序。
因此，伪代码是正确的。
参考
- 《算法导论 2.1》