使用循環不變來證明合併排序的正確性（初始化，維護，終止）

Question

你將如何去驗證合併排序的正確性，以及對循環不變量的推理嗎？唯一可以想象的是，在合併步驟中的子陣列（不變量）當組合時保持它們的狀態，即它們在每個合併步驟中再次被分類。但是我不知道我是否正確地進行了處理。我對Loop不變量和東西沒有太多的理解。有人能給我這個啓發嗎？說明在每個階段

一）初始化 二）維護 c）解僱

非常感激會發生什麼！

Answer 1

僞碼，歸併排序

MERGE-SORT（A，P，R）

1 if p < r 
    2 then q <-- [(p + r)/2] 
    3   MERGE-SORT(A, p, q) 
    4   MERGE-SORT(A, q + 1, r) 
    5   MERGE-SORT(A, p, q, r) 

MERGE-SORT（A，P，Q，R）

1 n1 <-- q - p + 1 
    2 n2 <-- r - q 
    3 create arrays L[1 ... n1 + 1] and R[1 ... n2 + 1] 
    4 for i <-- 1 to n1 
    5  do L[i] <-- A[p + i - 1] 
    6 for j <-- 1 to n2 
    7  do R[j] <-- A[q + j] 
    8 L[n1 + 1] <-- infinite 
    9 R[n2 + 1] <-- infinite 
    10 i <-- 1 
    11 j <-- 1 
    12 for k <-- p to r 
    13  do if L[i] <= R[j] 
    14   then A[k] <-- L[i] 
    15    i <-- i + 1 
    16   else A[k] <-- R[j] 
    17    j <-- j + 1 

我們嘗試對兩堆牌進行排序，但是我們避免檢查在每個基本步驟中堆是否爲空，並且我們使用無限作爲定位卡來簡化我們的代碼。所以，當哨兵卡infinie暴露時，它不能是較小的卡，除非這兩個樁暴露了它們的哨卡。但一旦發生這種情況，所有非哨兵卡都已放置在輸出樁上。由於我們事先知道，確切地說r - p + 1卡將被放置在輸出堆上，所以一旦我們執行了許多基本步驟，我們就可以停止。

• 循環不變：

  • 初始化：之前的循環的第一次迭代，我們有k = p，這樣子陣A[p ... k - 1]是空的。這個空的子陣列包含L和R的最小元素，並且從i = j = 1開始，L [i]和R [j]都是它們陣列中最小的元素，它們沒有被複制回A.

  • 維護：爲了看到每次迭代保持循環不變，讓我們首先假設l [i] < = R [j]。然後L [i]是尚未複製回A的最小元素。因爲A[p ... k - 1]包含k - p最小元素，所以在第14行將L [i]複製到A [k]後，子陣列A[p ... k]將包含k - p + 1最小元素。遞增k（在for循環更新中）和i（在第15行中）爲下一次迭代重新建立循環不變量。如果改爲L [i]> R [j]，則第16-17行執行適當的操作以保持循環不變。

  • 終止：終止時，k = r + 1。通過循環不變量，子陣列A[p ... k - 1]（其爲A[p ... r]）包含L[1 ... n1 + 1]和R[1 ... n2 + 1]的k - p = r - p + 1最小元素，按排序順序。陣列L和R一起包含n1 + n2 + 2 = r - p + 3元素。除了最大的兩個元素之外，所有元素都被複制到A中，而這兩個最大的元素是哨兵。