Z language project (Z Specification)

Using the attached software program (Tranzit) complete the following Z Specification. The work will only be awarded to someone who can demonstrate a knowledge of the formal Z notation language. Preference will be given to those who can supply examples demonstrating their knowledge of the Z language. ## 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 a detailed, comprehensive commentary. ## Platform Please use the attached program Tranzit for writing the Z Specification. An example specification is also attached. Please DO NOT attempt this project unless you have a knowledge of the Z notation. ## Deadline information Preference given to coders who can demonstrate their knowledge of Z before undertaking the project. The Tranzit program will be emailed to the coder.