正式な側面を使用してコードを作成する場合、ループ不変条件を決定する一般的な方法はありますか、それとも問題によって完全に異なりますか？
質問する
28780 次
5 に答える
21
1つの同じループが複数の不変条件を持つ可能性があり、計算可能性があなたに反することはすでに指摘されています。試せないという意味ではありません。
実際、あなたは帰納的不変量を探しています。不変量という言葉は、各反復で真であるプロパティにも使用できますが、1回の反復で保持されることを知るだけでは、次。Iが帰納的不変量である場合、 Iの結果は不変量ですが、帰納的不変量ではない可能性があります。
おそらく、いくつかの定義された状況（事前条件）でループの特定のプロパティ（事後条件）を証明するために帰納的不変量を取得しようとしています。
非常にうまく機能する2つのヒューリスティックがあります。
あなたが持っているもの（前提条件）から始めて、帰納的不変量が得られるまで弱めます。弱める方法を直感的に理解するには、1つまたは複数の順方向ループの反復を適用し、現在の数式で何が真でなくなるかを確認します。
必要なもの（事後条件）から始めて、帰納的不変量が得られるまで強化します。強化する方法を直感的に理解するには、1つまたは複数のループ反復を逆方向に適用し、事後条件を推測できるように何を追加する必要があるかを確認します。
コンピューターを使って練習したい場合は、 Frama-CのCプログラム用のJessie演繹的検証プラグインをお勧めします。他にも、特にJavaおよびJMLアノテーションの場合がありますが、私はそれらにあまり詳しくありません。あなたが考える不変条件を試すことは、それらが紙の上で働く場合に試すよりもはるかに速いです。プロパティが帰納的不変であるかどうかを検証することも決定不可能ですが、最新の自動証明者は多くの単純な例で優れています。そのルートに行くことにした場合は、リストからできるだけ多くを取得してください：Alt-ergo、Simplify、Z3。
オプションの（そしてインストールが少し難しい）ライブラリApronを使用すると、Jessieはいくつかの単純な不変条件を自動的に推測することもできます。
于 2010-08-05T11:25:59.910 に答える
9
ループ不変条件を生成することは実際には簡単です。trueたとえば、良いものです。それはあなたが望む3つの特性すべてを満たします：
- ループエントリの前に保持されます
- 各反復後に保持されます
- ループ終了後も保持します
しかし、あなたが求めているのは、おそらく最強のループ不変条件です。ただし、最強のループ不変条件を見つけることは、決定不可能な作業でさえある場合があります。記事「計算可能なループ不変条件の不十分さ」を参照してください。
于 2010-06-10T05:33:19.863 に答える
2
これを自動化するのは簡単ではないと思います。ウィキから：
ループと再帰プログラムの基本的な類似性のため、不変条件を使用してループの部分的な正当性を証明することは、誘導を介して再帰プログラムの正当性を証明することと非常に似ています。実際、ループ不変条件は、多くの場合、与えられたループと同等の再帰プログラムを証明しなければならない帰納的特性です。
于 2010-05-29T14:47:20.977 に答える
1
ブログでループ不変条件の記述について書いています。ループの検証パート2を参照してください。ループが正しいことを証明するために必要な不変条件は、通常、次の2つの部分で構成されます。
- ループが終了するときに意図される状態の一般化。
- ループ本体が整形式であることを保証するために必要な追加のビット（たとえば、境界内の配列インデックス）。
（2）は簡単です。（1）を導出するには、終了後の目的の状態を表す述語から始めます。ある範囲のデータに「forall」または「exists」が含まれている可能性があります。ここで、「forall」または「exists」の境界を変更して、（a）ループによって変更された変数（ループカウンターなど）に依存するようにし、（b）ループが最初に入力されたときに不変条件が自明に真になるようにします（通常、「forall」または「exists」の範囲を空にします）。
于 2011-02-10T01:20:39.003 に答える
0
ループ不変条件を見つけるためのヒューリスティックがいくつかあります。これに関する良い本の1つは、EdCohenによる「1990年代のプログラミング」です。事後条件を手動で操作して、適切な不変条件を見つける方法についてです。例：定数を変数に置き換える、不変条件を強化する、..。
于 2010-08-06T21:39:19.073 に答える