循环不变式

循环不变式(Loop Invariant) 是非常基础的一个概念，它是计算机科学中用于证明循环正确性的一种重要逻辑工具。是指在循环的每次迭代前后都保持为真的性质或条件，帮助验证循环的行为是否符合预期。

定义

循环不变式是在循环开始前、每次迭代后以及循环结束后均成立的逻辑断言。它反映了循环中变量的内在关系，与循环的终止条件共同保证程序的正确性。

性质

循环不变式有以下三条必须要满足的性质，这三条需要我们通过数学方法证明:

初始化(Initialization):循环开始前，不变式因变量初始值而成立。
保持(Maintenance):若某次迭代前不变式成立，则执行循环体后仍成立。
终止(Termination):循环结束时，不变式+终止条件共同推出目标结果。

这个定义非常漂亮，但还有更好理解的版本(《算法导论》原始版本的修改):

初始化: 循环开始前，不变式成立。
保持: 在某次迭代开始之前它成立，则迭代之后仍成立。
终止: 循环结束后，不变式提供一个性质来证明算法正确性。

解释

上面的这些内容比较抽象，但我们以代码为例就可以看出它们在讲什么:

// 典型: 数组求和
fn sum(arr: &[usize]) -> usize {
    let mut total = 0;
    let mut i = 0;
    while i < arr.len() {
        total += arr[i];
        i += 1;
    }
    total
}

让我们分析这个函数是否满足循环不变式，并进行证明。给定的循环不变式有两个:

total = arr + arr + ... + arr[i-1]
i <= arr.len()

证明

我们需要证明:

初始化: 在循环开始前，不变式成立。
保持: 如果在某次迭代前不变式成立，那么在下一次迭代前仍然成立。
终止: 循环终止时，不变式能推出算法的正确性。

1. 初始化

在循环开始前:

total = 0
i = 0
total = arr + ... + arr[i-1] 是空和(因为 i-1 = -1)，空和为 0，所以 total = 因为 i-1 = -10 满足。
i = 0 <= arr.len() 也成立。

2. 保持

假设在某次迭代前:

total = arr + ... + arr[i-1]
i <= arr.len()

执行循环体:

total += arr[i] ⇒ total = arr + ... + arr[i]
i += 1 ⇒ i 变为 i+1

此时:

total = arr + ... + arr[(i+1)-1] (因为 i 是更新后的值)，所以不变式仍然成立。
i <= arr.len(): 因为循环条件是 i < arr.len()，所以更新后的 i 满足 i <= arr.len()。

3. 终止

循环终止时:

i == arr.len() (因为循环条件是 i < arr.len()，且 i 每次增加 1)
此时 total = arr + ... + arr[i-1] = arr + ... + arr[arr.len()-1]，即整个数组的和。

因此，循环终止时 total 的值确实是数组所有元素的和，算法正确。

体会

可以发现，循环不变式是循环中始终保持为真的逻辑断言，它的三个特征都保证了它在循环前循环中循环后始终为真。

在设计算法时，循环不变式应满足以下要求:

1. 与算法目标相关

不变式应该直接或间接地描述算法的最终目标。

2. 足够强，能证明正确性

不变式不能太弱，否则无法保证算法的正确性。

例如:如果不变式仅仅是 i <= arr.len()，它不能直接证明 total 是正确的和。

3. 可验证

不变式必须能在循环的初始化、保持、终止三个阶段被严格证明。

可以发现: 这些证明与数学归纳法类似，但不同于归纳法，它可以终止，且必须证明终止阶段。

总的来说，设置循环不变式的步骤是:

明确算法目标。
设计一个与目标相关的不变式。
验证初始化、保持、终止。

循环不变式是算法正确性的重要工具，合理使用它可以提高代码的可读性和可靠性。

深化

我们以上一期习题来尝试给出循环不变式并证明。

pub fn realize5<T: PartialEq>(arr: &[T], v: T) -> Option<usize> {
    for i in 0..arr.len() {
        if v == arr[i] {
            return Some(i);
        }
    }
    None
}

对于上一个代码，我们尝试给出这样的一个不变式:

在每次循环开始时，v 不在arr[0..i]中，并且 i < arr.len()

证明

初始化

循环开始时，i = 0，arr[0..i] 是空数组(arr[0..0] 不包含任何元素，你需要注意a..b的左闭右开原则)。

不变式成立: v 不在空数组中且i < arr.len()。

保持

假设在某次循环开始时，v 不在 arr[0..i] 中。

执行循环体:

检查 arr[i] == v:
- 如果 arr[i] == v，则直接返回 Some(i) (此时 v 首次出现在 arr[i]，同样注意左闭右开原则，虽然 v 出现在 arr[i] 中，但并不出现在 arr[0..i]，所以是符合循环不变式的)。
- 如果 arr[i] != v，则 v 仍然不在 arr[0..i+1] 中 (因为 v不在arr[0..i]且arr[i] != v)。
循环结束时，i增加 1，不变式仍然成立。

终止

循环结束后有两种情况:

提前返回 Some(i):
- 此时 v 出现在 arr[i]，符合不变式。
循环全部执行完毕并返回 None:
- 此时 i = arr.len() - 1，且 v 不在 arr[0..arr.len()] 中。
- 由于循环已经检查了所有元素，但 v 仍然未被找到，因此 v 不在整个数组中，返回 None 是正确的。

练习与回答

考虑为上一期的主问题实现，给出一个循环不变式并证明。

设计

我们需要为 外层循环 和 内层循环 分别设计循环不变式。

外层循环的不变式

在每次外层循环开始时，arr[0..i] 是已排序的。(即前 i 个元素已经排好序)

内层循环的不变式

在每次内层循环开始时，arr[j..i] 的所有元素都大于 arr[j-1]，并且 arr[0..i] 除了 arr[j] 外仍然有序。(即 arr[j] 正在被插入到正确的位置，其余部分仍然有序)

证明

外层循环不变式的证明

初始化:
- 当 i = 1 时，arr[0..1] 只有 1 个元素，自然是有序的。
- 成立。
保持:
- 假设 arr[0..i] 是有序的。
- 内层循环会将 arr[i] 插入到 arr[0..i] 的正确位置，使得 arr[0..i+1] 有序。
- 成立。
终止:
- 当 i == arr.len() 时，arr[0..arr.len()] 是整个数组，并且已经有序。
- 成立。

内层循环不变式的证明

初始化:
- 内层循环开始时，j = i，arr[j..i] 是空区间(j == i)，所以 arr[j..i] 的所有元素(无)都大于 arr[j-1]。
- arr[0..i] 除了 arr[j] 外有序(因为外层循环不变式保证 arr[0..i] 有序)。
- 成立。
保持:
- 如果 arr[j] < arr[j-1]，则交换它们，此时:
- arr[j] 的新值是原来的 arr[j-1]，而 arr[j-1] 的新值是原来的 arr[j]。
- 由于 arr[0..i] 原本有序(除了 arr[j])，交换后 arr[j-1] 仍然比左边的元素大(否则不会继续循环)。
- 成立。
终止:
- 内层循环终止时，j == 0 或 arr[j] >= arr[j-1]。
- 此时 arr[j] 已经插入到正确的位置，arr[0..i+1] 有序。
- 成立。

代码的正确性

外层循环保证每次迭代后 arr[0..i] 有序。
内层循环保证 arr[j] 被正确插入到 arr[0..i] 的合适位置。
最终，整个数组 arr 被排序。

注: 上面的内容与《算法导论》有所不同，但尽量减少了术语的使用，理解难度更低。使得你能看懂代码，就基本能看懂证明。

Keyboard shortcuts

算法学习