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

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

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

(尽管在循环体期间它可以暂时为假)。另一方面，循环条件在循环结束后必须为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，而不管循环如何结束。

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

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

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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