- Complete the following algebraic specification for an abstract data type describing a queue of cars at an intersection by providing axioms.
algebra QueueOfCars imports Integer, Boolean; introduces sorts Queue, Car;
operations
New: → Queue;
CarArrives: Car x Queue → Queue;
CarDeparts: Queue → Queue;
IsEmpty: Queue → Boolean;
NumberOfCars: Queue → Integer;
Longer: Queue x Integer → Boolean;
FirstCar: Queue → Car;
Equal: Queue x Queue → Boolean;
WhichQueue: Queue x Queue x Car → Integer;
Position: Car x Queue → Integer; constrains New, CarArrives, CarDeparts, IsEmpty, NumberOfCars, Longer, FirstCar, Equal, WhichQueue, Position, so that Queue generated by [New, CarArrives]
IMPORTANT NOTES
- Description of the operations:
◦ CarArrives adds a car to the end of a queue
◦ CarDeparts removes a car from the front of a queue (the other side than the one where we add cars)
◦ IsEmpty returns true if a queue of cars is empty and false otherwise
◦ Longer returns true if a queue is longer than the integer and false otherwise (assume that the integer is never negative)
◦ NumberOfCars returns the number of cars in the queue
◦ FirstCar returns the car from the front of the queue without deleting it
◦ Equal returns true if number of cars in two queues is equal and false otherwise
◦ WhichQueue examines two queues and returns 1 if a given car is in the first queue, 2 if the car is in the second queue, and 0 if the car is not in the queues.
◦ Position examines if a given car is in a queue and returns the number of cars that are in front of this car in the queue (closer to the front of the queue) or -1 if this car is not in the queue
- You should provide only the axioms (including the for all and end statements)
- Be precise in terms of both syntax and symbols that you use
- Assume that error constant is available
◦ Assume that applying CarDeparts to empty queue generates error
◦ Assume that applying FirstCar to empty queue generates error
◦ Assume that = = and + operators are defined for the sort Integer
- Write neatly (preferably using a word processor)
