AMN and mathematical logical notation

Question

I'm not sure if this is suitable for stackoverflow, but I don't know where else to ask. I am studying the B-method to prove consistency in requirements specifications, and I have a problem with logical mathematical notation when specifying the preconditions for operations.

To simplify the original problem, I have a variable which is a subset of the flights of the Cartesian product between FLIGHT_NO x TIME x TIME, where for each member (no, td, ta) there are no number of flights, td departure time and arrival time. How can I get, using mathematical logical notation, the flight element that has the highest td value?

Answer 1

Do you want to get such an element or check that the element that you have satisfies this property? I ask because the second seems like a reasonable precondition for the operation. I do not know B-Method specifically; I looked through some documents, but I can not find a short link, so this may be wrong in some details.

The second should look like this ( prj2used for the second projection):

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

Then the first:

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

Answer 2

Forgive my ignorance, I am not familiar with the B-Method. But is it possible to use the uniqueness quantifier? It looks something like this:

there is a time td such that for all td ', td> td'

and

for all td, td ', td' ', if td> td' 'and td'> td '', then td == td '

, , , . , B- , , .

Answer 3

B. ABSTRACT_CONSTANTS PROPERTIES. , .

,

• , ;

DEFINITIONS
    FLIGHT_INFO == FLIGHT_NO * TIME * TIME

2. , - "", .

CONSTANTS
    flight_no, flight_departure, flight_arrival, last_flight

3. . , . . ( ), - .

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