5.2 正确性与循环不变量

第 5.1 节教会了我们书写和追踪算法。一次成功追踪只能证明一个输入运行正常，而算法规格通常提出全称命题：

\text{对每个允许输入，算法都会终止并产生要求的输出。}

第 3 章已经提供了全称证明与反例方法。现在我们把这些方法用于程序。

前置条件与后置条件定义承诺

前置条件说明算法开始前必须满足什么。后置条件说明算法结束时必须满足什么。

考虑：

text

DIVIDE-SUM(a, b, n)
    return (a + b) / n

必要的前置条件是 $n\ne0$ 。一种完整规格可以写成：

前置条件： $a,b,n\in\mathbb R$ 且 $n\ne0$ ；

后置条件：返回值等于 $(a+b)/n$ 。

如果输入违反前置条件，除非规格另外说明处理方式，否则算法没有义务给出有意义的行为。

对于求和算法

text

SUM-TO(n)
    total ← 0
    for i ← 1 to n
        total ← total + i
    return total

可以规定：

前置条件： $n$ 是非负整数；

后置条件：

total=\sum_{j=1}^{n}j=\frac{n(n+1)}{2}.

求和符号中的下标 $j$ 是局部数学名称。我们不用 $i$ ，是为了避免把整个求和与算法中不断变化的循环变量混淆。

部分正确与完全正确

“算法正确”实际上包含两项任务。

部分正确性表示：

\text{如果算法终止，那么输出满足后置条件。}

终止性表示：

\text{对每个满足前置条件的输入，算法都在有限步后结束。}

完全正确性把二者结合：

\text{完全正确性} = \text{部分正确性} + \text{终止性}.

一个无限循环可能在形式上满足部分正确性，因为它从未返回错误答案——它根本不返回。因此必须单独证明终止。

为什么循环需要新的证明思想

if 语句只有有限条分支，可以逐情况证明。循环的执行次数可能随输入变化，因此需要一个能描述每次迭代的命题。

循环不变量是一个在以下时刻都为真的命题：

1. 第一次迭代之前；

2. 每次完成迭代之后；

3. 因而在循环停止时仍然为真。

“不变量”表示即使变量值不断改变，这个命题仍保持成立。

不变量不一定就是最终后置条件。它通常描述已经完成的进度以及剩余工作。

为求和循环发现不变量

回到：

text

total ← 0
for i ← 1 to n
    total ← total + i
return total

在当前值为 $i$ 的迭代开始前，算法已经加入了

1,2,\ldots,i-1.

一个有用不变量是

total=\sum_{j=1}^{i-1}j.

下面用三项义务证明它。

1. 初始化

第一次迭代前， $i=1$ 且 $total=0$ 。从 $1$ 到 $0$ 没有待加项，这种空和定义为 $0$ 。因此

total=0=\sum_{j=1}^{0}j.

不变量在循环开始前成立。

2. 保持

假设在某个任意的 $i$ 迭代前，不变量成立：

total=\sum_{j=1}^{i-1}j.

循环体执行

total\leftarrow total+i.

更新后，

total =\sum_{j=1}^{i-1}j+i =\sum_{j=1}^{i}j.

随后循环变量前进到 $i+1$ 。使用新的循环值重写，就得到

total=\sum_{j=1}^{(i+1)-1}j.

因此，如果不变量在本次迭代前为真，它在下一次迭代前仍为真。

3. 与终止状态连接

完成最后一次 $i=n$ 的迭代后，循环变量已经越过 $n$ 。不变量告诉我们

total=\sum_{j=1}^{n}j,

这正是后置条件。

整个证明模式为：

\boxed{\text{初始化}} \longrightarrow \boxed{\text{保持}} \longrightarrow \boxed{\text{退出时推出后置条件}}.

它与第 3 章的数学归纳法相似：初始化对应基础情形，保持对应对循环次数的归纳步骤。

正在加载交互实验...

逐次推进求和机器，并在多个候选不变量中做出选择。只有断言与每个可见状态都匹配时，力场才会稳定；错误不变量会在第一个反例处破裂，而退出状态还必须能够解锁后置条件。

正在加载概念检查...

正在加载本节练习...

用递减度量证明终止

对 while 循环，可以寻找一个每次迭代都严格减小的非负整数数量。它常称为变式或秩函数。

考虑对正整数 $a,b$ 使用的欧几里得反复减法过程：

text

while a ≠ b
    if a > b
        a ← a - b
    else
        b ← b - a
return a

当 $a\ne b$ 时，两个值都保持为正。度量

V=a+b

是正整数。每次迭代都从较大值中减去一个正的较小值，因此 $V$ 会严格减少。

正整数的严格递减序列不可能无限持续，所以循环终止。

正确使用终止度量时要证明：

1. 它属于不存在无限严格递减链的集合，例如非负整数；

2. 每次继续循环的迭代都会让它减小；

3. 它不可能永远减小而不进入退出状态。

如果变量可能变成负数或来回振荡，只说“变量越来越小”并不充分。

线性搜索的正确性

假设数组

A[0],A[1],\ldots,A[n-1]

含有 $n$ 个元素。记号 $A[i]$ 表示索引 $i$ 处存储的元素。索引从 $0$ 开始，到 $n-1$ 结束。

目标是返回一个存放目标值 $t$ 的索引；如果 $t$ 不存在，就返回 $-1$ 。

text

LINEAR-SEARCH(A, t)
    for i ← 0 to length(A) - 1
        if A[i] = t
            return i
    return -1

一个有用循环不变量是：

> 在检查索引 $i$ 之前，目标值没有出现在索引 $0,1,\ldots,i-1$ 中。

初始化

在 $i=0$ 之前，没有更早的索引。关于空前缀的命题为真。

保持

如果 $A[i]\ne t$ ，那么检查索引 $i$ 后，目标不在索引 $0$ 到 $i$ 中。不变量已经为下一个值 $i+1$ 准备好。

如果 $A[i]=t$ ，算法返回 $i$ ，输出正确。

退出

如果循环结束仍未返回，说明每个有效索引都已检查并且不等于 $t$ 。此时返回 $-1$ 正确。

终止

for 循环最多检查 $n$ 个索引，所以一定终止。

这些论证合在一起证明了完全正确性。

测试发现错误，证明排除全部错误

测试与证明承担不同任务。

一个通过的测试说明某个所选输入运行正确；

一个失败测试就是反例，它证明实现不正确；

一个证明则建立对所有满足前置条件输入的正确性。

小输入和边界输入特别容易暴露错误：

空数组；

长度为 $1$ 的数组；

目标位于第一个或最后一个索引；

目标不存在；

目标重复出现。

考虑下面的错误搜索：

text

for i ← 0 to length(A) - 2
    if A[i] = t
        return i
return -1

它从不检查最后一个索引。输入

A=[4,7,9],\qquad t=9

就是反例：目标位于索引 $2$ ，算法却返回 $-1$ 。

其他错误可能越界读取数组，或者不推进索引，从而造成无效访问或不终止。好的对抗测试应当有意触发被怀疑的弱点。

正在加载交互实验...

调查多个“几乎正确”的搜索代理。构造对抗数组，运行动态执行，并捕获四类故障之一：错误答案、遗漏边界、无效访问或不终止。随后修补负责的代码行，并在同一个反例上重新运行。

正在加载概念检查...

正在加载本节练习...

注意

不变量必须在初始化时成立，并被每次迭代保持。一个只在循环退出时成立的命题可能是后置条件，但它不会自动成为有用不变量。

本节衔接

正确性关心算法是否返回正确答案并终止。但两个都正确的算法，工作量可能差别巨大。第 5.3 节将建立代价模型，计算操作次数怎样随输入规模增长，并在不受具体机器速度干扰的情况下比较增长率。

5.2 正确性与循环不变量

第 5.1 节教会了我们书写和追踪算法。一次成功追踪只能证明一个输入运行正常，而算法规格通常提出全称命题：

\text{对每个允许输入，算法都会终止并产生要求的输出。}

第 3 章已经提供了全称证明与反例方法。现在我们把这些方法用于程序。

前置条件与后置条件定义承诺

前置条件说明算法开始前必须满足什么。后置条件说明算法结束时必须满足什么。

考虑：

text

DIVIDE-SUM(a, b, n)
    return (a + b) / n

必要的前置条件是 $n\ne0$ 。一种完整规格可以写成：

前置条件： $a,b,n\in\mathbb R$ 且 $n\ne0$ ；

后置条件：返回值等于 $(a+b)/n$ 。

如果输入违反前置条件，除非规格另外说明处理方式，否则算法没有义务给出有意义的行为。

对于求和算法

text

SUM-TO(n)
    total ← 0
    for i ← 1 to n
        total ← total + i
    return total

可以规定：

前置条件： $n$ 是非负整数；

后置条件：

total=\sum_{j=1}^{n}j=\frac{n(n+1)}{2}.

求和符号中的下标 $j$ 是局部数学名称。我们不用 $i$ ，是为了避免把整个求和与算法中不断变化的循环变量混淆。

部分正确与完全正确

“算法正确”实际上包含两项任务。

部分正确性表示：

\text{如果算法终止，那么输出满足后置条件。}

终止性表示：

\text{对每个满足前置条件的输入，算法都在有限步后结束。}

完全正确性把二者结合：

\text{完全正确性} = \text{部分正确性} + \text{终止性}.

一个无限循环可能在形式上满足部分正确性，因为它从未返回错误答案——它根本不返回。因此必须单独证明终止。

为什么循环需要新的证明思想

if 语句只有有限条分支，可以逐情况证明。循环的执行次数可能随输入变化，因此需要一个能描述每次迭代的命题。

循环不变量是一个在以下时刻都为真的命题：

1. 第一次迭代之前；

2. 每次完成迭代之后；

3. 因而在循环停止时仍然为真。

“不变量”表示即使变量值不断改变，这个命题仍保持成立。

不变量不一定就是最终后置条件。它通常描述已经完成的进度以及剩余工作。

为求和循环发现不变量

回到：

text

total ← 0
for i ← 1 to n
    total ← total + i
return total

在当前值为 $i$ 的迭代开始前，算法已经加入了

1,2,\ldots,i-1.

一个有用不变量是

total=\sum_{j=1}^{i-1}j.

下面用三项义务证明它。

1. 初始化

第一次迭代前， $i=1$ 且 $total=0$ 。从 $1$ 到 $0$ 没有待加项，这种空和定义为 $0$ 。因此

total=0=\sum_{j=1}^{0}j.

不变量在循环开始前成立。

2. 保持

假设在某个任意的 $i$ 迭代前，不变量成立：

total=\sum_{j=1}^{i-1}j.

循环体执行

total\leftarrow total+i.

更新后，

total =\sum_{j=1}^{i-1}j+i =\sum_{j=1}^{i}j.

随后循环变量前进到 $i+1$ 。使用新的循环值重写，就得到

total=\sum_{j=1}^{(i+1)-1}j.

因此，如果不变量在本次迭代前为真，它在下一次迭代前仍为真。

3. 与终止状态连接

完成最后一次 $i=n$ 的迭代后，循环变量已经越过 $n$ 。不变量告诉我们

total=\sum_{j=1}^{n}j,

这正是后置条件。

整个证明模式为：

\boxed{\text{初始化}} \longrightarrow \boxed{\text{保持}} \longrightarrow \boxed{\text{退出时推出后置条件}}.

它与第 3 章的数学归纳法相似：初始化对应基础情形，保持对应对循环次数的归纳步骤。

正在加载交互实验...

正在加载概念检查...

正在加载本节练习...

用递减度量证明终止

对 while 循环，可以寻找一个每次迭代都严格减小的非负整数数量。它常称为变式或秩函数。

考虑对正整数 $a,b$ 使用的欧几里得反复减法过程：

text

while a ≠ b
    if a > b
        a ← a - b
    else
        b ← b - a
return a

当 $a\ne b$ 时，两个值都保持为正。度量

V=a+b

是正整数。每次迭代都从较大值中减去一个正的较小值，因此 $V$ 会严格减少。

正整数的严格递减序列不可能无限持续，所以循环终止。

正确使用终止度量时要证明：

1. 它属于不存在无限严格递减链的集合，例如非负整数；

2. 每次继续循环的迭代都会让它减小；

3. 它不可能永远减小而不进入退出状态。

如果变量可能变成负数或来回振荡，只说“变量越来越小”并不充分。

线性搜索的正确性

假设数组

A[0],A[1],\ldots,A[n-1]

含有 $n$ 个元素。记号 $A[i]$ 表示索引 $i$ 处存储的元素。索引从 $0$ 开始，到 $n-1$ 结束。

目标是返回一个存放目标值 $t$ 的索引；如果 $t$ 不存在，就返回 $-1$ 。

text

LINEAR-SEARCH(A, t)
    for i ← 0 to length(A) - 1
        if A[i] = t
            return i
    return -1

一个有用循环不变量是：

> 在检查索引 $i$ 之前，目标值没有出现在索引 $0,1,\ldots,i-1$ 中。

初始化

在 $i=0$ 之前，没有更早的索引。关于空前缀的命题为真。

保持

如果 $A[i]\ne t$ ，那么检查索引 $i$ 后，目标不在索引 $0$ 到 $i$ 中。不变量已经为下一个值 $i+1$ 准备好。

如果 $A[i]=t$ ，算法返回 $i$ ，输出正确。

退出

如果循环结束仍未返回，说明每个有效索引都已检查并且不等于 $t$ 。此时返回 $-1$ 正确。

终止

for 循环最多检查 $n$ 个索引，所以一定终止。

这些论证合在一起证明了完全正确性。

测试发现错误，证明排除全部错误

测试与证明承担不同任务。

一个通过的测试说明某个所选输入运行正确；

一个失败测试就是反例，它证明实现不正确；

一个证明则建立对所有满足前置条件输入的正确性。

小输入和边界输入特别容易暴露错误：

空数组；

长度为 $1$ 的数组；

目标位于第一个或最后一个索引；

目标不存在；

目标重复出现。

考虑下面的错误搜索：

text

for i ← 0 to length(A) - 2
    if A[i] = t
        return i
return -1

它从不检查最后一个索引。输入

A=[4,7,9],\qquad t=9

就是反例：目标位于索引 $2$ ，算法却返回 $-1$ 。

其他错误可能越界读取数组，或者不推进索引，从而造成无效访问或不终止。好的对抗测试应当有意触发被怀疑的弱点。

正在加载交互实验...

正在加载概念检查...

正在加载本节练习...

注意

不变量必须在初始化时成立，并被每次迭代保持。一个只在循环退出时成立的命题可能是后置条件，但它不会自动成为有用不变量。

5.2 正确性与不变量

5.2 正确性与循环不变量

前置条件与后置条件定义承诺

部分正确与完全正确

为什么循环需要新的证明思想

为求和循环发现不变量

1. 初始化

2. 保持

3. 与终止状态连接

用递减度量证明终止

线性搜索的正确性

初始化

保持

退出

终止

测试发现错误，证明排除全部错误

本节衔接

5.2 正确性与不变量

5.2 正确性与循环不变量

前置条件与后置条件定义承诺

部分正确与完全正确

为什么循环需要新的证明思想

为求和循环发现不变量

1. 初始化

2. 保持

3. 与终止状态连接

用递减度量证明终止

线性搜索的正确性

初始化

保持

退出

终止

测试发现错误，证明排除全部错误

本节衔接