0

これは、配列内の線形検索の擬似コードであり、配列内iの目的の要素が見つかった場合はインデックスを返し、そうでない場合はインデックスを返します (これは CLRS ブック、第 3 版、演習 2.1-3 からのものです)。eANIL

LINEAR_SEARCH (A, e)
    for i = 1 to A.length
        if A[i] == e
            return i
    return NIL

私はそこからループ不変式を推定しようとしているので、私の理解によれば、ループ内の任意の時点で、サブ配列A[1..i-1]には等値テストが偽であることが証明された値のみが含まれているという事実によって表されると思います。

具体的には、サブ配列の長さが null であることを意味する最初の反復の前に、そのような要素がそれに属するi-1 == 0ことはできません。次の反復の前に、等価テストも終了条件でもあるため、想定される不変プロパティは依然として true を保持する必要があります。そうでない場合、ループは既に終了しています。終了時に、関数がインデックスを返そうとしている (その場合、ループ不変条件は自明に true である) か、NIL が返されている (その場合、ループ不変条件は any に対して true を保持する) のいずれかです。vv == ei == A.length + 11 < j < i

上記は正しいですか？そうでない場合に備えて、正しいループ不変式を提供していただけますか?

ご清聴ありがとうございました。

4

1 に答える 1

1

  • ループ不変: for ループの各反復の開始時に、A[j] != efor allがありj < iます。

  • 初期化: 配列が空であるため、最初のループ反復の前に不変式が保持されます。

  • メンテナンス: ループの不変条件は各反復で維持されiます。ただし、その場合、ループの繰り返しでは値が返され、ループの繰り返しはなく、矛盾します。j < iA[j] == ejji

  • 終了ループが終了すると、2 つのケースが考えられます。1 つはi <= A.length反復後に終了する場合と、 を返すi場合ifですA[i] == e。もう 1 つのケースは、 をi超える場合ですA.length。この場合、ループ不変条件により、すべてj <= A.lengthの ,A[j] != eに対して、この返される NIL は正しいです。

于 2016-03-03T18:35:59.620 に答える