数学归纳分析程序正确性

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)



常规写法如下

static int fib(int i) {
    if (i == 0) {
      return 0;
    }
    if (i == 1) {
      return 1;
    }
    int tmp;
    int a = 0;
    int b = 1;
    int $i = 2;
  
    while ($i <= i) {
      $i++;
      tmp = a;
      a = b;
      b = tmp +b;
    }
    return b;
}



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



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

 static int fib(int i) {
     int[] L = new int[] {0, 0, 1};
     if (i == 0) {
       return L[1];
     }
     if (i == 1) {
       return L[2];
     }
     while (L[0] <= i) {
       next(L)；
     }
     return L[2];
  }
  static int next(int[] L) {
     int tmp;
     int a = L[1];
     int b = L[2];
     tmp = a;
     a = b;
     b = b + tmp;
     // 计算下一次循环需要的变量
     L[0] = L[0] + 1;
     L[1] = a;
     L[2] = b;
    
     return L[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项, 输出正确 。



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

static boolean search(int[] a, int target) {
    int left = 0;
    int right = a.length - 1;
    while (left < right) {
      int mid = (left + right) / 2;
      if (a[mid] > target) {
        right = mid + 1;
      }
      if(a[mid] < target) {
        left = mid + 1;
      } else {
        return true;
      }
    }
    return false;
  }