307

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

4

16 回答 16

390

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

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

在此示例中，（对于每次迭代）确实如此i + j == 9。一个较弱的不变量也是正确的，那就是 i >= 0 && i <= 10。

于 2010-07-11T02:10:59.517 回答
136

我喜欢这个非常简单的定义：（来源）

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

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

一个更简单的例子：循环不变量、正确性和程序推导。

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

于 2010-07-11T02:17:07.993 回答
44

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

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

  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

}

所以循环条件看起来很简单——当开始>结束时循环终止。但为什么循环是正确的？证明其正确性的循环不变量是什么？

不变量是逻辑语句：

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

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

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

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

于 2013-03-12T08:48:56.183 回答
38

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

以下是 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] 进行排序。

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

于 2015-01-05T07:12:22.400 回答
19

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

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

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

2）基本步骤：您决定两指方法。你的右手手指顺着列表向下移动。

3) 进度度量：进度度量是您的右手手指在列表中的距离。

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

5) 主要步骤：每次迭代，您将右手手指向下移动到列表中的一个条目。如果您的右手手指现在指向的条目比左手指的条目大，则移动您的左手指以与右手手指对齐。

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

7) 维护循环不变量：您知道循环不变量已保持如下。对于每一步，新的左手指元素是 Max(old left finger element, new element)。根据循环不变量，这是 Max(Max(shorter list), new element)。在数学上，这是 Max（更长的列表）。

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

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

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

11) 终止和运行时间：所需时间是列表长度的某个常数倍。

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

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

14）形式证明：算法的正确性由上述步骤得出。

于 2012-12-02T17:38:58.580 回答
6

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

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

于 2010-07-11T02:10:26.587 回答
6

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

于 2011-09-28T02:09:32.553 回答
4

不变的意思是永远不变

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

于 2014-09-19T07:02:34.807 回答
2

循环不变属性是一个条件，它适用于循环执行的每个步骤（即 for 循环、while 循环等）

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

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

初始化（开始）

维护（之后的每一步）

终止（完成时）

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

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

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

于 2017-03-09T01:13:50.830 回答
2

如何思考算法的定义，杰夫·埃德蒙兹（Jeff Edmonds）

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

于 2021-01-18T15:56:40.540 回答
1

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

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

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

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

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

于 2015-09-09T19:07:00.563 回答
1

对不起，我没有评论权限。

@Tomas Petricek 正如你提到的

一个较弱的不变式也是正确的，即 i >= 0 && i < 10（因为这是延续条件！）”

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

我希望我没有错，据我了解[1]，循环不变量在循环开始时为真（初始化），在每次迭代之前和之后都为真（维护），之后也为真循环的终止（Termination）。但是在最后一次迭代之后 i 变为 10。因此，条件 i >= 0 && i < 10 变为 false 并终止循环。它违反了循环不变量的第三个属性（终止）。

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

于 2016-11-05T05:10:33.173 回答
0

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

于 2015-05-30T20:11:55.723 回答
0

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

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

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

于 2017-10-28T13:59:53.737 回答
0

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

于 2018-10-10T13:54:15.970 回答
-1

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

它很简单，从 0 <= k < 长度扫描数组并比较每个元素。如果找到 V，或者如果扫描达到数组的长度，则终止循环。

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

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

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

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

于 2015-08-27T08:49:43.323 回答