循环不变式——从理论上证实算法的正确性

时间 2019-12-01

标签循环不变理论上证实算法正确性繁體版

原文原文链接

最近在看《算法导论》这本书，在它的第二章出现了一个很是有意思的概念——循环不变式（Loop Invariant）。一言以蔽之，提出循环不变式的目的是为了从理论上证实某个算法是正确的。算法

那么，如何从理论上证实某个算法是正确的？

说实话我之前没有思考过这个问题。习惯养成的缘由，我在调试代码时，老是试各类各样的输入和查看对应的输出以保证整个程序是正确的。并非说这样是错误的，而是指这个习惯让我没有去思考从理论上证实算法正确性这条路。若是只是盲目地多试几个输入的话，就好像让电脑用算术去证实哥德巴赫猜测同样，是很是不优雅的。你能够证实很是大的数知足哥德巴赫猜测，但你永远也没法说哥德巴赫猜测是对的。数组

其实从理论上证实算法的正确性简单得使人惊讶，这个过程跟数学概括法一模一样。咱们先来看看数学概括法是怎样的。oop

数学概括法有这么两步spa

奠基基数：通常验证n取最小项时成立
推导：假设时成立，经过推导能够证实时也成立。

咱们来举个例子调试

$1+2+3+\cdots+n = \frac{n(n+1)}{2}$

等差数列求和公式如何进行求证呢？code

验证该公式在时成立。即有左边，右边= $\frac{1(1+1)}{2}=1$ ，因此这个公式在时成立。排序

须要证实假设时公式成立，那么能够推导出时公式也成立。步骤以下：get

假设时公式成立，即 $1+2+\cdots+m=\frac{m(m+1)}{2}$ （等式1）

而后在等式两边同时分别加上获得 $1+2+\cdots+m+(m+1)=\frac{m(m+1)}{2}+(m+1)$ （等式2）这就是时的等式。咱们下一步须要根据等式1证实等式2 成立。经过因式分解合并，等式2的右边 $=\frac{m(m+1)}{2}+\frac{2(m+1)}{2}=\frac{(m+1)(m+2)}{2}=\frac{(m+1)[(m+1)+1]}{2}$ 也就是 $1+2+3+\cdots+(m+1)=\frac{(m+1)[(m+1)+1]}{2}$

这样咱们就完成了由成立推导出成立的过程，证毕。数学

结论：对于任意天然数n，公式均成立。it

那么接下来就让咱们用相似于数学概括法证实公式的方法来证实循环不变式以证实算法的正确性。

咱们以插入排序为例子（升序，在这里用伪代码来表示，数组的下标是）：

INSERTION-SORT(A)
  for j = 2 to A.length
    key = A[j]
    i = j-1
    while i>0 and A[i] > key
      A[i+1] = A[i]
      i = i-1
    A[i+1] = key
复制代码

就好像 $1+2+3+\cdots+n = \frac{n(n+1)}{2}$ 这样的公式同样，在此咱们能够为插入排序提出一个循环不变式：在每次for循环迭代开始以前，子数组仍是原来位置在的元素而且已经排好序了。

那么就跟数学概括法证实公式同样，咱们须要两步来证实它的正确性：

初始化（Initialization）：循环的第一次迭代以前循环不变式为真。
保持（Maintenance）:假设循环的某次迭代以前为真，那么能够推导出下次迭代以前它依然为真。

但由于咱们须要循环不变式来证实算法的正确性，咱们须要着重看循环结束时的状况，那么就引出了咱们须要证实循环不变式的第三个性质：

终止（Termination）:在循环终止时，不变式为咱们提供一个有用的性质，该性质有助于证实算法是正确的。

那么让咱们来看看是怎样具体证实的：

初始化：循环的第一次迭代以前（），由单个元素组成，因此循环不变式成立。
保持：假设时，循环不变式成立，也就是，子数组是原来位置在的元素而且已经排好序了。当前这个循环迭代会不断左移直到找到第一个比它小的元素。当这个循环迭代结束以后，仍是原来位置在的元素而且是排好序的。因此推导出时，循环不变式也成立。
终止：致使 for 循环终止的条件是，因此循环结束时，。在循环不变式中，咱们将用代替，也就是子数组仍是原来位置在的元素而且是排好序的。所以算法正确。

你会发现利用循环不变式来证实算法的正确性是如此得简单和优雅。