之前的回答已经很好地定义了循环不变量。

以下是CLRS的作者如何使用循环不变量来证明插入排序的正确性。

插入排序算法(见书):

INSERTION-SORT(A)
    for j ← 2 to length[A]
        do key ← A[j]
        // Insert A[j] into the sorted sequence A[1..j-1].
        i ← j - 1
        while i > 0 and A[i] > key
            do A[i + 1] ← A[i]
            i ← i - 1
        A[i + 1] ← key

循环不变量在这种情况下: 子数组[1到j-1]始终被排序。

现在让我们检查一下，证明这个算法是正确的。

初始化:在第一次迭代j=2之前。所以子数组[1:1]就是要测试的数组。因为它只有一个元素，所以它是有序的。这样不变性就被满足了。

维护:这可以通过在每次迭代后检查不变量来轻松验证。在这种情况下，它被满足了。

终止:这是我们将证明算法正确性的步骤。

当循环结束时，j=n+1。循环不变量再次被满足。这意味着子数组[1到n]应该排序。

这就是我们想用算法做的。因此，我们的算法是正确的。

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.

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

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

《如何思考算法》的定义，Jeff Edmonds著

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

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

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

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

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

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

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.

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

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