什么是循环不变量?

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

204768 次浏览
小开

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

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

小开
最佳答案

简单地说，循环不变量是对循环的每次迭代都成立的某个谓词(条件)。例如，让我们看一个简单的for循环，它看起来像这样:

int j = 9;
for(int i=0; i<10; i++)
j--;
< p >在这个例子的确i + j == 9(每迭代)。一个较弱的不变式也是成立的 i >= 0 && i <= 10 . < / p >
小开

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

循环不变量是(程序变量之间的)一种条件，它必须在每次循环迭代之前和之后立即为真。(请注意，在迭代过程中，这并没有说明它的真伪。)

循环不变量本身并没有什么作用。然而，给定一个适当的不变量，它可以用来帮助证明算法的正确性。CLRS中的简单示例可能与排序有关。例如，让你的循环不变量是这样的，在循环开始时，这个数组的第一个i项被排序。如果你能证明这确实是一个循环不变式(即它在每次循环迭代之前和之后都成立)，你可以用它来证明排序算法的正确性:在循环结束时，循环不变式仍然满足，计数器i是数组的长度。因此，第一个i项被排序意味着整个数组被排序。

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

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

小开

值得注意的是，循环不变量可以帮助迭代算法的设计，因为它被认为是一个断言，表示变量之间的重要关系，在每次迭代开始时和循环结束时，这些关系必须为真。如果这是成立的，计算是在有效的道路上。如果为false，则算法失败。

小开

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

例1.2.1“Find-Max两指算法”

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

.返回一个 基本步骤:你决定用两指法。你的右手手指

3)进步的衡量:进步的衡量是我们已经走了多远

4)循环不变量:循环不变量声明您的左手手指指向迄今为止您遇到的最大条目之一 正确的手指。< / p > 主要步骤:每次迭代，你的右手手指向下移动一个 列表中的条目。如果你的右手手指现在指向一个入口 这比左手手指的入口大，然后移动你的左手 手指和你的右手手指在一起

取得进步:你取得进步是因为你的右手手指移动了 一个条目. < / p >

7)保持循环不变:你知道循环不变式被维护如下。对于每一步，新的左手手指元素 是Max(旧的左手手指元素，新元素)。通过循环不变量， 这是Max(Max(更短的列表)，新元素)。从数学上讲，这是 马克斯(长列表)。< / p >

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

9)退出条件:当你的右手手指完成时，你就完成了

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

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

12)特殊情况:检查当有多个条目时会发生什么 当n = 0或n = 1时，

13)编码和实现细节:…

14)形式证明:算法的正确性由 以上步骤。< / p >

小开

在处理循环和不变量时，有一件事很多人没有马上意识到。他们混淆了循环不变量和循环条件(控制循环终止的条件)。

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

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

(尽管在循环体期间它可以暂时为假)。另一方面，循环条件 必须在循环结束后为false，否则循环将永远不会结束。

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

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

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] == a则a在数组中，而mid必须位于开始和结束之间。如果循环因为start > end而终止，则不可能存在start <= mid 而且 mid <= end这样的数字，因此我们知道语句A[mid] == a一定是假的。然而，结果是整个逻辑语句在空意义上仍然是真的。(在逻辑上，如果(假)那么(某物)总是真的。)

那么我说的循环条件在循环结束时必然为假呢?当在数组中找到元素时，循环条件在循环结束时为true !?实际上不是，因为隐含的循环条件实际上是while ( A[mid] != a && start <= end )，但我们缩短了实际的测试，因为第一部分是隐含的。这个条件在循环结束后明显为false，而不管循环如何结束。

小开

不变的意思是永不改变

这里循环不变量的意思是“发生在循环中的变量的变化(增加或减少)并没有改变循环条件，即条件是满足的”，因此循环不变量的概念就产生了

小开

之前的回答已经很好地定义了循环不变量。

以下是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。循环不变量再次被满足。这意味着子数组[1到n]应该排序。

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

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

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

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

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

< >强循环不变式(初始化): 在k - 1迭代中找不到V。第一次迭代，这是-1因此我们可以说V不在-1位置

< >强保养: 在下一次迭代中，V不在k-1中成立

< >强Terminatation: 如果V在k个位置或者k达到数组的长度，则终止循环

小开
很难跟踪循环发生了什么。在计算机编程中，循环不终止或未达到目标而终止是一个常见的问题。循环不变量有帮助。循环不变量是关于程序中变量之间关系的正式声明，它在循环运行之前为真(建立不变量)，在循环的底部也为真，每次通过循环(保持不变量)。 下面是在你的代码中使用循环不变量的一般模式:

< p >… //循环不变量在这里必须为真
. 0 while (TEST CONDITION) {
//循环的顶部
.循环的顶部
.循环的顶部 < br >… //循环的底部
.循环结束 //循环不变量在这里必须为真
. 0 } < br > //终止+循环不变量=目标
< br >… 在循环的顶部和底部之间，可能正在朝着实现循环的目标前进。这可能会扰乱(使不变量为假)。循环不变量的重点是保证在每次重复循环体之前不变量将被恢复。 这样做有两个好处:

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

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

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

小开

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

正如你提到的@Tomas Petricek

另一个较弱的不变式也是成立的i >= 0 &&我& lt;10(因为这是延续条件!)”

为什么它是循环不变量?

我希望我没有错，据我所知__abc0，循环不变量将在循环开始时为真(初始化)，它将在每次迭代(维护)和在循环结束后也为真(terminate)之前和之后为真。但是在最后一次迭代之后，i变成了10。条件i >= 0 &&我& lt;10变为false并终止循环。它违反了循环不变量的第三个性质(终止)。

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

小开

循环不变量属性是一个条件，适用于循环执行的每一步。For循环，while循环，等等)

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

对于一个正确的算法，循环不变量必须保持在:

初始化(开始)

维护(之后的每一步)

终止(当它完成时)

这被用来计算很多东西，但最好的例子是加权图遍历的贪婪算法。对于贪心算法产生最优解(穿过图的路径)，它必须达到连接所有节点在最小权值路径可能。

因此，循环不变的性质是所选择的路径具有最小的权值。在开始中，我们没有添加任何边，所以这个属性为真(在这种情况下，它不是假的)。在每一个步骤处，我们遵循最低权值边(贪婪步)，所以我们再次采用最低权值路径。在结束，我们已经找到了最低加权路径，所以我们的性质也是真的。

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

小开

简单地说，它是一个循环条件，在每次循环迭代中都为真:

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

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

小开

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

小开

由如何思考算法，作者:Jeff Edmonds定义

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

提交答案