我在读CLRS的《算法导论》。在第二章中，作者提到了“循环不变量”。什么是循环不变量?
当前回答
之前的回答已经很好地定义了循环不变量。
以下是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，则算法失败。
简单地说，循环不变量是对循环的每次迭代都成立的某个谓词(条件)。例如，让我们看一个简单的For循环，它是这样的:
int j = 9;
for(int i=0; i<10; i++)
j--;
在这个例子中，i + j == 9(对于每个迭代)是正确的。一个较弱的不变式也是成立的 I >= 0 && I <= 10。
《如何思考算法》的定义，Jeff Edmonds著
循环不变式是放置在循环和循环顶部的断言 每次计算返回到循环的顶部时，这必须成立。
之前的回答已经很好地定义了循环不变量。
以下是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]应该排序。
这就是我们想用算法做的。因此，我们的算法是正确的。
不变的意思是永不改变
这里循环不变量的意思是“发生在循环中的变量的变化(增加或减少)并没有改变循环条件，即条件是满足的”，因此循环不变量的概念就产生了
