問題タブ [formal-methods]

システムとその完全な状態空間が与えられた場合、その状態空間はそのシステムの動作の正式な仕様であると言えますか?

ここで問題をより明確に変更しました。送信側モデルと受信側モデルの 2 つの異なるモデルがあります。送信されたメッセージが受信者が受信したものと同じではないというプロパティを確認したい。

LTLSPEC (G(状態=受信者 -> messageTransmited != messageReceived))

ProBで多数のコードを視覚化する際に問題があります。このグラフは、ProB の (Graphviz の dotty を使用して) サーバーのログイン セクションを示していますが、グラフを取得するための多数のコードに対する解決策はありません。あなたの提案やアイデアを教えてください。

合金初心者です。

私は、Alloy で制約を作成し、モデルが制約に従って有効であることをアナライザーにチェックさせるのが本当に好きです。

しかし、「これらの制約の定義は単なる頭の体操ですか? それとも、より良いソフトウェアの構築に役立つでしょうか?」</p>

具体例を挙げてみましょう。電子メール クライアントのアドレス帳のモデルでは、アドレス帳に新しいエントリを追加するために次の制約を定義できます。

新しいブック b' のアドレス マッピングは、古いブック b のアドレス マッピングと同じですが、名前からアドレスへのリンクが追加されています。この制約は Alloy では次のように表されます: b'.addr = b.addr + n->a

それは美しいです。

しかし、追加操作がコードに実装されている場合、その関連性を確認するのに苦労しています。たとえば、Common Lisp でadd操作を実装しました。

つまり、「これはaddという名前の関数の定義で、3 つのパラメーターb、n、およびa (本、名前、住所) を持ちます。Common Lisp の set 関数adjoinを使用して、リスト ( na ) をbに追加します。"</p>

その関数は、単純な追加関数を正しく実装しているようです。Alloy で定義した拘束はどうすればよいですか? 制約を表現する追加のコードを作成する必要がありますか? 擬似コード: [1]

このようなコードを書くのは大変な作業のように思えますが、明らかなメリットはありません。

私の質問は次のとおりです: コードで Alloy モデルを実装する場合、Alloy で定義されている制約をどうすればよいですか?

また、Alloy モデルをコードに変換する方法を説明するチュートリアルはありますか? コードで Alloy 制約定義がどのように使用されるかの説明が含まれていますか?

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

[1] 注: Common Lisp には Screamer という制約プログラミング用の言語拡張があることを認識しています。

次の簡単な証明があります。

証明状態で、イザベルは次のように述べています。

エクスポートされたルールによってゴールを解決しようとして成功しました: n * n < a * b

しかしその後：

初期証明方法の適用に失敗しました⌂: これを使用: n < a n < b ゴール (1 サブゴール): 1. n * n < a * b

何が問題ですか？。実際、プロフを行うための実際の単一ステップに興味があるので、isabelle がその方法を教えてくれると思いました。

時々 UPPAAL で、int x:=1-0 のような 2 つの値を取る整数変数の例を見つけましたが、これは正確にはどういう意味ですか? xが最初に「1」を取り、次に「0」をとるように、またはXは2つの値の単なる配列ですか?

ありがとうございました