問題タブ [loop-invariant]

質問する

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

127 問題
Newest
Active
Bountied
318
Unanswered
0 投票する
1 に答える
210 参照

algorithm - このループは不変であり、その非公式な証明は正しいですか? (CLRS 第 3 版演習 2-1-3)

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

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

以下は、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言い換えれば、配列のサブ配列を参照するのは間違っていると感じます。サブ配列は、そもそもサブ配列がサブ配列であると想定されている配列の開始インデックスよりも小さいインデックスで終了します。これは、ループの最初の繰り返しの前に、上記のループ不変式が実際には偽であることを暗示しているようです。

考え？


12345678910