An Applicative Domain Model of Container Logistics. We refer to Appendix A, Sect. A.2, Container Logistics. We summarise a narrative of Container Logistics: There is given five sets of phenomena: A set of uniquely named container terminals, a set of uniquely named container ships, a set of uniquely identified containers, a set of uniquely named shipping routes, and a set of uniquely named trucks. A container terminal consists of a quay where zero, one or more container ships may be docked, and of a container pool (a storage area) where zero, one or more containers may be temporarily stored. Container ships and container terminal pools consist of one or more uniquely named bays, each bay consists of one or more uniquely named rows, and a row consists of one or more uniquely named (container) stacks. A container stack consists of zero, one or more containers. A container consists of a container box, with or without freight, and, if with freight, then the container box also carries a waybill. A waybill consists of the unique container identifier, its own unique waybill identifier, and a list of sailings. Each sailing is a triple: The name of a container ship and the pair of names of container terminals served by the named ship and from, respectively to which the container identified by the waybill is to be transported. The list of sailings must be well-formed: If two or more sailings, then the "to" terminal named in a "non-last" entry of the list must be the same as the "from" terminal named in the next entry of that list. A shipping route is a pair: The name of a container ship and a route. The route is a list of two or more trips. A trip is just the name of a container terminal. A route is subject to well-formedness: If ti are names of container terminals, then (tl,t2,...,tn—l,tn,tn—l,...,t2,tl) is a well-formed route of n container terminal visits, on an outward journey, and n—1 container terminal visits, on a return journey. Trucks carry at most one container: either from an outside to a container terminal pool area, or to a container ship, or from a container ship or a container terminal pool area to an outside.
1. Define a concrete type system for the above container logistics system components.
2. Indicate appropriate well-formedness predicates.