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

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

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

初始化(开始)

维护(之后的每一步)

终止(当它完成时)

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

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

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

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

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

在循环开始之前 在每次循环迭代之前 在循环结束之后

(尽管在循环体期间它可以暂时为假)。另一方面，循环条件在循环结束后必须为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 )

这句话是逻辑重言——在我们试图证明的特定循环/算法的上下文中，它总是正确的。并且在循环结束后，它提供了关于循环正确性的有用信息。

If we return because we found the element in the array then the statement is clearly true, since if A[mid] == a then a is in the array and mid must be between start and end. And if the loop terminates because start > end then there can be no number such that start <= mid and mid <= end and therefore we know that the statement A[mid] == a must be false. However, as a result the overall logical statement is still true in the null sense. ( In logic the statement if ( false ) then ( something ) is always true. )

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

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

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

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

正如你提到的@Tomas Petricek

另一个较弱的不变式也是成立的，即i >= 0 && i < 10(因为这是连续条件!)”

为什么它是循环不变量?

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

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

Loop invariant is a mathematical formula such as (x=y+1). In that example, x and y represent two variables in a loop. Considering the changing behavior of those variables throughout the execution of the code, it is almost impossible to test all possible to x and y values and see if they produce any bug. Lets say x is an integer. Integer can hold 32 bit space in the memory. If that number exceeds, buffer overflow occurs. So we need to be sure that throughout the execution of the code, it never exceeds that space. for that, we need to understand a general formula that shows the relationship between variables. After all, we just try to understand the behavior of the program.

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

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

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

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

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

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