迴圈不變量

2021-07-30 21:13:17

透過迴圈不變量(Loop Invariant)可以推理演算法的正確性。

迴路不變量透過證明三個演算法的屬性來確保演算法的正確性：

初始條件（Initialization)

證明迴圈開始前，條件為真。

迭代後，條件仍成立 （Maintain)

證明每個迴圈迭代（跑一圈）結束後，我們關注的條件仍然為真。也就是說迴圈的迭代會維護、保持該條件。

終止條件（Termination)

證明當迴圈終止（跑完最後一圈）後的結果符合演算法的要求。

以Insertion sort為例

偽代碼(Pesudocode)

INSERTION_SORT(input) {
	for i from 2 to input.length { // 從索引2開始
		key = input[i]
		j = i - 1
		while j > 0 and input[j] > key { // 當input[j]比key還大時...
			input[j + 1] = input[j] // 將input[j]複製到input[j+1]，也就是將input[j]往右移
			j = j - 1 // 將j指摽往左移動，以尋找更小的值來與key做比較
		}
		input[j+1] = key
	}
}

* 陣列索引由1開始（而非0)

用迴圈不變量證明Insertion sort的正確性

insertion sort裡面有個for迴圈，而且也只有個for loop。當這個for loop結束時，insertion sort就結束了。若我們能用迴圈不變量證明這個for loop能做到排序的目的，就等於這個insertion sort演算法是正確的

初始條件（Initialization）

長度為1的陣列無論數字大小，一定是照順序排的(sorted)。

我們的for loop由索引2開始。這時以input[1]，單一數字構成的陣列是有照順序的(sorted)

迭代後，條件能成立（Maintain)

for loop裏面有while loop。

while loop在input[j]大於Input[i]時持續將input[j]往後移動 input[j+1] = input[j]。

根據初始條件：

  1. 以input[1] 單一數字組成的陣列可視為已被排序的陣列 (n = 1)
  2. 若迴圈不變量的Maintain屬性成立，則迴圈迭代後input[1~i] 依然可視為已被排序的陣列 (n = k, n = k + 1)

因此無論i為何，迴圈迭代前 input[1~(i-1) 已被排序。迴圈迭代後input[1~i]

$$input[1 \text{\textasciitilde}i] \text{ is sorted} \text{ (A)} $$

兩個情況會造成while loop終止：

  1. j <= 0
  2. input[j] <= input[i]

接下來探討while loop結束後的input[j+1] = key 的效果

因為key = input[i]所以input[j+1] = key意味著input[j+1] = input[i]

當while loop因為j ≤ 0而中止後，因為不再對j的值做調整，j必然0。 則input[j+1] = input[i]意味著input[1] = input[i]。

也就是說while loop找不到任何一個input[j]是比input[i]小（或等於）的。此時input[i]是input[1~i]中最小的值。因此將input[i]依照順序放置在input[1]。

因為(A)，所以input[2~i]也是照順序排的，因此input[1~i]仍然保持正確的順序 □

當while loop因為input[j] ≤ input[i]而終止時，input[j + 1] = input[i]將input[i]插入在input[j]的右側

$$\brace {...,\space input_j,\space input_{j+1} = input[i],\space...}$$

因為(A)，input[1~j]有照順序排input[j+2~i]也有照順序排，因此插入後input[1~i]有照順序排 □

因此for loop結束後，input[1~i]為排序過的陣列。

終止條件（Termination)

我們要在終止條件這個屬性證明迴圈結束後的效果對我們的目的是有用的。

排序演算法的目的是將輸入的陣列排序。

由於Maintain屬性，我們知道當loop完成i的迭代時。input[1~i]完成排序；當loop完成i+1的迭代後input[1~(i+1)]完成排序。

由於for loop從i = 2跑到i = input.length，因此當for loop終止時input[1~(input.length)]完成排序，即input陣列完成排序。

參考資料

演算法導論 第二章

後記