このループは不変ですか？

Question

線形探索ループのための擬似コード：

for j = 1 to A.length 
    if(A[j] = v) 
     return j; 
return NIL 

ループ私が書いた不変：

forループの各反復の開始時に、Jは後に次のインデックスでありますA [j-1]はvと等しくない。

初期化：

Jがに等しく、それは A.length よりも小さいかどうかをチェックする前に、以前のインデックスがあります。この場合、A [0]は存在しないため、A [0]はvと等しくありません。

メンテナンス：

A [j]ははその後、ループが終了しVに等しい場合。つまり、次の反復はありません。しかし、それがvに等しくなければ、ループの次の反復が実行され、ループ不変式が保持されます。

終端：

終了するforループ引き起こす条件は、Jが大きいよりA.length又はVがA [j]がに等しくなるということです。 Jが大きくよりA.lengthになるまで、各ループの繰り返しが増加J ことであるので、我々はVに対するのすべての要素をチェックしています。したがって、アルゴリズムは正しい。 vがA [j]と等しい場合は、検索した要素が見つかりました。従ってアルゴリズムは正しい。

これらは正しいですか？

Answer 1

それほど悪くはありませんが、改善を加えることができます。

ループインバリアント（Loop Invariant）： "next after where ..."言語は不器用で、アルゴリズムが正しいという証拠には使用しないので、それを維持する理由はありません。このような何かが良いでしょう： "各反復の開始時に、A [i] == v"となるi <が存在しません。

メンテナンス：A [j]！= vの場合ループが続きます。A [i] == v、A [j]！のようなi < jが存在しないため！= vならば、A [i] == vとなるi < = jも存在せず、jの次の大きな値に対してループ不変量が成り立つ。

次に、終了条件で使用できます。配列内でvが見つかると、ループは早期に終了し、そのインデックスを返します。さもなければ、ループ不変量はj == length + 1に対して成り立ち、A [i] == vとなるようなi < =長さが存在しないこと、すなわちvが配列内に存在しないことが知られている。