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