問題タブ [b-method]

これがstackoverflowに適しているかどうかはわかりませんが、他にどこに尋ねるべきかわかりません。要求仕様の一貫性を証明するための B メソッドを研究していますが、操作の事前条件を指定する際の論理演算表記に問題があります。

元の問題を単純化すると、FLIGHT_NO x TIME x TIME の間のデカルト積のサブセットフライトである変数があります。ここで、各メンバー (no、td、ta) について、no はフライトの番号、td は出発時刻を意味します。そして到着時刻。数学論理表記法を使用して、td の最大値を持つフライトの要素を取得するにはどうすればよい ですか?

フランスで発明されたB-Methodについて聞いたことがあります。これは、C ++やJavaなどの従来のプログラミング言語に代わるものですか、それとも目的が異なるまったく異なるものですか？

これがstackoverflowに適しているかどうかはわかりませんが、他にどこに質問すればよいかわかりません。b言語で書かれたプログラム（B言語ではなく、CおよびC ++の前身）の場合、それがうまく書かれているかどうかを知りたいのですが、実行できるコンパイルまたはテストはありますか？

システムの仕様を B メソッドで書いています。一般的なセットのサブセットである次の変数があります。

1. 最初の記法: a :={x,y,z,v} b :={x,y,z}

セット "b" に何かが存在する場合は常に、セット "a" にも存在するという規則を述べたいと思います。これは、上記の仕様を次のように記述するのに役立ちます。

2. 2番目の表記: a :={v} b :={x,y,z}

2 番目の表記の説明: a :={v}、b :={x,y,z}、および規則から a :={x,y,z,v} をマシンに推論させたい。

最初の表記を避け、代わりに 2 番目の表記を書くようにルールを表現するにはどうすればよいでしょうか?

次のことを試しましたが、うまくいきませんでした