循环不变式的思想及其应用

　　循环不变式（loop invariants）不只是一种计算机科学的思想，准确地说是一种数学思想。在数学上阐述了通过循环（迭代、递归）去计算一个累计的目标值的正确性，属于基础数学的范畴，而且在计算机上也应用广泛。初次见到这个词是在《算法导论》，在第二章描述了这个思想和正确性，后来又在《编程珠玑》上再次重逢，不得不说是一种缘分。决定把自己的一些认识记录下来，用于阐述和传播这种优秀的基础方法。
　　循环不变式主体是不变式，也就是一种描述规则的表达式。其过程分三个部分：初始，保持，终止。
　　1、初始：保证在初始的时候不变式为真。
　　2、保持：保证在每次循环开始和结束的时候不变式都为真。
　　3、终止：如果程序可以在某种条件下终止，那么在终止的时候，就可以得到自己想要的正确结果。

　　在这三个部分中，前两个是条件，最有一个是结论。看起来很浅显易懂，小学生就能明白的道理，但是道理明白不代表会使用。下面就举两个例子。
　　
　　例子1、
　　问题：给出二分查找的实现,函数原形 int bsearch(int num[], int count, int goal); num是保存已经从小到大排序好的数字，count是数组元素个数，goal是待查找的数字；若查找成功则返回元素的下标，否则返回-1。
　　分析：二分查找的原理很简单：把数组分成三份，中间一份只有一个元素，其他两份个数基本相同，如果中间的元素等于目标值，就返回它的下标；如果大于，则去前半数组继续执行二分查找；如果小于，则去后半数组；直到数组没有元素为止。这是循环不变式的一个计算机算法应用，我们可以按照它的规则来做，我们的不变式就是：当前数组不为空；循环结束条件是：当前数组为空或找到目标元素。
　　代码:

int bsearch(int num[], int count, int goal)
{
    //检测初始时不变式的真值
    if ( (num == NULL) || (count <=0) )
        return -1;
    //准备循环
    int l = 0;//数组左端下标
    int r = count -1;//数组右端下标
    int m; //数组中间下标
    //循环开始
    while(r>=l)//r>=l就是不变式，代表数组中有元素
    {
        m = (r+l)/2; //计算中间位置
        if (a[m] == goal)//分支1，中间元素是目标元素
            return m;//则返回
        else if(a[m] > goal) //分支2，中间元素大于目标元素
            r = m - 1;//把数组右端标志放到m的前面一个元素
        else//分支3，中间元素小于目标元素
            l = m +1;//把数组左端标志放到m的后面一个元素
    }
    //运行到这里表示没有找到目标元素
    return -1;
}

　　代码可以进一步优化：

int bsearch(int num[], int count, int goal)
{
    int l = 0;
    int r = count -1;
    int m = (r+l)/2;
    for(num != NULL; r>=l; m = l+r/2)
    {
        if (a[m] > goal)        r = m - 1;
        else if (a[m] < goal)    l = m +1;
        else                    return m;
    }
    return -1;
}

　　小结：上述代码是直接手写，没有经过上机测试，由于遵循了循环不变式的要求，我有信心不出现逻辑错误，倘若真出现了错误，那么就一定是我没有遵循循环不变式的要求。其实二分法作为一种简单灵活而又高效的算法在1946年就被人提出来了，但是第一个正确的算法确实在1962年发表的，期间这么多年都没有人发布正确的算法，有人漏掉元素导致结果错误，有人重复计算导致死循环。其原因在于逻辑不够严密，没有正确的方法去指导他们写这个算法，但是有了循环不变式的帮助，一切变得明朗了许多。

　　例子2、
　　问题：有数列a[n],n属于自然数，a[1] = 2，递推公式1：a[i] = 2/(a[i-1]+1),i>1,i属于自然数。求通向公式
　　分析：这个问题求数列的通向公式，是一个递归式，可用数学归纳法：先分析数列规律，再用假设公式带入k，然后计算a[k]的值并验证，继而推广到a[n]。
　　解题：

　　第一步，找规律：
　　a[1] = 2
　　a[2] = 2/(2+1) = 2/3
　　a[3] = 2/(2/3+1) = 6/5
　　a[4] = 2/(6/5+1) = 10/11
    则根据规律设递推公式2：a[i] = 2a[i-1]的分母/(2a[i-1]的分母+(-1)^i),i>1,i属于自然树。
    
　　第二步，根据规律列出a[k]公式：
　　i=1,a[i] = 2;
　　i=2,a[i] = 2/(2+(-1)^2) = 2/(2+1) 

　　i=3,a[i] = 2(2+(-1)^2)/(2(2+(-1)^2)+(-1)^3)= 2(2+1)/(2(2+1)-1)
　　i=4,a[i] = 2(2(2+(-1)^2)+(-1)^3)/(2(2(2+(-1)^2)+(-1)^3)+ (-1)^4) = 2(2(2+1)-1) /(2(2(2+1)-1)+1)
    i=k,a[i] = 2(…(2(2(2+(-1)^2)+(-1)^3)+…)+(-1)^(k-1))/(2(…(2(2(2+(-1)^2)+(-1)^3)+…)+(-1)^(k-1))+(-1)^(k))
    
    第三步化简a[k]：

    　　由于a[k]分母中最深入的括号有k层，所以第一个+前面的2的系数2^(k-2),第一个+后面的(-1)^2的系数是2^(k-2),这个看作循环不变式的初始条件，中间循环第二个+后面的(-1)^3系数为2^(k-3),一直到最有一个+后面的(-1)^k系数为2^(k-k),总共有k-1个带有(-1)的项。在这些项目中，由于初始化计算正确，中间步骤正确，那么最后结果一定正确。
　　若k为奇数：
　　a[k]分母=2^(k-1)+2^(k-2)-2^(k-3)+….-2(k-k)，利用等比数列通向和公式求得=2^(k-1)+ (2^k-2)/3 – (2^(k-1)-1)/3 = (2^(k+1)-1)/3
　　则a[k]分子= (2^(k+1)-1)/3+1，a[k] = (2^(k+1)+2)/(2^(k+1)-1)
　　若k为偶数：a[k] = (2(k+1)-2)/(2^(k+1)+1),过程同上，略。
　　a[k] = (2(k+1)-2(-1)^k)/(2^(k+1)+(-1)^k)
　　
　　第四步，归纳证明
　　过程略

　　小结：在这个题目里面最难的就是根据那第三步，如果使用第二步得到的中间带省略号的公式。这时候就需要循环不变式来帮忙，只要初始值正确（正确计算最内部+两侧式子的系数），循环过程无误（正负号交替，系数依次/2），循环可以结束（共循环k-1次），那么结果就是正确的，可以放心大胆地继续划简，最后得到正确结果。

　　总结：循环不变式使用特点
　　1、在循环，迭代，递归等用上次结果作为下次初始值的累计过程都可以准确无误的使用。
　　2、在循环不变式三要素，初始，保持，结束。初始一定要正确，循环的时候也要保证不变式为真，循环一定要可以结束才能得到正确结果。其中后两条比较容易疏漏，解题时要慎而又慎严谨对待循环中不变式和结束条件。
　　3、可以把三要素再进行一次转化，使之更适合计算机程序：一次循环开始时候不变式为真，一次循环完毕时为真，总循环可以结束，结果必定正确。