数学归纳分析程序正确性

1 数学归纳

先看个数学证明问题:

s(n) = 1+2+3+...n = ((n+1) * n) / 2, 证明公式对任意整数n(n >= 0)都成立

证明：

设置断言 G(n): 0到n的整数之和s(n) = ((n + 1) * n) / 2

步骤1： 基底的证明

s(0) = ((0+1)*0) / 2 = 0，G(0)成立

步骤2：归纳的证明 

先假设 G(k)成立，可得到：

s(k) = 0+1+2...+k = ((k+1) * k) / 2

则：

s(k+1) = s(k) + k+1 = ((k+1) * k) / 2 + ((k+1) * 2) / 2 = ((k+1) * (k+2)) / 2

等式成立，推出G(k) 成立，则G(k+1)也成立

通过步骤1，步骤2证得断言G(n)是正确的

上面求证过程，就运用到了 数学归纳 思想。

2 运用数学归纳分析计算机程序正确性

求fibonacci数列([0, 1 , 1,  2,  3,....ai, a(i+1), a(i)+a(i+1)])第i项(i >= 0)

常规写法如下

staticintfib(inti){
    if(i ==0) {
      return0;
    }
    if(i ==1) {
      return1;
    }

   inttmp;
    inta =0;
    intb =1;
    int$i =2;

    while($i <= i) {
      $i++;
      tmp = a;
      a = b;
      b = tmp +b;
    }

    returnb;
}

思考：对任意的输入i, 怎么证明代码输出结果都是正确的? ......

把上面代码结构调整为下面这样,只要水为了方便分析，逻辑和上面代码等效

staticintfib(inti){
     int[] L =newint[] {0,0,1};
     if(i ==0) {
       returnL[1];
     }
     if(i ==1) {
       returnL[2];
     }
     while(L[0] <= i) {
       next(L)；
     }
     returnL[2];
  }

  staticintnext(int[] L){
     inttmp;
     inta = L[1];
     intb = L[2];
     tmp = a;
     a = b;
     b = b + tmp;
     // 计算下一次循环需要的变量
     L[0] = L[0] +1;
     L[1] = a;
     L[2] = b;

     returnL[2];
  }

用上面的 数学归纳思想 ，分析下程序是否正确。

证明：

设置断言 M(i): L(i) = [i, fib(i-2), fib(i-1)]（i > 2，fib(i) 表示fibonacci第i项）

步骤1： 基底的证明

i = 2时， L(2) = [2, 0, 1]；由fibonacci前3项为[0, 1, 1], 可知， L(2)成立 ;

步骤2：归纳的证明

由程序代码可知：L(k+1) = [k+1, L(k)[2], L(k)[1]+L(k)[2]],   假设M(k)成立，则：

L(k) = [k, fib(k-2), fib(k-1)]，所以：

L(k+1)=[k+1, fib(k-1), fib(k-1)+fib(k-2)] = [k+1, fib(k-1), fib(k)],

推出M(k)成立时，M(k+1)成立

所以断言正确

通过上面证明，可以得出，输入为i, 当循环结束时 $i = i + 1, 此时 L($i) = [i+1, fib(i-1), fib(i)],

所以L($i)[2] 为fibonacci第i项, 输出正确 。

问题：证明下面二分查找程序是否正确？

staticbooleansearch(int[] a,inttarget){
    intleft =0;
   intright = a.length -1;
    while(left < right) {
      intmid = (left + right) /2;
      if(a[mid] > target) {
        right = mid +1;
      }
      if(a[mid] < target) {
        left = mid +1;
      }else{
        returntrue;
      }
    }
    returnfalse;
  }