AMN と数学論理表記法

StackOverflow https://stackoverflow.com/questions/1893482

質問

これが stackoverflow に適切かどうかはわかりませんが、他にどこに問い合わせればよいのかわかりません。要求仕様の整合性を証明するためのBメソッドを勉強しているのですが、演算の事前条件を指定する際の論理演算の表記に問題があります。

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

役に立ちましたか？

解決

あなたはののような要素を取得したいか、またはのテストのにあなたが満足するこの特性を持っている要素の？第二は、操作に賢明な前提条件だので、私は求めています。私は、特にB-方法を知りません。私はいくつかのドキュメントを見てきましたが、クイックリファレンスを見つけることができないので、これはいくつかの詳細では間違っている可能性があります。

秒（prj2が第二投影するために使用される）は、このようになります。

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

そして、最初は、次のとおりです。

flightWithGreatestTd = choice({flight | HasGreatestTd(flight)})

他のヒント

私の無知を許して、私はB-法に精通していませんよ。しかし、あなたは一意数量詞を使用することができませんでしたか？

：それは次のようになりたいです

時間tdは、すべての回tdのような存在 'TD> TD'

と

すべてのTD、TD 'TD ''、のためであればTD> TD'およびTD'> TD '' その後、TD == TD'

これは、当然のことながら、セット内の1つの要素があることを前提としています。 B-方法は、一階述語論理のフルパワーを可能にしている場合、私は本当に言うことができないが、私はあなたがこの近くに来ることができると仮定します。

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

小さな抜粋が続きます。

  1. フライト情報を与えるデカルト積のショートカットが導入されます。
DEFINITIONS
    FLIGHT_INFO == FLIGHT_NO * TIME * TIME
  1. 4 つの定数が宣言され、最初の 3 つは「アクセサ」で、最後の定数は空ではないフライト情報のセットを最大の出発時刻を持つフライト情報にマップします。
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)))
ライセンス： CC-BY-SA と 帰属
所属していません StackOverflow
scroll top