Engineering Assignment 3 Solution

Description

1. (10 pts) 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)

Due Dates and Notes

Your assignment should be submitted via eClass.