問題タブ [loop-invariant]

正式な側面を使用してコードを作成する場合、ループ不変条件を決定する一般的な方法はありますか、それとも問題によって完全に異なりますか？

CLRS の「アルゴリズム入門」を読んでいます。第 2 章で、著者は「ループ不変条件」について言及しています。ループ不変条件とは

ループ不変条件とは何ですか? また、それらを使用してヒープ ソート アルゴリズムの正しさを証明するにはどうすればよいですか?

私はホーア論理を見ていますが、ループ不変条件を見つける方法を理解するのに問題があります。

誰かがループ不変条件を計算するために使用される方法を説明できますか？

そして、ループ不変条件が「有用な」ものであるために何を含むべきでしょうか？

私は単純な例だけを扱っており、不変条件を見つけて、次のような例で部分的および完全な修正を証明しています。

Introduction to Algorithms ( http://mitpress.mit.edu/algorithms ) に見られるように、演習では次のように述べられています。

入力:配列A[1..n]と値v

出力: Index i、 whereA[i] = vまたはNILifvが見つからないA

シーケンスをスキャンして v を探す LINEAR-SEARCH の疑似コードを記述します。ループ不変式を使用して、アルゴリズムが正しいことを証明します。(ループ不変条件が 3 つの必要なプロパティ (初期化、保守、終了) を満たしていることを確認してください。)

アルゴリズムの作成に問題はありませんが、得られないのは、ループの不変条件をどのように決定できるかということです。ループ不変の概念、つまり、ループの開始前、各反復の終了/開始時に常に真であり、ループが終了しても真である条件を理解したと思います。通常はこれが目標です。たとえば、sort の挿入、 の繰り返し、jから始まる要素は常にソートされます。これは私には理にかなっています。しかし、線形検索の場合は？ループ不変条件を考えるには単純すぎるように思えます。私は何か間違ったことを理解しましたか？次のような明白なものしか考えられません（NILまたは0とnの間のいずれかです）。よろしくお願いします！j = 2A[1..j-1]

上記のコードは、whileループを使用して、指定された正の整数の下位対数を計算して返すためのJavaのメソッドであることが意図されています。上記のループに不変条件をどのように提供しますか？つまり、開始前、ループ本体が終了するたび、およびループ条件の否定が保持されます。

このサンプルコードのループ不変条件とは何ですか。
これは、Cプログラミング言語で実装された抜粋コードです。

これらは私の最初の答えです（ループ不変条件）：

1. y>=n
2. x<=m
3. z>=0

私はまだこれについて確信が持てません。ありがとう。

だから私はこの割り当てを持っています:

質問 2 についてサポートが必要です。

階乗が逆に計算されていることに気付いたとき、私はそれを行う方法を知っていると思っていました。アルゴリズムは直感的には正しいのですが、ループが始まる前に成り立つループ不変条件を見つけることができないようです。

よくわかりません。ありがとう。

次の関数のループ不変条件を正しく識別するのに苦労しています。

x = 1 OR x = y!そのステートメントが前提条件として真であり、事後条件として真であるため、ループ不変条件を特定しました。

たとえば、y = 3の場合、ループの最初の反復でx = 1 * 3になり、3ではなく3になります。たとえば、すべての反復に当てはまるとは限りません。これは6に相当します。

これは私の混乱が本当に私が推測するところです。いくつかの本の記事は、ループ不変条件は、ループの最初またはループ（したがって前提条件）で真に等しくなければならず、ループの終わり（したがって事後条件）でも真でなければならないステートメントであると述べていますが、必ずしもそうする必要はありませんループの途中で真を保持します。

上記の関数の正しいループ不変条件は何ですか？

トリプルパワーの合計の不変量が何であるかは100％わかりません。

注：nは常に非負の値です。

擬似コード：

私はその厄介なことを知っており、はるかに簡単な方法で行うことができますが、これは私が期待していることです（主にアルゴリズム分析の練習のために）。

私は3つのループ不変条件を考え出すことになっています。LI1、LI2、およびLI3。
LI1の場合、不変量はtot =（i ^ 2（i + 1）^ 2）/ 4（0からiまでの立方体の合計の方程式）
と関係があると思います。ただし、LI2またはLI3に対して行います。LI2でのループはi^3を作成し、LI3はi ^ 2を作成しますが、それらをループ不変条件として定義する方法が完全にはわかりません。

最初のループのi++の直前にメインの合計に追加されたwhileループ本体のそれぞれに3つの別々の合計変数がある場合、不変条件を定義するのは簡単でしょうか？

あなたが与えることができるどんな助けにも感謝します。