AMN and math logic notation

Question

I'm not sure this is appropriate for stackoverflow, but I don't know where else to ask. I'm studying the B-Method for proving consistence in requirement specifications, and I have an issue with the logic math notation when specifying the pre conditions of the operations.

Simplifying the original problem, I have a variable which is a subset flights of the cartesian product between FLIGHT_NO x TIME x TIME, where for each member (no,td,ta), no means the number of the flight, td the time of departure and ta the tme of arrival. How can I get, using math logic notation, the element of flights that has the biggest value of td?

Answer 1

Do you want to get such an element, or to test that an element you have satisfies this property? I am asking because the second seems a sensible precondition to an operation. I don't know the B-Method specifically; I've looked at some documents, but can't find a quick reference, so this may be wrong in some details.

The second should look like this (prj2 is used for the second projection):

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

Then the first is:

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

Answer 2

Forgive my ignorance, I'm not familiar with the B-Method. But couldn't you use the uniqueness quantifier? It'd look something like:

there exists a time td such that for all times td', td > td'

and

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

This, of course, assumes that there is exactly one element in the set. I can't really tell if the B-Method allows for the full power of first order logic but I assume you could come close to this.