不变的意思是永不改变

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

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.

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

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

除了这些不错的答案，我想Jeff Edmonds在《如何思考算法》(How to Think About Algorithms)中举的一个很好的例子可以很好地说明这个概念:

EXAMPLE 1.2.1 "The Find-Max Two-Finger Algorithm" 1) Specifications: An input instance consists of a list L(1..n) of elements. The output consists of an index i such that L(i) has maximum value. If there are multiple entries with this same value, then any one of them is returned. 2) Basic Steps: You decide on the two-finger method. Your right finger runs down the list. 3) Measure of Progress: The measure of progress is how far along the list your right finger is. 4) The Loop Invariant: The loop invariant states that your left finger points to one of the largest entries encountered so far by your right finger. 5) Main Steps: Each iteration, you move your right finger down one entry in the list. If your right finger is now pointing at an entry that is larger then the left finger’s entry, then move your left finger to be with your right finger. 6) Make Progress: You make progress because your right finger moves one entry. 7) Maintain Loop Invariant: You know that the loop invariant has been maintained as follows. For each step, the new left finger element is Max(old left finger element, new element). By the loop invariant, this is Max(Max(shorter list), new element). Mathe- matically, this is Max(longer list). 8) Establishing the Loop Invariant: You initially establish the loop invariant by point- ing both fingers to the first element. 9) Exit Condition: You are done when your right finger has finished traversing the list. 10) Ending: In the end, we know the problem is solved as follows. By the exit condi- tion, your right finger has encountered all of the entries. By the loop invariant, your left finger points at the maximum of these. Return this entry. 11) Termination and Running Time: The time required is some constant times the length of the list. 12) Special Cases: Check what happens when there are multiple entries with the same value or when n = 0 or n = 1. 13) Coding and Implementation Details: ... 14) Formal Proof: The correctness of the algorithm follows from the above steps.

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

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

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

By itself, a loop invariant doesn't do much. However, given an appropriate invariant, it can be used to help prove the correctness of an algorithm. The simple example in CLRS probably has to do with sorting. For example, let your loop invariant be something like, at the start of the loop, the first i entries of this array are sorted. If you can prove that this is indeed a loop invariant (i.e. that it holds before and after every loop iteration), you can use this to prove the correctness of a sorting algorithm: at the termination of the loop, the loop invariant is still satisfied, and the counter i is the length of the array. Therefore, the first i entries are sorted means the entire array is sorted.

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

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

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

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

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