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

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

不变的意思是永不改变

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

除了这些不错的答案，我想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.

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

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

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

初始化(开始)

维护(之后的每一步)

终止(当它完成时)

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

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

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

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

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

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