1

次の線形検索アルゴリズムがあるとします (要素の配列の最初の要素のインデックスとしてインデックス 1 を参照します)。

found_idx = nil
for i = 1 to A.length
  if A[i] == value
    found_idx = i
    return found_idx
  end-if
end-for
found_idx

このループ不変式が正しいかどうか疑問に思っていました。

以下は、CLRS のフォーマットに従った、このループ不変式の非公式な説明です。

  1. 初期化: i = 1 であり、i-1 で終わる配列が空であるため、最初の反復の前は true であり、したがって found_idx は nil です。
  2. メンテナンスi: の各値でA[i]がチェックされて iからインクリメントされるため、これは各反復後に真になりi-1ます。
  3. Termination : これはi > A.length、 までのすべての要素A.lengthがチェックされたことを意味する場合に終了します。

私の主な懸念点は、ループが配列の最初の要素である 1i-1から始まるため、で終わるインデックスを参照するのは正しくないということです。i言い換えれば、配列のサブ配列を参照するのは間違っていると感じます。サブ配列は、そもそもサブ配列がサブ配列であると想定されている配列の開始インデックスよりも小さいインデックスで終了します。これは、ループの最初の繰り返しの前に、上記のループ不変式が実際には偽であることを暗示しているようです。

考え？

4

1 に答える 1