循環不變式——從理論上證實算法的正確性

時間 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 循環終止的條件是，因此循環結束時，。在循環不變式中，咱們將用代替，也就是子數組仍是原來位置在的元素而且是排好序的。所以算法正確。