shiro

循环不变式
必须被证明的三条性质: 初始化:循环的第一次迭代之前,它为真。保持:如果循环的某次迭代之前它为真,那么下次迭代之前...
扫描右侧二维码阅读全文
29
2018/08

循环不变式

必须被证明的三条性质:

初始化:
循环的第一次迭代之前,它为真。
保持:
如果循环的某次迭代之前它为真,那么下次迭代之前它仍为真。
终止:
在循环终止时,不变式为我们提供一个有用的性质,该性质有助于证明算法是正确的。


当前两条性质成立时,在循环的每次迭代之前循环不变式为真。这里利用了数学的数学归纳法,其中为了证明某条性质成立,需要一个基本情况和一个归纳步。基本情况相对于初始化,归纳步相对于保持。
第三条性质可能是最重要的,因为将使用循环不变式来证明正确性。

以上的内容源自算法导论的第二章,这是一种思想,一种保证程序正确性的一种思想。


接下来以书本的例子插入排序算法为例子

例如:
这里有一个数组A={31, 41, 59, 26, 41, 58}

  • 31, 41, 59, 26, *41, 58
  • 31, 41, 59, 26, *41, 58
  • 26, 31, 41, 59, *41, 58
  • 26, 31, 41, *41, 59, 58
  • 26, 31, 41, *41, 58, 59
//CPP
void Insertion_Sort(std::vector<int> &vec) {
    for(auto j = 1; j < vec.size(); ++j){
        int key = vec[j];
        int i = j - 1;
        while(i > -1 && vec[i] > key){
            vec[i+1] = vec[i];
            --i;
        }
        vec[i+1] = key;   
    }
}

初始化:可以看到第一次循环迭代之前(j = 1) < vec.siez()这个条件是成立的。即初始条件成立。
保持:这个阶段的代码可以看到for循环之中,每次迭代基于上一次迭代的正确置换,而第一次条件是成立的,所以之后数据排序顺序也是正确的。
终止:最后当j = vec.size()时,循环终止,产生一个结果,这个结果时基于之前的两个性质得到的最终结果,在例程里显示的就是最后的数据是升序排列的。

其实自己写程序的时候大部分会忽略第一第二性质,只完成第三性质,虽然程序能够通过,不过代码的质量往往很差,且坎坷。

遵循循环不变式这个思想,能够写出严谨且准确质量高的代码。


(以下为他人总结)
总结:循环不变式使用特点:

  • 在循环,迭代,递归等用上次结果作为下次初始值的累计过程都可以准确无误的使用。
  • 在循环不变式三要素,初始,保持,结束。初始一定要正确,循环的时候也要保证不变式为真,循环一定要可以结束才能得到正确结果。其中后两条比较容易疏漏,解题时要慎而又慎严谨对待循环中不变式和结束条件。
  • 可以把三要素再进行一次转化,使之更适合计算机程序:一次循环开始时候不变式为真,一次循环完毕时为真,总循环可以结束,结果必定正确。
Last modification:August 30th, 2018 at 01:08 pm
If you think my article is useful to you, please feel free to appreciate

Leave a Comment