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

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

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

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

初始化(开始)

维护(之后的每一步)

终止(当它完成时)

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

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

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

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

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著

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

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