マージソートの正当性をループ不変条件の推論で証明する方法を教えてください。マージステップは、サブアレイ（不変量）を結合して状態を維持すると、つまり、それぞれのマージステップでソートされます。しかし、正しく処理されているかどうかはわかりません。ループ不変量やものについてはあまり理解していません。これで私を啓発することはできますか？各フェーズループ不変式を使用してマージソート（初期化、メンテナンス、終了）の正確性を証明する
a）の初期化 b）のメンテナンス c）の終了
多くの義務で何が起こるかを説明！ソート
MERGE、マージソートのための
は擬似コード（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
カードの2つのパイルをソートすることはできますが、各基本ステップでパイルが空であるかどうかを確認することは避け、コードを単純化するためにセンチネルカードとして無限を使用します。したがって、センチネルカードのインフィニティが公開されるたびに、両方のパイルにセンチネルカードが公開されていない限り、それはより小さなカードになることはできません。しかしそれが起こると、すべての非センチネルカードは既に出力ファイルに置かれています。正確にr - p + 1のカードが出力ファイルに置かれることを事前に知っているので、多くの基本ステップを実行すると停止できます。
ループ不変：
初期化：そのサブアレーA[p ... k - 1]が空であるので、ループの最初の反復に先立って、我々は、k = pを持っています。この空の部分配列にはLとRの最小要素のk - p = 0が含まれ、i = j = 1以来、L [i]とR [j]の両方は、配列にAにコピーされていない配列の最小要素です。
メンテナンス：各反復がループ不変量を維持することを知るために、まずl [i] < = R [j]と仮定する。 A[p ... k - 1]には、最小要素がk - pであるため、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要素を含んでいます。 2つの最大要素を除いてすべてがAにコピーされており、この2つの最大要素はセンチネルです。