Z Specification

Using the supplied software (which I shall email to the successful coder) complete the below Z Specification. Full, complete schemas should be delivered along with a comprehensive commentary. ## Deliverables Complete and fully-functional working program(s) in executable form as well as complete source code of all work done. Complete copyrights to all work purchased. Write a Z specification for the system informally described below. The ACME car hire company has a fleet of cars distributed across the country in a number of depots in several major cities. Each car is identified by a unique id number. The depot in which the car is currently garaged, the car's current mileage and the car's manufacturer is recorded for each car. A client can hire a car from any depot and return it to any other depot. When a customer hires a car from a particular depot, they provide their name and specify the make of car they want, and the hire date is recorded. A specific car (if available) is then allocated to them. When the car is returned (possibly to another depot), its new mileage is inspected, and the customer is charged 10p per mile plus a fixed charge of £20 for each day of the hire period. The ACME company is so successful that sometimes there's a queue of people waiting to return their hired car to a depot. When this happens, the company deals with the queue in strict order. Occasionally a customer in the queue gets tired of waiting and leaves, hoping to return later when the queue is shorter. Write a Z specification for the system informally described above. You should include robust specifications for the following operations: (a) Hiring a car. (This operation ignores cars which may be in the returning queues - only those cars actually in the depots are available for hire.) (b) Returning a car. (This comprises essentially three operations - joining a particular returning queue, dealing with the car at the front of a queue by issuing a bill etc., and leaving the queue early.) (c) Answering the following queries: (i) Which depots currently have a car of this particular make? (ii) Which cars are currently garaged at this particular depot? (iii) Is there a returning car of this particular make queueing at this particular depot? If so, what position is it in the queue? State clearly any assumptions you make, and remember that the English commentary component of a Z specification is an important aid to understanding, so please include it. ## Platform Dedicated schema writing software. Will be supplied upon commencement of the project.