什么是循环不变量？

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

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

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

旦彤

我喜欢这个非常简单的定义:(来源）循环不变量是[程序变量中的]条件，它必须在循环的每次迭代之前和之后立即生效。（注意，这在迭代的某个部分没有说明它的真实性或虚假性。）循环不变本身并没有多大作用。但是，给定适当的不变量，它可以用来帮助证明算法的正确性。 CLRS中的简单示例可能与排序有关。例如，让你的循环不变，就像在循环开始时，对这个数组的第一个i条目进行排序。如果你可以证明这确实是一个循环不变量（即它在每次循环迭代之前和之后保持），你可以用它来证明排序算法的正确性：在循环终止时，循环不变量仍然满足，计数器i是数组的长度。因此，第一个i条目被排序意味着整个数组被排序。一个更简单的例子：循环不变量，正确性和程序派生。我理解循环不变量的方式是作为推理程序的系统的，正式的工具。我们做一个单独的陈述，我们专注于证明是真的，我们称之为循环不变量。这组织了我们的逻辑。虽然我们也可以非正式地讨论某些算法的正确性，但使用循环不变量会迫使我们仔细思考并确保我们的推理是不透明的。

帆攀缺锯欧

在处理循环和不变量时，有许多人没有立即意识到这一点。他们在循环不变量和循环条件（控制循环终止的条件）之间感到困惑。正如人们所指出的，循环不变量必须是真的在循环开始之前在循环的每次迭代之前循环结束后（虽然在循环体中它可能暂时是假的）。另一方面，循环终止后循环条件必须为假，否则循环永远不会终止。因此，循环不变量和循环条件必须是不同的条件。复杂循环不变量的一个很好的例子是二进制搜索。

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 > end那么就不会有number13ѭ和mid <= end这样的数字，因此我们知道语句A[mid] == a必须是假的。但是，因此整体逻辑语句在空意义上仍然是正确的。（在逻辑中，语句if（false）then（something）总是如此。）那么当循环终止时，我所说的循环条件必然是假的呢？看起来当在数组中找到元素时，当循环终止时，循环条件为真！它实际上不是，因为隐含的循环条件实际上是while ( A[mid] != a && start <= end )但是我们缩短了实际测试，因为第一部分是隐含的。无论循环如何终止，这个条件在循环后显然都是假的。

咖哀烈

以前的答案以非常好的方式定义了循环不变量。现在让我试着解释CLRS的作者如何使用Loop Invariants来证明Insertion Sort的正确性。插入排序算法（如书中所示）：

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

在这种情况下循环不变（来源：CLRS书）：子阵列[1到j-1]始终排序。现在让我们检查一下并证明算法是正确的。初始化：在第一次迭代之前j = 2。所以Subarray [1：1]是要测试的数组。因为它只有一个元素所以它被排序。因此Invariant是满意的。维护：通过在每次迭代后检查不变量可以很容易地验证这一点。在这种情况下，它是满意的。终止：这是我们证明算法正确性的步骤。当循环终止时，则j = n + 1的值。再次满足循环不变量。这意味着应该对子阵列[1到n]进行排序。这就是我们想要用算法做的事情。因此我们的算法是正确的。

浩挎

除了所有的好答案之外，我想Jeff Edmonds的“如何思考算法”这个很好的例子可以很好地说明这个概念：例1.2.1“Find-Max双指算法” 1）规格：输入实例由列表L（1..n）组成元素。输出由索引i组成，使得L（i）具有最大值值。如果有多个条目具有相同的值，那么任何条目其中一个被退回。 2）基本步骤：您决定使用双指方法。你的右手指在列表中运行。 3）进度测量：进度的衡量标准是沿着进度列出你的右手指是。 4）循环不变量：循环不变量表明你的左手指向你目前遇到的最大条目之一右手指。 5）主要步骤：每次迭代，你将右手指向下移动一个列表中的条目。如果右手指现在指向一个条目它比左手指的入口大，然后向左移动用右手指指。 6）取得进步：你的右手指移动，你取得了进步一个条目。 7）维护循环不变量：您知道循环不变量已按如下方式维护。对于每个步骤，新的左手指元素是Max（旧左手指元素，新元素）。通过循环不变量，这是Max（Max（更短列表），新元素）。在数学上，这是 Max（更长的列表）。 8）建立循环不变量：最初通过将两个手指指向第一个元素来建立循环不变量。 9）退出条件：当你的右手指完成时你就完成了遍历清单。 10）结束：最后，我们知道问题解决如下。通过出口条件，你的右手已经遇到了所有的条目。通过循环不变量，你的左手指指向最大值这些。退回此条目。 11）终止和运行时间：所需的时间是一些常数乘以列表的长度。 12）特殊情况：检查有多个条目时会发生什么具有相同的值或当n = 0或n = 1时。 13）编码和实施细节：...... 14）形式证明：算法的正确性来自于以上步骤。

嗓瑰

应当注意，循环不变量在被认为是表达变量之间的重要关系的断言时可以帮助设计迭代算法，所述变量在每次迭代开始时和循环终止时必须为真。如果这种情况成立，则计算是在实现有效性的道路上。如果为false，则算法失败。

凰葱崎济邯

在这种情况下，不变量意味着在每个循环迭代中的某个点必须为真的条件。在契约编程中，不变量是在调用任何公共方法之前和之后必须为真（通过契约）的条件。

瞥同忙接

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

谷靛

很难跟踪循环发生的情况。在没有实现其目标行为的情况下不终止或终止的循环是计算机编程中的常见问题。循环不变量有帮助。循环不变量是关于程序中变量之间关系的形式语句，它在循环运行之前保持为真（建立不变量），并且在循环的底部再次为真，每次循环（保持不变量））。以下是在代码中使用循环不变量的一般模式： ... // Loop Invariant必须在此处为true while（TEST CONDITION）{ //循环的顶部 ... //循环的底部 // Loop Invariant必须在此处为true } //终止+循环不变=目标 ... 在环的顶部和底部之间，可能正朝着达到环的目标的方向前进。这可能会扰乱（伪造）不变量。循环不变量的要点是在每次重复循环体之前恢复不变量的承诺。这有两个好处：工作不会以复杂的，依赖于数据的方式传递到下一轮。每个都独立于所有其他循环通过循环，使用不变的服务将通道绑定到一个工作整体。你的循环工作的推理减少到推断循环不变量随着每次循环而恢复。这将循环的复杂整体行为分解为小的简单步骤，每个步骤可以单独考虑。循环的测试条件不是不变量的一部分。这是循环终止的原因。你分别考虑两件事：为什么循环应该终止，以及循环在终止时实现其目标的原因。如果每次循环都接近满足终止条件，则循环将终止。通常很容易确保这一点：例如将计数器变量加1，直到达到固定的上限。有时终止背后的推理更加困难。应该创建循环不变量，以便在达到终止条件并且不变量为真时，达到目标：不变+终止=>目标需要练习创建简单且相关的不变量，其捕获除终止之外的所有目标达成。最好使用数学符号来表达循环不变量，但是当这导致过于复杂的情况时，我们依赖于明确的散文和常识。

嗓瑰

对不起，我没有评论权限。你提到的@Tomas Petricek 一个较弱的不变量也是如此，即i> = 0＆amp;＆amp;我＆lt; 10（因为这是继续条件！）“ 它是如何循环不变的？我希望我没有错，据我所知[1]，循环开始时循环不变将是正确的（初始化），在每次迭代之前和之后都是真的（维护），它也将是真的循环终止（终止）。但是在最后一次迭代之后，我变成10.因此，条件i> = 0＆amp;＆amp;我＆lt; 10变为false并终止循环。它违反了循环不变量的第三个属性（终止）。 [1] http://www.win.tue.nl/~kbuchin/teaching/JBP030/notebooks/loop-invariants.html

香腔弥胯瓤

循环不变属性是一个条件，它适用于循环执行的每一步（即for循环，while循环等）这对循环不变证明至关重要，其中一个人能够证明算法在其执行的每个步骤中都能正确执行，这个循环不变属性成立。要使算法正确，Loop Invariant必须保持在：初始化（开始）维护（后续的每一步）终止（当它完成时）这用于评估一堆事物，但最好的例子是加权图遍历的贪心算法。对于产生最佳解决方案（图中的路径）的贪婪算法，它必须连接到可能的最低权重路径中的所有节点。因此，循环不变性是所采用的路径具有最小权重。一开始我们没有添加任何边，所以这个属性是真的（在这种情况下它不是假的）。在每一步，我们都遵循最低权重边缘（贪婪的步骤），所以我们再次采用最低权重路径。最后，我们找到了最低的加权路径，所以我们的属性也是如此。如果算法不这样做，我们可以证明它不是最优的。

抽法

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

骚瓤

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

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

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

爆刺疤灯

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

缕嚏冻

在线性搜索中（根据书中给出的练习），我们需要在给定数组中找到值V. 其简单的是从0 <= k <扫描阵列。长度和比较每个元素。如果找到V，或者扫描到达数组的长度，则只需终止循环。根据我对上述问题的理解 - 循环不变量（初始化）：在k-1次迭代中找不到V.第一次迭代，这将是-1，因此我们可以说在位置-1处找不到V. 修的：在下一次迭代中，在k-1中找不到的V成立 Terminatation：如果在k位置找到V或k到达阵列的长度，则终止循环。

什么是循环不变量？

15 个回复

发起人

clrs

loop_invariant

问题状态

什么是循环不变量？

与内容相关的链接

15 个回复

发起人

clrs

loop_invariant

问题状态