307

CLRS の「アルゴリズム入門」を読んでいます。第 2 章で、著者は「ループ不変条件」について言及しています。ループ不変条件とは

4

16 に答える 16

390

簡単に言えば、ループ不変条件とは、ループのすべての反復で保持される述語 (条件) です。たとえば、次のforような単純なループを見てみましょう。

int j = 9;
for(int i=0; i<10; i++)  
  j--;

この例では、(反復ごとに) が true ですi + j == 9。また真であるより弱い不変式は、それ i >= 0 && i <= 10です。

于 2010-07-11T02:10:59.517 に答える
136

私はこの非常に単純な定義が好きです: ( source )

ループ不変条件は、ループの各反復の直前と直後に必ず真になる [プログラム変数間の] 条件です。(これは、反復の途中でその真偽について何も述べていないことに注意してください。)

それ自体では、ループ不変式はあまり機能しません。ただし、適切な不変量が与えられれば、それを使用してアルゴリズムの正しさを証明することができます。CLRS の単純な例は、おそらくソートに関係しています。たとえば、ループの不変条件を次のようにします。ループの開始時に、iこの配列の最初のエントリがソートされます。これが実際にループ不変条件であること (つまり、すべてのループ反復の前後で保持されること) を証明できる場合、これを使用してソート アルゴリズムの正しさを証明できます。ループの終了時に、ループ不変条件は依然として満たされます。 、カウンターiは配列の長さです。したがって、最初のiエントリがソートされているということは、配列全体がソートされていることを意味します。

さらに単純な例:ループの不変条件、正しさ、およびプログラムの派生。

私がループ不変式を理解する方法は、プログラムについて推論するための体系的で正式なツールです。真であることの証明に焦点を当てた単一のステートメントを作成し、それをループ不変条件と呼びます。これにより、ロジックが整理されます。一部のアルゴリズムの正しさについて非公式に議論することもできますが、ループ不変条件を使用すると、非常に慎重に考える必要があり、推論が完全になります。

于 2010-07-11T02:17:07.993 に答える
44

ループや不変条件を扱うときに、多くの人がすぐに気付かないことが1つあります。それらは、ループ不変条件とループ条件付き（ループの終了を制御する条件）の間で混乱します。

人々が指摘するように、ループ不変条件は真でなければなりません

  1. ループが始まる前
  2. ループの各反復の前
  3. ループが終了した後

（ループの本体では一時的にfalseになる可能性がありますが）。 一方、ループが終了した後は、ループ条件がfalseである 必要があります。そうでない場合、ループは終了しません。

したがって、ループ不変条件とループ条件付きは異なる条件である必要があります。

複雑なループ不変条件の良い例は、二分探索です。

bsearch(type A[], type a) {
start = 1, end = length(A)

    while ( start <= end ) {
        mid = floor(start + end / 2)

        if ( A[mid] == a ) return mid
        if ( A[mid] > a ) end = mid - 1
        if ( A[mid] < a ) start = mid + 1

    }
    return -1

}

したがって、ループ条件は非常に単純に見えます。start> endの場合、ループは終了します。しかし、なぜループが正しいのですか？それが正しいことを証明するループ不変条件とは何ですか？

不変条件は論理ステートメントです。

if ( A[mid] == a ) then ( start <= mid <= end )

このステートメントは論理的なトートロジーです。これは、証明しようとしている特定のループ/アルゴリズムのコンテキストでは常に当てはまります。また、ループが終了した後のループの正確性に関する有用な情報を提供します。

配列内に要素が見つかったために戻る場合、ステートメントは明らかに真です。これA[mid] == aはa、配列内にmidあり、開始と終了の間にある必要があるためです。そして、ループが終了した場合、そのstart > endような数はあり得ないstart <= mid ため 、ステートメントは偽でなければならないことがmid <= endわかります。A[mid] == aただし、結果として、全体的な論理ステートメントはnullの意味で依然として真です。（論理的には、ステートメントif（false）then（something）は常にtrueです。）

さて、ループが終了するときに条件付きで必ずfalseになるループについて私が言ったことはどうですか？要素が配列で見つかった場合、ループが終了するとループ条件が真になるように見えます！？暗黙のループ条件は実際にはそうであるため、実際にはそうではありませんwhile ( A[mid] != a && start <= end )が、最初の部分が暗黙であるため、実際のテストを短縮します。この条件は、ループがどのように終了するかに関係なく、ループの後で明らかに誤りです。

于 2013-03-12T08:48:56.183 に答える
38

以前の回答は、非常に良い方法でループ不変条件を定義しました。

以下は、CLRS の作成者が挿入ソートの正確性を証明するためにループ不変条件を使用した方法です。

挿入ソート アルゴリズム(Book に記載):

INSERTION-SORT(A)
    for j ← 2 to length[A]
        do key ← A[j]
        // Insert A[j] into the sorted sequence A[1..j-1].
        i ← j - 1
        while i > 0 and A[i] > key
            do A[i + 1] ← A[i]
            i ← i - 1
        A[i + 1] ← key

この場合、ループ不変: サブ配列 [1 から j-1] は常に並べ替えられます。

これをチェックして、アルゴリズムが正しいことを証明しましょう。

初期化: 最初の反復の前に j=2。したがって、サブアレイ [1:1] はテスト対象のアレイです。要素が 1 つしかないため、ソートされます。したがって、不変条件が満たされます。

メンテナンス: これは、反復ごとに不変条件をチェックすることで簡単に確認できます。この場合は満足です。

終了:これは、アルゴリズムの正しさを証明するステップです。

ループが終了すると、j=n+1 の値になります。ここでもループ不変条件が満たされます。これは、サブ配列 [1 から n] を並べ替える必要があることを意味します。

これが私たちのアルゴリズムでやりたいことです。したがって、私たちのアルゴリズムは正しいです。

于 2015-01-05T07:12:22.400 に答える
19

すべての良い答えに加えて、 ジェフ・エドモンズによるアルゴリズムについての考え方からの素晴らしい例は、概念を非常によく説明できると思います。

例 1.2.1 「Find-Max 2 本指アルゴリズム」

1) 仕様: 入力インスタンスは、要素のリスト L(1..n) で構成されます。出力は、L(i) が最大値を持つようなインデックス i で構成されます。この同じ値を持つエントリが複数ある場合は、それらのいずれかが返されます。

2) 基本的な手順: 2 本指の方法を決定します。あなたの右手の指がリストを下っていきます。

3) 進捗の尺度: 進捗の尺度は、右の指がリストに沿ってどれだけ離れているかです。

4) ループ不変条件: ループ不変条件は、左の指が、これまでに右の指が遭遇した最大のエントリの 1 つを指していることを示しています。

5) 主な手順: 繰り返しのたびに、右の指をリスト内の 1 エントリ下に移動します。右の指が左の指のエントリよりも大きいエントリを指している場合は、左の指を右の指と同じ位置に移動します。

6) 進歩する: 右の指が 1 つのエントリを移動するため、進歩します。

7) ループ不変条件の維持: ループ不変条件が次のように維持されていることがわかります。各ステップで、新しい左指要素は Max(古い左指要素、新しい要素) です。ループ不変条件により、これは Max(Max(shorter list), new element) です。数学的には、これは Max(長いリスト) です。

8) ループ不変条件の確立: 最初に、両方の指を最初の要素に向けることによって、ループ不変条件を確立します。

9) 終了条件: 右手の指がリストの走査を終了すると終了です。

10) エンディング: 最終的に、問題は次のように解決されることがわかっています。終了条件により、右手の指はすべてのエントリに遭遇しました。ループ不変式により、左指はこれらの最大値を指します。このエントリを返します。

11) 終了と実行時間: 必要な時間は、リストの長さの定数倍です。

12) 特殊なケース: 同じ値を持つエントリが複数ある場合、または n = 0 または n = 1 の場合に何が起こるかを確認します。

13) コーディングと実装の詳細: ...

14) 形式的証明: アルゴリズムの正しさは、上記の手順に従います。

于 2012-12-02T17:38:58.580 に答える
6

ループ不変条件は、各反復の開始時およびループの終了時に真でなければならない変数間の重要な関係を表すアサーションと見なされる場合、反復アルゴリズムの設計に役立つことに注意してください。これが成り立つ場合、計算は有効性に向かっています。false の場合、アルゴリズムは失敗しています。

于 2011-09-28T02:09:32.553 に答える
6

この場合の不変とは、すべてのループ反復の特定の時点で真でなければならない条件を意味します。

コントラクト プログラミングでは、不変条件は、パブリック メソッドが呼び出される前後に (コントラクトによって) true でなければならない条件です。

于 2010-07-11T02:10:26.587 に答える
4

不変の意味は決して変わらない

ここで、ループ不変とは、「ループ内の変数に発生する変更（インクリメントまたはデクリメント）がループ条件を変更していない、つまり条件が満たされている」ことを意味するため、ループ不変の概念が生まれました

于 2014-09-19T07:02:34.807 に答える
1

コメント権限がなくてすみません。

あなたが言及した@Tomas Petricek

また真であるより弱い不変条件は、i >= 0 && i < 10 です (これは継続条件であるためです!)"

どのようにループ不変なのか?

私が理解している限り、私が間違っていないことを願っています[1]、ループ不変条件はループの開始時に真になり (初期化)、各反復の前後に真になり (メンテナンス)、その後も真になります。ループの終了 (Termination) . しかし、最後の反復の後、i は 10 になります。したがって、条件 i >= 0 && i < 10 は false になり、ループを終了します。ループ不変条件の 3 番目のプロパティ (終了) に違反しています。

[1] http://www.win.tue.nl/~kbuchin/teaching/JBP030/notebooks/loop-invariants.html

于 2016-11-05T05:10:33.173 に答える
1

ループで何が起こっているかを追跡するのは困難です。目的の動作を達成せずに終了しない、または終了しないループは、コンピューター プログラミングでは一般的な問題です。ループ不変条件が役立ちます。ループ不変条件は、ループが実行される直前に true を保持し (不変条件を確立する)、ループの最後で再び true になる、プログラム内の変数間の関係に関する正式なステートメントです (不変条件を維持します)。 ）。コードでループ不変条件を使用する一般的なパターンは次のとおりです。

... // ここでループ不変条件が真でなければなりません
while ( TEST CONDITION ) {
// ループの先頭
...
// ループの最後
// ここでループ不変条件が真でなければなりません
}
// 終了 + ループ不変条件 =ゴール
...
ループの上部と下部の間で、ループのゴールに到達するための前進が行われていると考えられます。これは、不変式を乱す (偽にする) 可能性があります。ループ不変条件のポイントは、毎回ループ本体を繰り返す前に不変条件が復元されるという約束です。これには 2 つの利点があります。

作業は、複雑でデータに依存する方法で次のパスに持ち越されません。各パスは他のすべてのパスとは独立してループを通過し、不変式はパスをまとめて機能する全体にバインドする役割を果たします。ループが機能するという推論は、ループを通過するたびにループ不変式が復元されるという推論に縮小されます。これにより、ループの複雑な全体的な動作が小さな単純なステップに分割され、それぞれを個別に検討できます。ループのテスト条件は、不変条件の一部ではありません。それがループを終了させるものです。ループが終了する理由と、ループが終了したときにループが目的を達成する理由の 2 つを別々に検討します。ループを通過するたびに、終了条件を満たすことに近づくと、ループは終了します。多くの場合、これを保証するのは簡単です。一定の上限に達するまで、カウンタ変数を 1 ずつ進めます。場合によっては、解雇の背後にある理由がより難しい場合があります。

ループの不変条件は、終了条件が達成され、不変条件が真の場合に目標に到達するように作成する必要があります。

不変条件 + 終了 => 目標
終了以外のすべての目標達成を捉える、単純で関係のある不変条件を作成するには、練習が必要です。ループの不変条件を表すには数学記号を使用するのが最善ですが、これが過度に複雑な状況につながる場合は、明確な散文と常識に頼ります。

于 2015-09-09T19:07:00.563 に答える
0

ループ不変式は、 などの数式(x=y+1)です。その例では、xandyはループ内の 2 つの変数を表します。xコードの実行中にこれらの変数の動作が変化することを考慮すると、考えられるすべての toおよびy値をテストして、バグが発生するかどうかを確認することはほとんど不可能です。xは整数であるとしましょう。整数は、メモリ内に 32 ビット空間を保持できます。その数を超えると、バッファ オーバーフローが発生します。そのため、コードの実行全体を通して、そのスペースを超えないようにする必要があります。そのためには、変数間の関係を示す一般式を理解する必要があります。結局のところ、プログラムの動作を理解しようとするだけです。

于 2015-05-30T20:11:55.723 に答える
0

ループ不変条件は、ループ実行の前後で真であるアサーションです。

于 2018-10-10T13:54:15.970 に答える
-1

線形検索 (本で与えられた演習に従って) では、与えられた配列で値 V を見つける必要があります。

配列を 0 <= k < length からスキャンし、各要素を比較するだけです。V が見つかった場合、またはスキャンが配列の長さに達した場合は、ループを終了します。

上記の問題での私の理解によると-

ループ不変条件 (初期化): k - 1 回の反復で V が見つかりません。最初の反復では、これは -1 になるため、V が -1 の位置に見つからないと言えます

保守: 次の反復では、k-1 に見つからない V が true を保持します。

終了: V が k の位置で見つかった場合、または k が配列の長さに達した場合、ループを終了します。

于 2015-08-27T08:49:43.323 に答える