0 
int i, temp; 
a is an array of integers [1...100] 

i = 1; 

while i < 100 
    if a[i] > a[i+1] 
        temp = a[i]
        a[i] = a[i+1]
        a[i+1] = temp 
    i = i+1

ループの不変条件を見つけて、それらの正式なステートメントを書く方法を理解するのに苦労しています。したがって、ループ不変条件は、ループの各反復の直前と直後に真である条件にすぎません。コードがスワップを行っているようです。次の要素が配列内で現在の要素よりも大きい場合は、場所を切り替えます。つまり、ループ不変式の定義から、実際には i < 100 のように聞こえますが、それはループが実行されるためには true でなければならないためですが、私にはよくわかりません。いくつかの説明をいただければ幸いです。

4

4 に答える 4

2

あなたの定義によれば、ループの不変条件が 2 つあります。

1. i < 100
2. a[i] = greater than a[j] for all j < i, where i is the loop variable.

これは実際には、バブル ソートの 1 つの外側ループの繰り返しです。このループの最後で、配列の最大値が一番上にバブルします (a[100]) 。

于 2013-12-03T17:27:11.687 に答える
1

大まかに言えば、あなたは正しいです。ループ不変条件は、「ループの各反復の直前と直後に真である条件」です。ただし、この定義では、問題のコードのループ不変条件は文字通り無数にあり、それらのほとんどは特に重要ではありません。たとえば、i < 101、i < 102、i < 103、... はすべて、特定のコードのループ不変条件です。

ただし、通常、ループ不変条件を見つけるためだけにループ不変条件を見つけることには関心がありません。代わりに、プログラムが正しいことを証明することに関心があり、プログラムが正しいことを証明したい場合は、適切に選択されたループ不変条件が非常に役立つことがわかります。

たとえば、問題のコードはバブル ソート アルゴリズムの内側のループであり、その目的は配列を "よりソート" することです。したがって、このコードが完全に正しいことを証明するには、次の 3 つのことを証明する必要があります。

(1) 実行がコードの最後に到達すると、配列はコードの先頭の配列の順列になります。(2) 実行がコードの最後に到達すると、配列内の反転の数はゼロであるか、コードの開始時の配列内の反転の数よりも少なくなります (この条件は、外側のバブルソートアルゴリズムのループが終了します)。(3) コードが終了します。

(1) を証明するには、3 つの実行パスを考慮する必要があります (パス 2 を検討する場合、ループ不変条件が重要な役割を果たします)。

(PATH 1) 実行がコードの先頭から始まり、ループの先頭に初めて到達したときに何が起こるかを考えてみてください。この実行パスでは配列に対して何も行われないため、配列はコードの先頭にある配列の順列です。

(PATH 2) 次に、実行がループの先頭から開始され、ループを一巡して、ループの先頭に戻るとどうなるかを考えてみましょう。a[i] <= a[i+1] の場合、スワップは発生せず、したがって、配列はコードの先頭で配列の順列のままです (何も行われないため)。または、a[i] > a[i+1] の場合、スワップが発生します。ただし、コードの先頭では、配列は依然として配列の順列です (スワップは順列の一種であるため)。したがって、実行がループの先頭に到達するたびに、配列はコードの先頭にある配列の順列になります。「配列はコードの先頭にある配列の順列である」というステートメントは、コードが正しいことを証明するために必要な、適切に選択されたループ不変条件であることに注意してください。

(パス 3) 最後に、実行がループの先頭から開始され、ループに入らずにコードの最後まで実行されるとどうなるかを考えてみましょう。この実行パスでは配列に対して何も行われないため、配列はコードの先頭にある配列の順列です。

これらの 3 つのパスは、実行がコードの先頭からコードの末尾まで進む可能性のあるすべての方法をカバーしているため、(1) コードの末尾の配列は先頭の配列の順列であることが証明されました。コードの。

于 2014-09-25T16:01:20.487 に答える
-1

ループは test によって制御されますi < 100。ループの本体内ではi、いくつかの場所で使用されますが、1 つの場所にのみ割り当てられます。代入は常に発生iし、ループへのエントリを許可する任意の値に対して、代入は終了条件に向かって収束します。したがって、ループは終了することが保証されます。

プログラムの正確さに関しては、それは別の問題です。配列がゼロベースまたは 1 ベースのインデックス付けを使用しているかどうかに応じてi、配列アクセスに使用している方法が問題になる可能性があります。ゼロベースの場合、最初の要素を見ることはなくa[i+1]、最後の反復で範囲外になります。

于 2013-12-03T18:34:27.927 に答える