soen331_a5

Problem 6. Provide a contract for operation changeDepartureBy(time: Integer) that changes the departure time. Sooner departures are not permitted, and the arrival time is expected to be automat- icaly updated. Solution. context Flight : : changeDepartureBy ( time : Integer ) pre : s e l f . depatureTime > 1 post : s e l f . arrivalTime = s e l f . arrivalTime@pre + time Problem 7. “Flights arriving at the airport are handled by an airline that is housed by the airport.” Solution. context Airport inv : s e l f . a r r i v i n g F l i g h t s − > e x i s t s ( f : Flight | f . a i r l i n e = s e l f . a i r l i n e ) Problem 8. “No multiple flights depart from an airport at the same time.” Solution. context Airport inv : s e l f . departingFlights − > f o r A l l ( f1 , f2 : Flight | f1 <> f2 implies f1 . departureTime <> t2 . departureTime ) Problem 9. “The number of passengers that have booked a flight cannot exceed the capacity of the flight.” Solution. context Flight pre : s e l f . passengers − > s i z e () < s e l f . capacity Problem 10. “All tickets on connections scheduled by a rail company are tickets issued by that company.” “All tickets issued by a rail company correspond to connections handled by the company.” Solution. context Ticket inv : s e l f . schedule . getConnection − > f o r A l l ( c : Connection | c . railcompany = s e l f . railcompany ) 2