AMN und mathematische Logik Notation

Question

Ich bin mir nicht sicher, dass dies für Stackoverflow geeignet ist, aber ich weiß nicht, wo sonst zu fragen. Ich bin die B-Methode Studium in Anforderungsspezifikationen beweist Konsistenz, und ich habe ein Problem mit der Notation Logik Mathematik, wenn die vorge Bedingungen der Operationen angeben.

das ursprüngliche Problem Vereinfachen, habe ich eine Variable, die eine Teilmenge ist Flüge des kartesischen Produkts zwischen FLIGHT_NO x ZEIT x Zeit, in der für jedes Mitglied (nein, td, ta), nicht bedeutet, dass die Nummer des Fluges, td die Zeit der Abfahrt und ta TME nach der Ankunft. Wie kann ich, mathematische Logik-Notation, das Element von Flüge , die den größten Wert td hat?

Answer 1

Möchten Sie get ein solches Element, oder auf Test , dass ein Element, das Sie erfüllt diese Eigenschaft haben? Ich frage, weil die zweite eine vernünftige Voraussetzung für eine Operation scheint. Ich weiß nicht, die B-Methode speziell; Ich habe schon in einigen Dokumenten gesucht, aber nicht eine schnelle Referenz finden, so kann dies in einigen Details falsch sein.

Die zweite sollte wie folgt aussehen (prj2 ist für die zweite Projektion verwendet wird):

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

Dann wird der erste ist:

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

Answer 2

Verzeihen Sie meine Unwissenheit, ich bin nicht vertraut mit der B-Methode. Aber könnte man nicht die Einzigartigkeit quantifier benutzen? Es wäre in etwa so aussehen:

gibt es eine Zeit td, so dass für alle Zeiten td 'td> td'

und

für alle td, td ', td '', wenn td> td '' und td> td '' dann td == td'

Das ist natürlich, geht davon aus, dass es genau ein Element in dem Satz ist. Ich kann wirklich nicht sagen, ob die B-Methode für die volle Leistung ersten Ordnung Logik erlaubt, aber ich nehme an, Sie schließen dazu kommen könnten.

Answer 3

Es ist möglich, Funktionen in B. Funktionen konstante Werte zu definieren und sind in der ABSTRACT_CONSTANTS Klausel aufgeführt werden, und in der PROPERTIES-Klausel definiert. Ich versuche zu erklären, wie man dieses Konstrukt verwenden kann, um Ihr Problem zu lösen.

Es folgt einen kleinen Auszug wobei

1. eine Abkürzung für das kartesische Produkt Fluginformationen zu geben eingeleitet wird;

DEFINITIONS
    FLIGHT_INFO == FLIGHT_NO * TIME * TIME

2. vier Konstanten deklariert sind, die ersten drei sind „Accessoren“, und der letzte bildet eine nicht-leere Menge von Fluginformationen zu den Fluginformationen mit der größten Abflugzeit.

CONSTANTS
    flight_no, flight_departure, flight_arrival, last_flight

3. Dann werden diese Konstanten eingegeben und als Gesamt-Funktionen definiert. Beachten Sie, dass die letzte Funktion als Eingabe eine nicht-leere Menge nehmen müssen. Hier habe ich noch auf verschiedene Ansätze, diese Funktionen zu spezifizieren. Eine davon ist definitorischen (mit Gleichheit), und der andere ist axiomatischen.

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)))