問題タブ [formal-verification]

2 つの LTL を比較して、一方が互いに矛盾する可能性があるかどうかを確認するにはどうすればよいですか? 階層的なステート マシンと、各ステートの動作を説明する LTL があるためです。ローカル LTL がグローバル LTL と矛盾する可能性があるかどうかを知る必要があります。「機能仕様と自動競合検出」という記事で、L(f) の交差 L(g) が空である場合、2 つの LTL プロパティ f と g が矛盾することを見ました。そして、これはまさに、プログラムとして f とプロパティとして ¬g を使用したモデル チェックの問題です。誰でもこれで私を助けることができますか？LTL f を SPIN/Promela のプログラムに変換するにはどうすればよいですか??

ありがとう。

私は現在、楽しいプロジェクトとして Z3 の上に自分のプログラミング言語用の自動検証ツールを書いています。これを使用して、ループを使用したフィボナッチ実装が再帰を使用したものと同等であることを証明しようとしています。

入力プログラムが正しい場合、つまり、Z3 に対して適切な入力を生成し、Z3 が満足できないと言う場合、これは私のコンテキストではプログラムが正しいことを意味します。しかし、変数の初期化を 1 つ変更したためにプログラムが正しく表示されなくなったとき、検証者は次の Z3 式を思いつきました。これは私にはそれほど複雑ではないように見えますが、Z3 は「不明」と言っています。

2 つの量指定子は、フィボナッチの再帰的な定義を表していることに注意してください。私の友人は、一致するループを回避するためのこのトリックを教えてくれました: fib を再帰関数として定義する代わりに、定義を提供しない別の関数 fakeFib を導入し、それを fib の再帰定義で使用します。また、検証者にそれらが等しいことを伝えますが、その量指定子は fib のパターンのみを取得し、fakeFib のパターンは取得しません。つまり、プログラムの正しさを証明するには、1 レベルの再帰を見るだけで十分です (ただし、k レベルに簡単に拡張できます)。しかし、ループの一致を避けるために、その制限に耐えることができます。

コードの「バグ」は、変数を誤って初期化したことであり、これが最終的(= 1 (fib 0))に最後のアサーションで誤ったコンポーネントにつながりました。正しいプログラムの場合、それは(= 0 (fib 0)).

いくつかの観察：

• で置き換える(= 1 (fib 0))と(= 0 (fib 0))、Z3 はそれが満足できないことをすぐに判断します。
• 以前は、オプション(set-option :smt.auto-config false)と(set-option :smt.mbqi false)設定がなく、マシンのメモリが不足し、rise4fun の時間が不足していました。
• (set-option :smt.macro-finder true)同様の質問を持つ人々にとってうまくいったと思われる設定は、私にはうまくいきませんでした。これは、1 つだけでなく2 つの量指定子があることが原因であると推測していfibます。
• 比較としてcvc4を使用してみましたが、すぐに「不明」と表示されました。したがって、私の問題は Z3 固有のものではないようです。
• 式は明らかに充足可能です。(= 1 (fib 0))であるfalseため、最後のアサーション全体が自動的に true になります。(>= n 0)も満足しやすい。

プロセス a またはプロセス b がクリティカル セクションに入りますが、同時にではありません。これが発生した場合 (つまり、それらが同時にクリティカル セクションに入った場合)、割り込みが実行されます。

p = プロセス a

q = プロセス b

r = クリティカル セクション

演算子 ∨ = または

演算子 → = 含意

私の答え ：

(p ∨ q) → r

これは正しいですか、それとも私が何か間違ったことをしましたか? 命題論理を理解しようとしています。

dafny で再帰的な sum 関数を書き、その正しさを証明しようとしました。私は書いた：

これは私が書いた証明です：

SUM1:

SUM2:

私が得るエラー：

理由を理解してください。

以下のリンクのコードの次の証明を書きました。count2 メソッドの証明について助けを求めたいと思います。代替証明は私にはあまり明確ではありません ありがとう

http://rise4fun.com/Dafny/ueBY

このプログラムを dafny で証明しようとしていますが、最後の不変条件でエラーが発生し、なぜ機能しないのかわかりません。

このプログラムは、ソートされた配列に int を挿入するメソッドで構成されています。int は正しい位置に挿入されます。つまり、5 を 1,2,3,4,5,6,7 に挿入すると、次の値が返されます: 1,2,3,4,5,5,6,7

ありがとう