循环不变式（loop invariant）主要来帮助我们来理解算法的正确性。
对于循环不变式，必需证明它的三个性质：
初始化：它在循环的第一轮迭代开始之前，应该是正确的。
保持：如果在循环的某一次迭代开始之前它是正确的，那么，在下一次迭代开始之前，它也应该保持正确。
终止:当循环结束时，不变式给了我们一个有用的性质，它有助于表明算法是正确的。
关循环不变式与数学归纳法有些类似，但是与它的常见用法不同：在归纳法中，归纳的步骤是无穷地使用的；而在这儿，当循环结束时， 即终止“归纳”。
霍纳规则的正确性：
以下代码片段实现了用于计算多项式
的霍纳规则
1 y=0
2 i=n
3 while i>=0
4 do y=a(i)+x*y
5 i=i-1
2 i=n
3 while i>=0
4 do y=a(i)+x*y
5 i=i-1
以下给出的是针对第3~5行中while循环的一个循环不变式：
初始化：当循环第一次的时候，n=n-1,y=a(n)
保持：当i=n-j与i=n-j-1 的时候，y(n-j-1)=a(n-j-1)+x*y(n-j)
终止： 当循环结束的时候，