問題タブ [formal-methods]

Derek Andrews と Darrel INCE による Practical Formal Methods with VDM の Chapter 5 から質問があります。

マップの価格が車をその価格に関連付ける場合、セットBLには、British Leyland 製の車とFiat製の車が含まれます。この章とセットの章で説明されているマップ機能とセット機能を使用して、次の説明を書き留めます。

(d) 価格が 6000 ～ 7000 ポンドのフィアット車の数

ここまでは・・・と思います。

1. すべての法定通貨の価格を取得します。つまり、価格マップのサブセットを返すprice(fiat)

つまり、{プント -→ 5500、パンダ -→ 6600}

2.価格帯（法定通貨）のマップ上のカード制限の可能性...

しかし、これが合法かどうかはわかりません

これは比較的簡単なはずだと思いますが、誰かがこれに答える方法を知っているかどうか疑問に思っていました:

自然数列の最小値を返す再帰関数 seq-min : N+ -> N を定義します。

・・・のようなことを考えていました。

助けてくれてありがとう！

z3 -p最新の (不安定な) Z3 で実行すると、モジュールごとにグループ化されたパラメーターのリストが表示されます。指示は次のとおりです。

一般に、これらの命令はどのように C API に変換されますか? 現在のドキュメントでは、「グローバル」構成を扱う API 呼び出しのセット( など) と、 などの型をZ3_set_param_value中心に構築された別のオブジェクト固有の呼び出しのセットがあるようです。Z3_paramsZ3_solver_set_params

Z3_set_param_value特に、任意のモジュールの任意のパラメーターをグローバルに設定するために使用できるかどうか疑問に思っていました。他の StackOverflow の回答Z3_paramsでは、グローバル パラメータに対してもオブジェクトの使用が宣伝されていますがtimeout(またはそうでしょうか?)、この API が構文:timeoutにどのようにマップされるかは明確ではありません。module.parameter=value

Cを見ると、Cはコード内で使用できる正式なメソッド（frama-c、VCC、verifast）を適切にサポートしています。私が知る限り、C++には匹敵するものはないようです。

C++ で書かれたセーフティ クリティカルなソフトウェアを推論するために利用できる形式的な方法は何ですか?

私は本を​​読み進めています: 1990 年代のプログラミング。

演習 10.12 を解くのに苦労しています。

新しい変数 n を次のように導入します。

それは私を不変に導きます

とガード

束縛関数は

割り当てによって進捗が行われる

解決策が非常に単純であることはわかっていますが、I0 の不変性を維持しようとするといつも行き詰まります。

I0 の不変性を維持するための割り当ての計算方法を教えてください。

ありがとう。

データ/コマンド交換プロトコルを記述する正式な/伝統的な方法はありますか? たとえば、プログラミング言語の場合、構文とセマンティクスを記述する複数のアプローチがあります (例: http://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form )。

私が探しているアプローチは、（アカデミックとは対照的に）かなり実用的です。仕様に取り組んでいる間、アイデアを他の人に明確に転送/広めるために、データ交換の記述に日常的に使用するものが必要です。したがって、デファクト スタンダードとして認識されていないものの、有用なものがあれば、それも問題ありません。

UML シーケンス図と「通信プロトコルの仕様と検証のための正式な方法、Carl A. Sunshine 著、1979 年」を調べました。前者の方法には「ペイロード」の説明がありませんが (少なくとも私が理解していることから)、後者の方法は方法ではなく考慮事項を説明する教育的な論文です (ただし、私はまだこの論文を読んでいます)。

前もって感謝します

ウィキペディアがリストするループ不変条件を考えると、ループの最も弱い前提条件を生成する良い方法 ( http://en.wikipedia.org/wiki/Predicate_transformer_semanticsから):

M[x <- N] は、M 内のすべての x を N に置き換えます。

さて、私の問題は変数 y です。\forall y, は式で y をバインドするため、「y は新しい変数のタプルです」は解析されません。"[x <- y]" の y と同じように、y は \forall でバインドされていますか? 上記を解析することはできません。

編集：参照要求を避けるために言い換えました。

私の質問は、ループ不変条件と最も弱い前提条件の計算との間の直接的な関係は何かということです。実際に行われている多くのことは、ループの最も弱い前提条件を検証に適した前提条件に緩和しているようです。ウィキペディアの上記は、ループ不変条件が与えられた場合、鼻の最も弱い前提条件を実際に計算できることを示唆していますが、この条件を理解するのに苦労しています。

例 1

例 2

これらの文の <> はどういう意味ですか?

私が見つけたすべての例には、宣言が 2 つしかありませんでしたsuch as name and date OR members and telephone。ただし、私のシナリオは次のとおりです。

AppointmentDB という Z スキーマを作成したいと考えています。AppointmentDB は、目的、出席者、スケジュールなどの予定の詳細を保持します

私の見解（編集済み）：

5 つの宣言と 1 つの述語があります。

ご覧のとおり、APPOINTMENT を他のすべての属性にリンクしようとしています。スキーマは正しいか完全か、またはさらに最適化するにはどうすればよいですか? また、述語部内で定義する関係から、どの関係を考えればよいかを知るにはどうすればよいでしょうか。