循环不变式

//invariant:we have written r rows so far.
int r=0;
//setting r to 0 makes the invariant true
while(r!=rows)
{
//we can assume that the invariant is true here
//writting a row of output makes the invariant false
std::cout<<std::endl;
//incrementing i makes the invarian true again
++r;
}

上面这个循环很简单，就是要使循环体执行n次，但是从中我们可以发现一个循环不变式，那就是“we have written r rows so far”，循环不变式要成立只需当1while开始之前循环不变式成立，2当我们执行到循环体尾部时循环不变式成立。当我们将i设为0时，此时我们一次都没有循环显然循环不变式成立，因为我们此时还没有输出一行，当我们输出一行后，此时循环不变式即为假了，但是++r使得循环不变式又为真了，因此我们可以得出此循环不变式是成立的，当最后跳出循环体时，r==rows了，即我们已经输出了rows行了！

PS:从Accelerated C++上面看到一个概念，真的是一本不错的书。