問題タブ [loop-invariant]

配列には、最初に値が増加し、次に値が減少する整数が含まれます。どの時点で数が減少し始めるかは不明です。2 番目の配列が昇順で並べ替えられるように、最初の配列の数値を別の配列にコピーする効率的なコードを記述します。

コードは以下のとおりです。

ここでのループ不変条件は何ですか?

私はループ不変条件を学んでおり、ますます難しい質問に挑戦してきました。今日、質問を解決しましたが、私の解決策が正しいかどうかわかりません。誰かが私の答えを確認して、解決策を与えるのではなく説明してもらえますか?

コード：

ループ不変条件:c.size() == i

質問：

c.size()==i述語がループ不変条件であるかどうかを簡単に説明してください。それがループ不変条件である場合、メソッドがその仕様に関して部分的に正しいことを検証するのに十分かどうかを説明してください. 述語がループ不変条件でない場合、またはメソッド pairwiseMin の部分的な正しさを検証するには不十分な場合は、メソッドが部分的に正しいことを示すために使用できるループ不変条件を定義します。

私の解決策：

はい、ループが実行される前後に前提条件事後条件が満たされるため、ループ不変です。

最初の反復:

c.size() をチェック

したがって、部分的な正しさを証明するには十分です。

したがって、次のコードがある場合:

ここで、ループ不変条件を見つけなければなりません。このようなループの場合、Y = i^2 の不変式はループ不変式と見なされると言われましたが、それがループ不変式であることを証明する方法がわからないのです。Y は単なるものであるため、ループの前、ループ中、およびループ後は常に true です。これは、i*i が何であれ ... それが不変式であることの有効な証拠ですか?

また、不変式を使用してアルゴリズムを証明する場合、合計 = i*i (または Y、ループ不変式) の 1 から n までの合計 = n(n+1)(2n+1 )/6

それでは、帰納法を使ってそれが正しいことを示しますか? アルゴリズムを証明するためにループ不変式を適切に使用していますか?

助けていただければ幸いです:)

ループ不変式が問題の正しさを証明するためのものであることは知っていますが、問題がどんなに些細なものであっても、どのようにループ不変式を作成するのかがよくわかりません。これが例です。誰かが私が考え出すために考慮すべきステップは何かを指摘できますか. ループ内で変化するすべての値が不変条件に含まれている必要があることはわかっています。この問題について教えてください。事後条件も見つける必要があります。説明は答えよりも価値があります。助けてください。

g++ を使用して、ループ不変コードのモーション最適化の結果を確認することにしました。しかし、次のコードをコンパイルして-fmove-loop-invariantsそのアセンブリを分析しk + 17たところ、ループ本体でまだ計算が実行されていることがわかりました。

コンパイラがそれを最適化するのを妨げるものは何ですか?

コンパイラは、再計算する方が効率的であると結論付けているのk + 17でしょうか?

g++ 4.6.3 と g++ 4.8.3 の両方を使用して試しg++ -O0 -fmove-loop-invariantsてみました。g++ -O3g++ -O3 -fmove-loop-invariants

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

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

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

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

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

この有効なトリプルの有効性を証明するには:

ループ不変条件とは何ですか?

Eiffel のループは次の形式に従います。

上記の Eiffel 疑似コードを、ループの不変条件/不変条件をサポートしない言語にどのように翻訳しますか? assertそのようなターゲット言語に、不変/変種をチェックする命令があると仮定しましょう。