ループ不変

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

形式プログラム検証、特にFloyd-Hoare アプローチでは、ループ不変条件は形式述語論理によって表現され、ループの特性、およびループを使用する拡張アルゴリズム(通常は正当性特性)を証明するために使用されます。ループ不変条件は、ループに入るときと各反復の後に真になるため、ループから出るときに、ループ不変条件とループ終了条件の両方が保証されます。

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

ループと再帰プログラムは類似しているため、不変式を持つループの部分的な正しさを証明することは、帰納法によって再帰プログラムの正しさを証明することと非常に似ています。実際、ループ不変式は、特定のループと同等の再帰プログラムに対して証明される帰納的仮説と同じであることがよくあります。

次のC サブルーチンは 、長さが 1 以上であれば、max()引数配列 の最大値を返します。3、6、9、11、13 行目にはコメントがあります。各コメントは、関数のその段階での 1 つ以上の変数の値についてアサーションを行います。ループ本体内のループの最初と最後 (6 行目と 11 行目) の強調表示されたアサーションはまったく同じです。したがって、これらはループの不変プロパティを記述します。13 行目に到達しても、この不変条件は保持され、5 行目のループ条件が false になったことがわかります。両方のプロパティを合わせると、は の最大値に等しいこと、つまり、14 行目から正しい値が返されることがわかります。 a[]ni!=nma[0...n-1]

int max ( int n , const int a []) {      
    整数m = a [ 0 ];   
    // mはa[0...0]の最大値に等しい
    整数i = 1 ;   
    ( i != n )の間{    
        // mはa[0...i-1]の最大値に等しい
        もし( m < a [ i ] )   
            m = a [私];  
        // mはa[0...i]の最大値に等しい
        ++私;
        // mはa[0...i-1]の最大値に等しい
    }
    // mはa[0...i-1]の最大値に等しく、i==n
    mを返します。 
}

防御的プログラミングパラダイムに従うと、の不正な負の値による無限ループを回避するために、 5 行目のループ条件i!=nを に変更する方が適切です。このコード変更は直感的には違いを生まないはずですが、その正しさを導く推論はいくぶん複雑になります。なぜなら、 のみが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が保存される場合、より正確には、CとIの両方が事前に保持されていた場合、実行後もIが保持される場合（上の行）、${\displaystyle \mathrm {body} }$${\displaystyle \mathrm {body} }$
• ループ前にIが true であった場合(下の行)、ループ全体の実行後にCとI はそれぞれ false と true になることが保証されます。${\displaystyle {\mathtt {while}}\ (C)\ \mathrm {body} }$

言い換えると、上記の規則は、ホーア トリプル を前提とする演繹ステップです。このトリプルは、実際にはマシンの状態の関係です。ブール式が true である状態から始まり、 と呼ばれるコードを正常に実行すると、マシンはIが trueである状態になります。この関係が証明できれば、この規則により、プログラムが正常に実行されると、Iが true である状態から が成立する状態に移行すると結論付けることができます。この規則のブール式Iは、ループ不変量と呼ばれます。 ${\displaystyle \{C\land I\}\;\mathrm {body} \;\{I\}}$${\displaystyle C\land I}$${\displaystyle \mathrm {body} }$${\displaystyle {\mathtt {while}}\ (C)\ \mathrm {body} }$${\displaystyle \lnot C\land I}$

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

表記は、文のシーケンスが実行される前にが真であれば、文のシーケンスが実行された後にが真であるP { seq } Qことを意味します。すると、不変関係定理は次のように成り立ちます。 PseqQ

P & c { seq } P

暗示する

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

次の例は、このルールがどのように機能するかを示しています。次のプログラムを考えてみましょう。

ただし、(x < 10)
    x := x+1;

すると、次のホーアトリプルが証明されます。

${\displaystyle \{x\leq 10\}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{x=10\}}$

ループの条件Cwhileは です。有用なループ不変量Iを推測する必要がありますが、 が適切であることがわかります。これらの仮定の下で、次の Hoare トリプルを証明することができます。 ${\displaystyle x<10}$${\displaystyle x\leq 10}$

${\displaystyle \{x<10\land x\leq 10\}\;x:=x+1\;\{x\leq 10\}}$

この 3 つは、割り当てを管理する Floyd-Hoare 論理の規則から形式的に導出できますが、直感的にも正当化されます。計算はが真である状態から開始され、これは単に が真であることを意味します。計算ではxに 1 が加算され、これは(整数 x に対して) が依然として真である ことを意味します。${\displaystyle x<10\land x\leq 10}$${\displaystyle x<10}$${\displaystyle x\leq 10}$

この前提の下で、ループのルールによりwhile次の結論が導かれます。

${\displaystyle \{x\leq 10\}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{\lnot (x<10)\land x\leq 10\}}$

ただし、事後条件( x は10 以下であるが、10 未満ではない) は論理的には と同等であり、これが私たちが示したかったことです。 ${\displaystyle \lnot (x<10)\land x\leq 10}$${\displaystyle x=10}$

プロパティは、例のループの別の不変式であり、自明なプロパティは別の不変式です。上記の推論規則を前の不変式に適用すると、 が生成されます。これを不変式に適用すると、 が生成され、少し表現力が増します。 ${\displaystyle 0\leq x}$${\displaystyle \mathrm {true} }$${\displaystyle \{0\leq x\}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{10\leq x\}}$${\displaystyle \mathrm {true} }$${\displaystyle \{\mathrm {true} \}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{10\leq x\}}$

Eiffelプログラミング言語は、ループ不変条件をネイティブにサポートしています。^{[6]ループ不変条件は、}クラス不変条件と同じ構文で表現されます。以下のサンプルでは、​​ループ不変条件式は、x <= 10ループの初期化後、およびループ本体の実行後にそれぞれ真である必要があります。これは実行時にチェックされます。

    
x := 0からx <= 10まで不変、 x > 10までループx := x + 1終了          
    
          
    
          
    
            
    

Whileyプログラミング言語は、ループ不変条件に対する第一級のサポートも提供します。^[7]whereループ不変条件は、次に示すように、 1つ以上の節を使用して表現されます。

function  max ( int []  items )  ->  ( int  r ) 
// max を計算するには少なくとも 1 つの要素が必要です
requires  | items |  >  0 
// (1) 結果がどの要素よりも小さくないこと
が保証されます all  {  i  in  0 .. | items |  |  items [ i ]  <=  r  } 
// (2) 結果が少なくとも 1 つの要素と一致すること
が保証されます some  {  i  in  0 .. | items |  |  items [ i ]  ==  r  } : 
    // 
    nat  i  =  1 
    int  m  =  items [ 0 ] 
    // 
    while  i  <  | items | 
    // (1) これまでに見つかったどのアイテムも m より大きいものではありません
    where  all  {  k  in  0 .. i  |  items [ k ]  <=  m  } 
    // (2) これまでに見つかった 1 つ以上のアイテムが m と一致します
    where  some  {  k  in  0 .. i  |  items [ k ]  ==  m  } : 
        if  items [ i ]  >  m : 
            m  =  items [ i ] 
        i  =  i  +  1 
    // 
    return  m

関数max()は整数配列の最大要素を決定します。これを定義するには、配列に少なくとも 1 つの要素が含まれている必要があります。の事後条件max()では、返される値が (1) どの要素よりも小さくないこと、および (2) 少なくとも 1 つの要素と一致することが要求されます。ループ不変式は、whereそれぞれが事後条件の節に対応する 2 つの節を通じて帰納的に定義されます。基本的な違いは、ループ不変式の各節は結果が現在の要素まで正しいことを識別するのに対しi、事後条件は結果がすべての要素に対して正しいことを識別することです。

ループ不変条件は、次のいずれかの目的に使用できます。

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

1. の場合、自然言語コメント (// m equals the maximum value in a[0...i-1]上記の例のような) で十分です。

2. については、 Cライブラリassert.hや、上記Eiffel の句などのプログラミング言語のサポートが必要ですinvariant。多くの場合、ランタイム チェックは、コンパイラまたはランタイム オプションによってオン (デバッグ実行用) とオフ (本番実行用) を切り替えることができます。^{[引用が必要]}

3. については、通常、上記の Floyd-Hoare 規則に基づいて、特定のループ コードが実際に特定のループ不変条件 (セット) を満たしていることを数学的に証明することをサポートするツールがいくつか存在します。

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

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

( 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 ; ( 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-7。17～ 19 ページ、セクション 2.1: 挿入ソート。 
• David Gries . 「ループ不変条件とループを開発するための標準戦略に関するメモ」Science of Computer Programming、第 2 巻、pp. 207–214。1984 年。
• Michael D. Ernst、Jake Cockrell、William G. Griswold、David Notkin。「プログラム進化をサポートするために、適切なプログラム不変条件を動的に発見する」国際ソフトウェア工学会議、pp. 213–224。1999 年。
• Robert Paige. 「不変条件によるプログラミング」IEEEソフトウェア、3(1):56–69。1986年1月。
• Yanhong A. Liu、Scott D. Stoller、Tim Teitelbaum。効率的な計算のための不変条件の強化。コンピュータプログラミングの科学、41(2):139–172。2001年10月。
• Michael Huth、Mark Ryan。「コンピュータサイエンスにおける論理」、第 2 版。