循环不变式

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

定义

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

性质

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

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

这个定义非常漂亮, 但还有更好理解的版本:

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

解释

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

#![allow(unused)]
fn main() {
// 典型: 数组求和
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. 可验证

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

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

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

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

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

深化

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

#![allow(unused)]
fn main() {
pub fn linear_search<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 被排序.

Note

上面的内容与《算法导论》有所不同, 但尽量减少了术语的使用, 理解难度更低.

Keyboard shortcuts

算法学习