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

以下是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]应该排序。

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

在处理循环和不变量时，有一件事很多人没有马上意识到。他们混淆了循环不变量和循环条件(控制循环终止的条件)。

正如人们指出的那样，循环不变量必须为真

在循环开始之前 在每次循环迭代之前 在循环结束之后

(尽管在循环体期间它可以暂时为假)。另一方面，循环条件在循环结束后必须为false，否则循环将永远不会终止。

因此循环不变量和循环条件必须是不同的条件。

复杂循环不变量的一个很好的例子是用于二分搜索。

bsearch(type A[], type a) {
start = 1, end = length(A)

    while ( start <= end ) {
        mid = floor(start + end / 2)

        if ( A[mid] == a ) return mid
        if ( A[mid] > a ) end = mid - 1
        if ( A[mid] < a ) start = mid + 1

    }
    return -1

}

因此循环条件看起来非常简单——当开始>结束时，循环终止。但是为什么循环是正确的呢?什么是循环不变量来证明它的正确性?

不变量是逻辑语句:

if ( A[mid] == a ) then ( start <= mid <= end )

这句话是逻辑重言——在我们试图证明的特定循环/算法的上下文中，它总是正确的。并且在循环结束后，它提供了关于循环正确性的有用信息。

If we return because we found the element in the array then the statement is clearly true, since if A[mid] == a then a is in the array and mid must be between start and end. And if the loop terminates because start > end then there can be no number such that start <= mid and mid <= end and therefore we know that the statement A[mid] == a must be false. However, as a result the overall logical statement is still true in the null sense. ( In logic the statement if ( false ) then ( something ) is always true. )

那么我说的循环条件在循环结束时必然为假呢?当在数组中找到元素时，循环条件在循环结束时为true !?实际上不是，因为隐含的循环条件实际上是while (A[mid] != A && start <= end)，但我们缩短了实际的测试，因为第一部分是隐含的。这个条件在循环结束后明显为false，而不管循环如何结束。

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

以下是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]应该排序。

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

在线性搜索(根据书中给出的练习)中，我们需要在给定的数组中找到值V。

它很简单，从0 <= k < length开始扫描数组并比较每个元素。如果找到V，或者扫描到数组的长度，就终止循环。

根据我对上述问题的理解-

循环不变量(初始化): 在k - 1迭代中找不到V。第一次迭代，这是-1因此我们可以说V不在-1位置

保养: 在下一次迭代中，V不在k-1中成立

Terminatation: 如果V位于k个位置，或者k达到数组的长度，则终止循环。

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

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

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

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

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