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

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

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

初始化(开始)

维护(之后的每一步)

终止(当它完成时)

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

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

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

不变的意思是永不改变

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

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。