什么是循环不变式

循环不变式是一种帮助我们理解算法正确性的工具。定义一个循环不变式(Loop invariance)，然后证明关于这个循环不变式的三个性质：

初始化： 循环的第一次迭代之前，循环不变式为真。
保持： 如果循环的某次迭代之前循环不变式为真，那么下次迭代之前循环不变式仍为真。
终止： 在循环终止时，不变时为我们提供了一个有用的性质，该性质帮助我们证明算法是正确的。

可以看到循环不变式的思想其实和归纳法的思想是一样的。如果能够理解归纳法，那么就能够理解循环不变式。

下面以插入排序的例子，来具体的说明什么是循环不变式。

给出插入排序的一个实现：

 def insert_sort(A):
    for j in range(1, len(A)):
      key = A[j]
      i = j - 1
      while i > -1 and A[i] > key:
          A[i+1] = A[i]
          i = i - 1
      A[i+1] = key
    return A

给出最外层for循环的循环不变式：在每次迭代之前，子数组A[0..j-1]是排序好的。

初始化：在第一轮迭代开始之前 j=1, 子数组A[0..j-1]只包含A[0]一个元素，故子数组 A[0..j-1] 是有序的。

保持: 在while循环中，将A[j-1]，A[j-2]等等向右移动一个位置，直到找到A[j]的适当的位置即i+1，将A[j]插入到该位置。此时的子数组A[0..j]由原来的子数组A[0..j]中的元素组成，但是已经按序排列。故，下一次迭代增加 j 时仍然保持循环不变式。

终止： 循环终止的条件是 j > len(A)-1, 故当循环终止时，j = len(A)。根据循环不变式，子数组A[0..len(A)-1]是排好序的。子数组A[0..len(A)-1]的长度为（len(A) - 1） - 0 + 1 = len(A), 故数组A是有序的。

至此证明了插入排序的正确性。

如何使用循环不变式的思想写代码

如果我们可以使用循环不变式来证明算法的正确性，那么在构思算法时，使算法的形式易于使用循环不变式来证明并且满足循环不变式的三个性质，我们就能够确信算法是正确的。

在打开编辑器写代码之前，应该在纸面上或者脑海里构建循环不变式，构思算法使其易于证明循环不变式的三个性质，最终写下代码，这时就可以确信算法的实现在逻辑上是正确的。

不经构思而写出的结构混乱的循环，会导致我们在测试阶段不断地对循环变量、边界等等进行修修补补，或者干脆算法逻辑上就是错误的，导致浪费大量的时间在 Debug 阶段。而使用循环不变式，首先确定循环不变式，再写出易于证明的算法，证明其正确性，会大幅度减少花费在Debug上面的时间。