其中为了证明某条性质成立，需要证明一个基本情况和一个归纳步
循环的第一次迭代之前，他为真。
证明第一次迭代之前不变式成立对应于基本情况
如果循环的某次迭代之前它为真，那么下次迭代之前它仍为真
证明从一次迭代到下一次迭代不变式成立 对应于归纳步
在循环终止时，不变式为我们提供一个有用的性质，该性质有助于证明算法是正确的。
终止性不同于我们通常使用数学归纳法的做法，在归纳法中，归纳步骤是无限地使用的，这里当循环终止时，停止"归纳”。