关于"循环不变式"是什么？

只爱你一人

近段时间在啃accelerated C++接触到一个叫循环不变式的东西,看了半天,上网找了半天,都没给说清楚循环不变式是个什么东西,只说是用于检查循环的正确性的,我的理解是循环不变式于while循环来说是就是就是它的条件语句呢?

仰望天上的光

不是。
条件语句和不不变式没有任何关系。

循环不变式确保每次循环后都得到正确的状态，却不保证循环能结束。正确的条件语句保证循环能结束。

所以不变式+条件语句  就可以得到循环结束后的正确状态。

只爱你一人

仰望天上的光 发表于 2012-4-9 22:56

                               
登录/注册后可看大图

不是。
条件语句和不不变式没有任何关系。

那我怎么才能找到循环不变式呢？它是否在程序段里面？难道它只是一个验算方法而以，并不存在于代码里吗？

仰望天上的光

只爱你一人 发表于 2012-4-9 23:09

                               
登录/注册后可看大图

那我怎么才能找到循环不变式呢？它是否在程序段里面？难道它只是一个验算方法而以，并不存在于代码里吗？

循环不变式当然存在于代码里，事实上一般是先找出循环不变式，再写代码的。
循环体里做的事情归纳起来就是两个：
1.破坏不变式
2.恢复不变式

只爱你一人

仰望天上的光 发表于 2012-4-9 23:23

                               
登录/注册后可看大图

循环不变式当然存在于代码里，事实上一般是先找出循环不变式，再写代码的。
循环体里做的事情归纳起来就 ...

取accelerated C++第２章的例子片段：输出未知行数问题，(变量　r　就是已经输出的行数，rows>=3)

　　　int r =0;                          这条语句就是“不变式”，它表示当前已经输出的行数，因为还没进入循　　　　　　　　　　　　　　　　　　　　　　　环，所以什么也没输出，即r=0,不变式为真
　　　while ( r != rows ) {
             cout<<endl;　　　　　　　进入循环后，这条语句输出了一行，即破坏不变式，不变式为假
             ++r;　　　　　　　　　　　r自增１,即恢复不变式，不变式又为真
         }
请问是这样吗？

仰望天上的光

只爱你一人 发表于 2012-4-10 00:05

                               
登录/注册后可看大图

取accelerated C++第２章的例子片段：输出未知行数问题，(变量　r　就是已经输出的行数，rows>=3)

　　 ...

是的，由你所说的不变式可以得出结论：每次循环结束“当前已经输出了r行”这个不变式总是成立的。但这里并没有给出该循环什么时候结束。

这个要根据循环条件r!=row
将其取反，得到r==row
所以循环结束的时候r==row
结合前面的不变式得到：循环结束的时候。已经输出了row行

只爱你一人

仰望天上的光 发表于 2012-4-10 00:18

                               
登录/注册后可看大图

是的，由你所说的不变式可以得出结论：每次循环结束“当前已经输出了r行”这个不变式总是成立的。但这里并 ...

终于搞明白了！谢谢！