3

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

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

4

3 に答える 3

4

そのような要素を取得したいですか、それともあなたが持っている要素がこのプロパティを満たしているかをテストしたいですか? 2 番目の操作は合理的な前提条件と思われるため、質問しています。B-メソッドについては特に知りません。いくつかのドキュメントを見ましたが、クイック リファレンスが見つからないため、詳細が間違っている可能性があります。

2 番目は次のようになります (prj2は 2 番目の投影に使用されます)。

HasGreatestTd(flight) = flight \in flights \and \forall flight' (flight' \in flights => prj2(flight) >= prj2(flight'))

次に、最初は次のとおりです。

flightWithGreatestTd = choice({flight | HasGreatestTd(flight)})
于 2009-12-12T17:10:10.960 に答える
1

私の無知を許してください、私はBメソッドに精通していません。しかし、一意性量指定子を使用できませんでしたか? 次のようになります。

すべての時間 td', td > td' となるような時間 td が存在します。

と

すべての td、td'、td'' について、td > td'' および td' > td'' の場合、td == td'

もちろん、これはセット内に要素が 1 つだけあることを前提としています。B メソッドが 1 次ロジックの能力を最大限に発揮できるかどうかはわかりませんが、これに近づくことができると思います。

于 2009-12-12T17:13:27.950 に答える
0

B で関数を定義することができます。関数は定数値を持ち、ABSTRACT_CONSTANTS 句にリストされ、PROPERTIES 句で定義されます。この構造を使用して問題を解決する方法を説明しようとしています。

小さな抜粋に従います。

  1. フライト情報を提供するデカルト積のショートカットが導入されました。
DEFINITIONS
    FLIGHT_INFO == FLIGHT_NO * TIME * TIME
  1. 4 つの定数が宣言され、最初の 3 つは「アクセサー」であり、最後の 1 つは空でない一連のフライト情報を出発時刻が最大のフライト情報にマップします。
CONSTANTS
    flight_no, flight_departure, flight_arrival, last_flight
  1. 次に、これらの定数は型付けされ、合計関数として定義されます。最後の関数は、空でないセットを入力として受け取る必要があることに注意してください。ここでは、これらの関数を指定するためにさまざまなアプローチを使用しました。1 つは (等式で) 定義的であり、もう 1 つは公理的です。
PROPERTIES
    // typing 
    flight_no: FLIGHT_INFO --> FLIGHT_NO &
    flight_departure: FLIGHT_INFO --> TIME &
    flight_arrival: FLIGHT_INFO --> TIME &
    last_flight : POW1(FLIGHT_INFO) --> FLIGHT_INFO &
    // value
    flight_no = %(no, dt, at).(no |-> dt |-> at : FLIGHT_INFO | no) &
    flight_departure = %(no, dt, at).(no |-> dt |-> at : FLIGHT_INFO | dt) &
    flight_arrival = %(no, dt, at).(no |-> dt |-> at : FLIGHT_INFO | at) &
    !fs.(fs : POW1(FLIGHT_INFO) =>
       last_flight(fs) : fs &
       !(fi).(fi : FLIGHT_INFO & fi : fs =>
          flight_departure(fi) <= flight_departure(last_flight(fs)))
于 2017-06-29T11:47:17.317 に答える