循环不变量（loop invariant）的理解算法

【循环不变量（loop invariant）的理解】在计算机科学中，循环不变量（loop invariant），是一组在循环体内、每次迭代均保持为真的某种性质，通常被用来证明程序或算法的正确性。
理解循环不变量这个概念对我们理解算法过程，和解决算法问题有很大的帮助。下面参考《算法导论》，对循环不变量的概念进行详细的解释。
我们使用循环不变量帮助我们理解一个算法为什么是对的。对于一个给定的循环不变量，我们必须遵循以下三个属性：

初始化：在循环的第一次迭代之前，循环不变量为真。
保持：如果在循环的一次迭代之前循环不变量为真，那么在下一次迭代之前循环不变量同样为真。
终止：当循环结束时，不变量能够提供我们有用的属性，用于帮助我们证实算法是正确的。

当保证前两个属性时，循环不变量在循环的任意迭代之前都满足。注意它与数学归纳法的相似性，当你想证明一个属性存在时，你需要证明一个基准和一个归纳步。相应的，我们第一次迭代之前保证不变量成立对应于一个基准，我们在每次迭代之间保证不变量成立对应于一个归纳步。
因为我们用循环不变量证明算法正确性，所以第三个属性或许是最重要的。通常，我们必须保证在循环结束时“循环不变量”和“循环终止条件”同时成立。这与数学归纳法有所不同。数学归纳法常采用无限的归纳步，而循环不变量的归纳往往随着循环的终止而结束。
接下来，我们通过插入排序算法来更好的理解循环不变量。
先贴代码（Go语言）

func insertionSort(nums []int) { j, n := 0, len(nums) for j < n { i := j - 1 key := nums[j] for i >= 0 && nums[i] > key { nums[i+1] = nums[i] i-- } nums[i+1] = key j++ } }

循环不变量： j之前（不包含nums[j]）的元素已经排好序（升序）。

初始化： j为0，表示目前排好序的子数组没有元素，不变式成立。
保持：如果前一轮迭代j满足条件，则[0,j)范围内子数组的元素均为升序。当前迭代中nums[j+1]与子数组的元素从大到小进行对比。如果找到第一个比nums[j+1]小的元素，则在其后插入一个值为nums[j+1]的元素。因此在此次迭代结束后，[0,j+1)范围内子数组的元素均为升序，不变式成立。
终止： j不断递增，当j == n 时，所有数组的元素均被遍历处理，此时[0,n)为升序，不变式成立。