アルゴリズムの正確性証明方法1:サイクル不変量

前の文章でアルゴリズムの正確性の概念とその役割を書きました.次はサイクル不変量のアルゴリズムの正確性証明における使い方を書きます.
サイクル不変量(loop invariant)
循環を利用するアルゴリズムでは,循環不変量によってその正確性を証明できる.いわゆる循環不変量とは、循環全体の過程で不変の性質を維持することであり、次の3つの場合には同じままでなければならず、その性質は循環終了後にアルゴリズムの正しさを証明することができる.

初期化(循環初期化後、循環条件試験前)

反復(第n回の反復後、第n＋1回の反復前)

終了(サイクル終了、つまりサイクル条件がfalseと判断された場合)

例
次に、並べ替えの中のmerge関数について、サイクル不変量を説明します.

1: int* merge(int* sld, int* srd, int lc, int rc)
2: {
3:     int tc = lc + rc;
4:     int* md = (int*) malloc(sizeof(int) * (tc));
5: 
6:     int li = 0; //          
7:     int ri = 0; //          
8:     for (int i = 0; i < tc; ++i)
9:     {
10:         if (li >= lc) //        
11:             md[i] = srd[ri++];
12:         else if (ri >= rc) //        
13:             md[i] = sld[li++];
14:         else if (sld[li] <= srd[ri]) //        ，         
15:             md[i] = sld[li++];
16:         else
17:             md[i] = srd[ri++];
18:     }
19: 
20:     return md;
21: }

まずこの関数の役割を説明します.sndとsrdは並べ替えられた配列で、サイズはそれぞれlcとrcで、循環tc(lc＋rc)はそれらの元素を2回ずつ比較して、新たに割り当てられた配列mdにコピーします.このアルゴリズムの正確性をどう証明しますか?
まず循環不変量を設定してから、8-18行の循環が以上の3つの状況でこの循環不変量を満たすかどうかを確認します.
md[0-i]の元素はsd[0-li]とsrd[0-ri]の元素の和の順序付けの結果です.

初期化はこのときi=0、li=0、ri=0となるので、md[0]、sd[0]の大きさはいずれも0となり、サイクル不変量を満たす.

反復は、SLd[li]とsrd[lr]を比較して小さいmd[i]にコピーしなければならない.このときmd[0-i]はmd[0-i]+min(sd[li],srd[ri])であり、liまたはlrを1だけ増加させて、iを増加させて循環不変量を満たす.

サイクル終了条件はi>=tc(lc+rc)であり、このときmd[0-tc]の要素はsd[0-lc]とsrd[0-rc]の要素と順序付けされた結果である.
終了時に循環不変量が有益な情報を与えてくれました.この時mdはすでにsdとsrdの全部の要素を統合して並べ替えました.これによってアルゴリズムの正しさを証明しました.