循环不变式：算法中基础概念的明晰

循环不变式

循环不变式主要用来辅助我们理解算法的正确性，对于循环不变式，必须证明它的三个性质

初始化：它在循环的第一轮迭代开始之前，应该是正确的。 保持：如果在某一次循环迭代开始之前是正确的，那么在下一次迭代开始之前，它也应该保持正确（假设当循环变量等于k时符合，再看执行一遍循环体后是否还符合循环不变式）。 结束：当循环结束时，不变式给了我们一个有用的性质，它有助于表明算法是正确的（这一步是和数学归纳法不同的一点，用循环不变式则更进一步，数学归纳法到这里就得出了一个关系式就结束，而用循环不变式，不但要先确保一个正确的关系式，还要看最后循环结束时，循环变量最后等于多少，根据循环不变式推导是否符合自己的要求。）。 编写循环时，让每次循环都成立的逻辑表达式称为循环不变式（loop invariant）。 注意：每个循环都可以找到一个循环不变式，我们可以通过这个循环不变式证明循环迭代的正确性。

案例分析

 利用循环不变量证明下述计算a^n算法的正确性：

Exp(a,n)

1    i<--1

2    pow<--1

3    while i<=n do

4            pow<-pow*a

5            i<--i+1

6    return pow

初始化：循环开始之前，i=1，pow=a^(i-1)=1，等式成立，所以迭代之前循环不变式成立。

保持：假设i=k的时候循环不变式成立,此时还未执行循环语句，循环不变式成立，即a^(k-2)=1，则在循环中执行的pow=pow*a,那么pow=a^(k-1)。即在迭代过程中，循环不变式保持成立。

终止：当k=n+1时，循环终止，此时pow=a^n。所以算法终止时，得到的是一个正确的结果，返回了a的n次幂。

、