1 初始化

循环的第一次迭代之前，它为真；

2 保持

如果循环的某次迭代之前它为真，那么下次迭代之前它仍然为真；

3 终止

在循环终止时，不变式为我们提供了一个有用的性质，该性质有助于证明算法是正确的。

4 例子解读

# 插入法伪代码
INSERTION-SORT(A)
1 for j=2 to A.length
2    key = A[j]
3    //insert A[j] into the sorted sequence A[1...j-1]
4    i=j-1
5    while i>0 and A[i]>key
6        A[i+1] = A[i]
7        i = i-1
8    A[i+1] = key

• 初始化： 首先证明在第一次循环迭代之前（当j=2时），循环不变式成立。所以子数组A[1..j-1]仅由单个元素A[1]组成，很明显子数组就是排好序的。

• 保持：第二步，证明每次迭代保持循环不变式。非形式地，for循环体的4~7行将A[j-1],A[j-2],A[j-3]等向右移动一个位置，直到找到A[j]的适当位置，第8行将A[j]插入该位置，此时A[1..j]已经排好序了，那么对for循环的下一次迭代增加j将保持循环不变式；

• 终止：最后研究在循环终止时发生了什么。导致for循环终止的条件是j>A.length=n，因为每次循环迭代j增加1，那么必有j = n+1。在循环不变式的表述中将j用n+1代替，我们有： 子数组A[1...n]由原来在A[1...n]中的元素组成，但已按序排列。因此我们推断整个数组已排序，算法正确。