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

正如你提到的@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

It is hard to keep track of what is happening with loops. Loops which don't terminate or terminate without achieving their goal behavior is a common problem in computer programming. Loop invariants help. A loop invariant is a formal statement about the relationship between variables in your program which holds true just before the loop is ever run (establishing the invariant) and is true again at the bottom of the loop, each time through the loop (maintaining the invariant). Here is the general pattern of the use of Loop Invariants in your code:

... // the Loop Invariant must be true here while ( TEST CONDITION ) { // top of the loop ... // bottom of the loop // the Loop Invariant must be true here } // Termination + Loop Invariant = Goal ... Between the top and bottom of the loop, headway is presumably being made towards reaching the loop's goal. This might disturb (make false) the invariant. The point of Loop Invariants is the promise that the invariant will be restored before repeating the loop body each time. There are two advantages to this:

Work is not carried forward to the next pass in complicated, data dependent ways. Each pass through the loop in independent of all others, with the invariant serving to bind the passes together into a working whole. Reasoning that your loop works is reduced to reasoning that the loop invariant is restored with each pass through the loop. This breaks the complicated overall behavior of the loop into small simple steps, each which can be considered separately. The test condition of the loop is not part of the invariant. It is what makes the loop terminate. You consider separately two things: why the loop should ever terminate, and why the loop achieves its goal when it terminates. The loop will terminate if each time through the loop you move closer to satisfying the termination condition. It is often easy to assure this: e.g. stepping a counter variable by one until it reaches a fixed upper limit. Sometimes the reasoning behind termination is more difficult.

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

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

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

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

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

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

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

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

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.

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

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

在这个例子中，i + j == 9(对于每个迭代)是正确的。一个较弱的不变式也是成立的 I >= 0 && I <= 10。