什么是循环不变量？

Question

我正在阅读 CLRS 的《算法导论》。在第二章中，作者提到了“循环不变量”。什么是循环不变量？

Answer 1

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

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

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

Answer 2

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

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

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

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

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

Answer 3

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

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

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 and mid <= end 因此我们知道语句 A[mid] == a 必须为 false。然而，结果是整个逻辑陈述在零意义上仍然是正确的。 （在逻辑中，语句 if ( false ) then (something ) 总是 true。）

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

Answer 4

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

以下是 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 到 n] 应该被排序。

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

Answer 5

除了所有好的答案之外，我想 Jeff Edmonds 的如何思考算法中的一个很好的例子可以很好地说明这个概念：

示例 1.2.1“Find-Max 二指算法”

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

2) 基本步骤：您决定使用两指方法。你的右手手指
顺着列表往下看。

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

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

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

6) 取得进步：你取得进步是因为你的右手手指移动了
一项。

7）维护循环不变式：您知道循环不变式已按如下方式维护。对于每一步，新的左手指元素
是Max（旧左指元素，新元素）。由循环不变式，
这是 Max(Max(较短的列表)，新元素)。从数学上来说，这是
最大（更长的列表）。

8) 建立循环不变式：首先通过将两根手指指向第一个元素来建立循环不变式。

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

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

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

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

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

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

Answer 6

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

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

Answer 7

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

Answer 8

不变式的含义是永不改变

这里的循环不变式是指“循环中变量发生的变化（递增或递减）不会改变循环条件，即条件满足”，由此产生了循环不变式的概念

Answer 9

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

这对于循环不变证明至关重要，可以证明算法在以下情况下正确执行：该循环不变属性在其执行的每一步中都保持不变。

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

初始化（开始）

维护（之后的每一步）

终止（当它结束时）完成）

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

因此，循环不变性是所采用的路径权重最小。在开始时，我们没有添加任何边，因此该属性为 true（在本例中，它不是 false）。在每一步，我们遵循最低权重边缘（贪婪步骤），因此我们再次采用最低权重路径。在最后，我们找到了最低权重的路径，因此我们的属性也是正确的。

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

Answer 10

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

...
// 这里循环不变式必须为真
while (测试条件) {
// 循环顶部
...
// 循环底部
// 这里循环不变式必须为真
}
// 终止 + 循环不变式 = 目标
...
在循环的顶部和底部之间，可能正在朝着实现循环的目标取得进展。这可能会扰乱（使错误）不变量。循环不变量的要点是保证每次重复循环体之前都会恢复不变量。
这样做有两个优点：

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

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

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

Answer 11

如何思考算法的定义，作者：Jeff Edmonds

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

Answer 12

抱歉，我没有评论权限。

正如您提到的@Tomas Petricek

一个较弱但同样成立的不变量是 i >= 0 &&我< 10（因为这是继续条件！）”

怎么是循环不变式？

希望我没有错，据我了解^[1]，循环不变式在开始时为真循环（初始化），每次迭代（维护）之前和之后都会为真，循环终止（终止）后它也会为真，但在最后一次迭代之后 i 变成 10。所以 & 10 变为假并终止循环。

，条件 i >= 0 & ; .tue.nl/~kbuchin/teaching/JBP030/notebooks/loop-invariants.html" rel="nofollow noreferrer">http://www.win.tue.nl/~kbuchin/teaching/JBP030/notebooks/loop-不变量.html

Answer 13

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

Answer 14

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

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

在此我们可以说 i 的状态为 i<10 且 i>=0

Answer 15

循环不变量是在循环执行之前和之后都为 true 的断言。

Answer 16

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

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

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

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

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

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