什么是循环不变量？

Question

我正在阅读 CLRS 的“算法简介”。在第 2 章中，作者提到了“循环不变量”。什么是循环不变量？

Answer 1

在这种情况下，不变量是指在每次循环迭代中的某个点必须为真的条件。

在契约编程中，不变量是在调用任何公共方法之前和之后必须为真（通过契约）的条件。

Answer 2

简单来说，循环不变量是对循环的每次迭代都成立的谓词（条件）。例如，让我们看一个简单的for 循环，如下所示：

int j = 9;
for(int i=0; i<10; i++)  
  j--;

在这个例子中，i + j == 9 是真的（对于每次迭代）。一个较弱的不变量也是正确的，即 i >= 0 && i <= 10.

Answer 3

我喜欢这个非常简单的定义：(source)

循环不变量是[在程序变量中]的条件，在循环的每次迭代之前和之后都必须立即为真。 （请注意，在迭代过程中，这并没有说明它的真假。）

就其本身而言，循环不变量并没有多大作用。然而，给定一个适当的不变量，它可以用来帮助证明算法的正确性。 CLRS 中的简单示例可能与排序有关。例如，让您的循环不变量类似于在循环开始时，对该数组的第一个 i 条目进行排序。如果你能证明这确实是一个循环不变量（即它在每次循环迭代之前和之后都成立），你可以用它来证明一个排序算法的正确性：在循环终止时，循环不变量仍然满足，而计数器i 是数组的长度。因此，第一个i 条目已排序意味着整个数组已排序。

一个更简单的例子：Loops Invariants, Correctness, and Program Derivation。

我理解循环不变量的方式是作为一种系统的、正式的工具来推理程序。我们做了一个我们专注于证明真实的声明，我们称之为循环不变量。这组织了我们的逻辑。虽然我们也可以非正式地争论某些算法的正确性，但使用循环不变量会迫使我们非常仔细地思考并确保我们的推理是无懈可击的。

Answer 4

应该注意的是，当考虑到表达变量之间重要关系的断言时，循环不变量可以帮助设计迭代算法，这些关系在每次迭代开始时和循环终止时都必须为真。如果这一点成立，则计算正在走向有效性。如果为 false，则算法失败。

Answer 5

除了所有好的答案之外，我想 Jeff Edmonds 的 How to Think About Algorithms 中的一个很好的例子可以很好地说明这个概念：

示例 1.2.1 “查找最大两指算法”

1) 规范：一个输入实例由一个列表 L(1..n) 组成 元素。输出由索引 i 组成，使得 L(i) 具有最大值 价值。如果有多个具有相同值的条目，则任何 其中一个被退回。

2) 基本步骤：您决定使用两指法。你的右手手指 在列表中运行。

3) 进度衡量标准：进度衡量标准是沿着 列出你的右手手指。

4) 循环不变量： 循环不变量表明您的左手指指向您迄今为止遇到的最大条目之一 右手手指。

5) 主要步骤：每次迭代，你的右手手指向下移动一个 列表中的条目。如果你的右手手指现在指向一个条目 比左手指的入口大，然后向左移动 手指与你的右手手指。

6) 取得进步：你取得进步是因为你的右手手指移动 一个条目。

7) 保持循环不变量： 你知道循环不变量的保持如下。对于每一步，新的左手指元素 是 Max（旧左指元素，新元素）。由循环不变量， 这是 Max(Max(shorter list), new element)。从数学上讲，这是 最大（更长的列表）。

8) 建立循环不变量：您最初通过将两个手指指向第一个元素来建立循环不变量。

9) 退出条件：当你的右手手指完成时你就完成了 遍历列表。

10) 结束：最后，我们知道问题解决如下。经过 退出条件，你的右手手指已经碰到了所有的 条目。通过循环不变量，您的左手指指向最大值 这些。返回此条目。

11) 终止和运行时间：所需的时间是恒定的 乘以列表的长度。

12) 特殊情况：检查有多个条目时会发生什么 具有相同的值或当 n = 0 或 n = 1 时。

13) 编码和实现细节：...

14) 形式证明：算法的正确性来自 以上步骤。

Answer 6

在处理循环和不变量时，许多人没有立即意识到一件事。他们在循环不变量和循环条件（控制循环终止的条件）之间感到困惑。

正如人们指出的那样，循环不变量必须为真

1. 循环开始之前
2. 循环的每次迭代之前
3. 循环结束后

（尽管在循环主体期间它可能暂时为假）。 另一方面，循环条件 必须在循环终止后为假，否则循环将永远不会终止。

因此循环不变量和循环条件必须是不同的条件。

复杂循环不变量的一个很好的例子是二分搜索。

bsearch(type A[], type a) {
start = 1, end = length(A)

    while ( start <= end ) {
        mid = floor(start + end / 2)

        if ( A[mid] == a ) return mid
        if ( A[mid] > a ) end = mid - 1
        if ( A[mid] < a ) start = mid + 1

    }
    return -1

}

所以循环条件 似乎 非常简单 - 当 start > end 循环终止。但为什么循环是正确的？证明其正确性的循环不变量是什么？

不变量是逻辑语句：

if ( A[mid] == a ) then ( start <= mid <= end )

这个陈述是一个逻辑重言式 - 在我们试图证明的特定循环/算法的上下文中它总是正确的。它还提供了有关循环终止后循环正确性的有用信息。

如果我们返回是因为我们在数组中找到了元素，那么该语句显然是正确的，因为如果A[mid] == a 那么a 在数组中并且mid 必须在开始和结束之间。如果循环因start > end 而终止，则不存在start <= mid 和 mid <= end 这样的数字，因此我们知道语句A[mid] == a 必须为假。然而，结果是整个逻辑陈述在空意义上仍然是正确的。 （在逻辑上，if (false) then (something) 的语句总是正确的。）

现在我所说的当循环终止时循环条件必然为假呢？看起来当在数组中找到元素时，当循环终止时循环条件为真！？实际上不是，因为隐含的循环条件实际上是while ( A[mid] != a && start <= end )，但我们缩短了实际测试，因为第一部分是隐含的。无论循环如何终止，这个条件在循环之后显然是错误的。

Answer 7

不变的意思是永远不变

这里的循环不变量意味着“循环中变量发生的变化（递增或递减）不会改变循环条件，即条件满足”，因此循环不变量的概念已经出现

Answer 8

以前的答案以非常好的方式定义了循环不变量。

以下是 CLRS 的作者如何使用循环不变量来证明插入排序的正确性。

插入排序算法（如书中给出）：

INSERTION-SORT(A)
    for j ← 2 to length[A]
        do key ← A[j]
        // Insert A[j] into the sorted sequence A[1..j-1].
        i ← j - 1
        while i > 0 and A[i] > key
            do A[i + 1] ← A[i]
            i ← i - 1
        A[i + 1] ← key

在这种情况下循环不变量： 子数组[1 到 j-1] 总是排序的。

现在让我们检查一下，证明算法是正确的。

初始化：在第一次迭代 j=2 之前。所以子数组[1:1]就是要测试的数组。因为它只有一个元素，所以它是排序的。因此满足不变量。

维护：这可以通过在每次迭代后检查不变量来轻松验证。在这种情况下，它是满意的。

终止：这是我们将证明算法正确性的步骤。

当循环终止时，j=n+1 的值。再次满足循环不变量。这意味着应该对 Sub-array[1 to n] 进行排序。

这就是我们想要用我们的算法做的事情。因此我们的算法是正确的。

Answer 9

循环不变量是一个数学公式，例如(x=y+1)。在该示例中，x 和 y 表示循环中的两个变量。考虑到这些变量在整个代码执行过程中的变化行为，几乎不可能测试所有可能的 x 和 y 值并查看它们是否产生任何错误。假设x 是一个整数。整数可以在内存中保存 32 位空间。如果超过该数量，则会发生缓冲区溢出。所以我们需要确保在代码的整个执行过程中，它永远不会超过那个空间。为此，我们需要了解一个显示变量之间关系的通用公式。 毕竟，我们只是试图了解程序的行为。

Answer 10

在线性搜索中（根据书中给出的练习），我们需要在给定数组中找到值 V。

它很简单，从 0

根据我对上述问题的理解-

循环不变量（初始化）： 在 k - 1 次迭代中找不到 V。第一次迭代，这将是 -1 因此我们可以说 V 在位置 -1 找不到

维护： 在下一次迭代中，在 k-1 中找不到的 V 成立

终止： 如果 V 在 k 位置找到或 k 达到数组的长度，则终止循环。

Answer 11

很难跟踪循环发生的情况。不终止或在没有达到其目标行为的情况下终止的循环是计算机编程中的常见问题。循环不变量有帮助。循环不变量是关于程序中变量之间关系的正式陈述，它在循环运行之前成立（建立不变量）并且在循环底部再次为真，每次通过循环（保持不变量)。 以下是代码中使用循环不变量的一般模式：

... // 这里的循环不变量必须为真
而（测试条件）{
// 循环顶部
...
// 循环底部
// 这里的循环不变量必须为真
}
// 终止 + 循环不变量 = 目标
...
在环路的顶部和底部之间，可能正在朝着达到环路的目标前进。这可能会扰乱（使错误）不变量。 Loop Invariants 的重点是保证在每次重复循环体之前都会恢复不变量。 这样做有两个好处：

工作不会以复杂的、依赖数据的方式进行到下一个阶段。每个通道都独立于所有其他通道通过循环，不变量用于将通道绑定在一起成为一个工作整体。 循环工作的推理简化为循环不变量在每次通过循环时恢复的推理。这将循环的复杂整体行为分解为简单的小步骤，每个步骤都可以单独考虑。 循环的测试条件不是不变量的一部分。这就是使循环终止的原因。您分别考虑两件事：为什么循环应该终止，以及为什么循环在终止时实现其目标。如果每次通过循环您更接近满足终止条件，则循环将终止。通常很容易保证这一点：例如。将计数器变量递增 1 直到达到固定上限。有时终止的原因更困难。

应该创建循环不变量，以便当满足终止条件并且不变量为真时，达到目标：

不变 + 终止 => 目标
创建简单且相关的不变量需要练习，这些不变量捕获除终止之外的所有目标实现。最好使用数学符号来表示循环不变量，但是当这导致过于复杂的情况时，我们依赖于清晰的散文和常识。

Answer 12

抱歉，我没有评论权限。

你提到的@Tomas Petricek

一个较弱的不变式也是正确的，即 i >= 0 && i

它是如何成为循环不变量的？

希望我没有看错，据我了解^[1]，循环不变量在循环开始（初始化）时会为真，每次迭代前后都会为真（维护）和循环终止后（终止）也是如此。但是在最后一次迭代之后 i 变为 10。因此，条件 i >= 0 && i

[1]http://www.win.tue.nl/~kbuchin/teaching/JBP030/notebooks/loop-invariants.html

Answer 13

循环不变属性是循环执行的每一步都成立的条件（即 for 循环、while 循环等）

这对于循环不变证明是必不可少的，在这种证明中，如果算法在执行的每一步都保持该循环不变属性，则可以证明该算法正确执行。

为了使算法正确，循环不变量必须保持在：

初始化（开头）

维护（之后的每一步）

终止（完成后）

这用于评估一堆东西，但最好的例子是用于加权图遍历的贪心算法。贪心算法要产生最优解（图上的路径），它必须尽可能以最低权重路径连接所有节点。

因此，循环不变属性是所走路径的权重最小。在开始我们没有添加任何边，所以这个属性是真的（在这个例子中它不是假的）。在每一步，我们遵循最低权重边缘（贪婪步骤），因此我们再次采用最低权重路径。在最后，我们找到了最低加权路径，所以我们的性质也是如此。

如果算法不这样做，我们可以证明它不是最优的。

Answer 14

简单来说，就是一个在每次循环迭代中都为真的LOOP条件：

for(int i=0; i<10; i++)
{ }

在这里我们可以说 i 的状态是i<10 and i>=0

Answer 15

循环不变量是在循环执行前后为真的断言。

Answer 16

How to Think About Algorithms 的定义，Jeff Edmonds

循环不变量是放置在循环顶部的断言，并且 每次计算返回到循环顶部时，它都必须成立。