ループ不変

コンピュータサイエンスにおいて、ループ不変条件とは、プログラムループの各反復処理の前（および後）に真となる特性のことです。これは論理的なアサーションであり、コードアサーションによって検証されることもあります。ループの効果を理解するには、その不変条件を知ることが不可欠です。

形式的なプログラム検証、特にフロイド・ホーア方式では、ループ不変条件は形式述語論理によって表現され、ループの特性、ひいてはループを用いるアルゴリズム（通常は正当性）の証明に用いられる。ループ不変条件はループへの進入時および各反復後に真となるため、ループからの脱出時には、ループ不変条件とループ終了条件の両方が保証される。

プログラミング手法の観点から見ると、ループ不変条件は、この実装の詳細を超えてループのより深い目的を特徴付ける、ループのより抽象的な仕様と見なすことができます。調査論文^{[ 1 ]}では、コンピュータサイエンスの多くの分野（検索、ソート、最適化、算術など）の基本的なアルゴリズムを取り上げ、それぞれをその不変条件の観点から特徴付けています。

ループと再帰プログラムは類似性が高いため、不変条件を持つループの部分的な正当性を証明することは、帰納法を用いて再帰プログラムの正当性を証明することと非常によく似ています。実際、ループの不変条件は、与えられたループと同等の再帰プログラムに対して証明すべき帰納的仮説と一致することがよくあります。

次のCサブルーチンは 、引数配列の長さが 1 以上であれば、max()その配列内の最大値を返します。3、6、9、11、13 行目にコメントがあります。各コメントは、関数のその段階における 1 つ以上の変数の値についてアサーションを行っています。ループ本体内の強調表示されたアサーションは、ループの開始時と終了時 (6 行目と 11 行目) でまったく同じです。したがって、これらはループの不変特性を説明しています。13 行目に到達したとき、この不変条件はまだ有効であり、5 行目のループ条件が偽になったことがわかります。これらの特性を合わせると、は の最大値に等しい、つまり 14 行目から正しい値が返されることがわかります。a[]ni!=nma[0...n-1]

int max ( int n , const int a []) {int m = a [ 0 ];// m は a[0...0] の最大値に等しいint i = 1 ;while ( i != n ) {// m は a[0...i-1] の最大値に等しい( m < a [ i ])の場合m = a [ i ];// m は a[0...i] の最大値に等しい++ i ;// m は a[0...i-1] の最大値に等しい}// m は a[0...i-1] の最大値であり、i==n である。mを返す;}

防御的プログラミングパラダイムに従うと、の不正な負の値による無限ループを避けるために、i!=n5 行目のループ条件を に変更する方が良いでしょう。 このコードの変更は直感的には違いを生まないはずですが、13 行目で のみが既知となるため、その正しさに至る推論はやや複雑になります。 も成り立つことを得るには、その条件をループ不変条件に含める必要があります。6 行目では が 5 行目の (変更された) ループ条件から得られるため、 10行目で がインクリメントされた後、11 行目で が成り立つことから、 もループの不変条件であることは容易にわかります。 しかし、正式なプログラム検証のためにループ不変条件を手動で提供する必要がある場合、 のような直感的にあまりにも明白な特性はしばしば見落とされます。i<nni>=ni<=ni<=ni<ni<=nii<=n

フロイド・ホーア論理では、^{[ 2 ] [ 3 ]} whileループの部分的正しさは、次の推論規則によって規定される。

${\displaystyle {\frac {\{C\land I\}\;\mathrm {body} \;\{I\}}{\{I\}\;{\mathtt {while}}\ (C)\ \mathrm {body} \;\{\lnot C\land I\}}}$

これはつまり：

• あるプロパティIがコードによって保持される場合${\displaystyle \mathrm {body} }$より正確には、実行後に私が保持する場合${\displaystyle \mathrm {body} }$CとIの両方が事前に保持していた場合—（上段）
• ループ全体の実行後、CとIはそれぞれ偽と真であることが保証される。${\displaystyle {\mathtt {while}}\ (C)\ \mathrm {body} }$ただし、ループの前に私が真であった場合（下の行）。

言い換えれば、上記の規則は、ホア三重項を前提とする演繹的ステップである。${\displaystyle \{C\land I\}\;\mathrm {body} \;\{I\}}$この三つ組は実際には機械の状態に関する関係です。これは、ブール式が成り立つ状態から開始する場合に常に成立します。${\displaystyle C\land I}$これは真実であり、あるコードを正常に実行しています。${\displaystyle \mathrm {body} }$すると、マシンはIが真となる状態になります。この関係が証明できれば、この規則によって、プログラムが正常に実行されたと結論付けることができます。${\displaystyle {\mathtt {while}}\ (C)\ \mathrm {body} }$私が真実である状態から、${\displaystyle \lnot C\land I}$この規則は成り立つ。この規則におけるブール式Iはループ不変式と呼ばれる。

使用される表記法に多少のバリエーションがあり、ループが停止するという前提のもと、この規則は不変関係定理としても知られています。^{[ 4 ] [ 5 ]} 1970年代のある教科書では、学生プログラマーが理解しやすいように次のように提示されています。^{[ 4 ]}

という表記は、一連の文の実行前にが真であれば、実行後にが真であるP { seq } Qことを意味する。すると、不変関係定理が成り立つ。PseqQ

P & c { seq } P

暗示する

P { DO WHILE (c); seq END; } P & ¬c

while (x < 10) x := x+1;

ループ不変条件は、以下のいずれかの目的を果たすことができます。

1. 純粋なドキュメンタリー
2. コード内でチェックされる（例：アサーション呼び出しによる）
3. フロイド・ホア法に基づいて検証される

1.については、（上記の// m equals the maximum value in a[0...i-1]例のような）自然言語によるコメントで十分です。

2.の場合、 Cライブラリのassert.hや、 Eiffelの上記に示した句など、プログラミング言語のサポートが必要です。多くの場合、実行時チェックはコンパイラまたは実行時オプションによって、デバッグ実行時には有効に、本番実行時には無効にinvariant切り替えることができます。

3.については、与えられたループコードが実際に与えられた（一連の）ループ不変条件を満たすことを、通常上記のフロイド・ホーア規則に基づいて数学的証明をサポートするツールがいくつか存在する。

抽象解釈の手法は、与えられたコードのループ不変条件を自動的に検出するために使用できます。ただし、このアプローチは非常に単純な不変条件（など0<=i && i<=n && i%2==0）に限定されます。

ループ不変コードとは、プログラムの意味に影響を与えることなくループ本体の外に移動できる文または式のことです。このような変換はループ不変コード移動と呼ばれ、一部のコンパイラはプログラムを最適化するために実行します。ループ不変コードの例（C言語の場合）は次のとおりです。

for ( int i = 0 ; i < n ; ++ i ) { x = y + z ; a [ i ] = 6 * i + x * x ; }

計算処理x = y+zをx*xループの前に移動することで、同等でありながらより高速なプログラムを作成できます。

x = y + z ; t1 = x * x ; for ( int i = 0 ; i < n ; ++ i ) { a [ i ] = 6 * i + t1 ; }

それとは対照的に、例えば、そのプロパティは0<=i && i<=n元のプログラムと最適化されたプログラムの両方でループ不変ですが、コードの一部ではないため、「ループの外に移動させる」と言うのは意味がありません。

ループ不変コードは、対応するループ不変特性を誘発する可能性がある。上記の例の場合、ループ不変コードがループの前とループ内の両方で計算されるプログラムを考えるのが最も分かりやすい。

x1 = y + z ; t1 = x1 * x1 ; for ( int i = 0 ; i < n ; ++ i ) { x2 = y + z ; a [ i ] = 6 * i + t1 ; }

このコードのループ不変特性は(x1==x2 && t1==x2*x2) || i==0、ループの前に計算された値がループ内で計算された値と一致することを示している（最初の反復の前を除く）。

• 不変量（コンピュータサイエンス）
• ループ変異体
• Whileループの最も弱い前提条件

• Thomas H. Cormen、Charles E. Leiserson、Ronald L. Rivest、Clifford Stein。『アルゴリズム入門』第2版。MIT PressおよびMcGraw-Hill、2001年。ISBN 0-262-03293-717～19ページ、セクション2.1：挿入ソート。
• David Gries。「ループ不変条件とループを開発するための標準的な戦略に関する注記」。コンピュータプログラミングの科学、第2巻、 207～214ページ、1984年。
• Michael D. Ernst、Jake Cockrell、William G. Griswold、David Notkin。「プログラム進化をサポートする可能性のあるプログラム不変条件の動的発見」。国際ソフトウェア工学会議、pp.  213–224。1999年。
• ロバート・ペイジ。「不変条件を用いたプログラミング」。IEEE Software、3(1):56–69。1986年1月。
• Yanhong A. Liu、Scott D. Stoller、Tim Teitelbaum。「効率的な計算のための不変条件の強化」。Science of Computer Programming、41(2):139–172。2001年10月。
• マイケル・ハース、マーク・ライアン著。「コンピュータサイエンスにおける論理学」、第2版。