Consider a multi-storey long term parking garage. Vehicles are assigned to single spots and a spot can only accommodate a single vehicle. The parking management keeps a log of the cars that are parked. Upon entering the garage, the system will allocate a vehicle to a spot and upon leaving the garage, the system will deallocate that vehicle from its spot, thus making that spot available.

Class ParkingManagement Define a formal specification in Object-Z for class ParkingManagement to support the following operations:

AllocateVehicleOK: Allocates a vehicle to a single parking spot. DeallocateVehicleOK: Deallocates a vehicle from a single parking spot. FindVehicleOK: Returns the parking spot of a given vehicle.

You will also need to provide appropriate success and error schemata, thus combining the definitions above to produce robust specifications for the following interface:

AllocateVehicle, DeallocateVehicle, and FindVehicle.

Subclassify ParkingManagement to introduce class ParkingManagement2 that behaves exactly like ParkingManagement, while introducing the following operations:

• GetNumberOfVehicles returns the total number of vehicles currently present in the garage.

• ReallocateVehicleOK places a parked vehicle to a different parking spot. Provide any additional schema(ta) in order to extend the interface to include a robust operation ReallocateVehicle.

• GetAllVehicles returns a collection of all vehicles currently present in the garage.

The extended interface will now include operations

GetNumberOfVehicles, ReallocateVehicle, and GetAllVehicles.