循环不变式(Loop Invariant)与算法正确性

循环不变式是让循环成立的一个statement，其必须具备三个性质：

1. 初始(Initialization)：在循环开始（第一次迭代）之前，它为真
2. 保持(Maintenance)：如果循环的某次迭代之前它为真，那么下次迭代之前它仍为真。
3. 终止(Termination)：当循环终止时（在某种条件下），不变式为我们提供一个有用的性质，该性质有助于证明算法是正确的。

Insertion Sort

对于插入排序来说，“A[1, …, j - 1]是有序的”这一statement是它的循环不定式。

初始：在进行第一次循环之前(j = 2)，因为仅有单个元素A[1]，因此A[1,…, j - 1]一定是有序的。

保持：因为循环将循环中的每一元素向右移动，直到此次插入的A[j]到恰当的元素。因此我们可以保证，从A[1,…, j - 1]一定是有序的。

终止：for循环终止的条件是j超出A的长度。因为每次j都是增加1，因此必会发生j>A.length。那么整个数组A[1, …, j]一定是有序的

Insertion-Sort(A)
  for j = 2 to A.length
      key = A[j]
      i = j - 1
      while i > 0 and A[i] > key
          A[i + 1] = A[i]
          i = i - 1
      A[i + 1] = key