Double ended queue data abstraction.

[JamesBwoii]

Hi, I'm working through a question where I need to design the Deque data abstraction giving it's formal specification with axioms.

A deque is a queue where items can be added to and remove from either end of the queue.

I've already got an abstraction for a normal queue and from what I can see it also seems to apply for a deque. I was wondering if someone could just have a look an check.

View attachment 4342

Thanks!

 

[Future Bruno]

Formal Specification for a Deque:A deque is an abstract data type that models a linear structure, consisting of a collection of elements, where elements can be added to and removed from either the front or the back of the structure.Axioms: 1. A Deque D is a finite ordered collection of elements 2. The elements in a Deque are indexed from 0 to n-1, where n is the number of elements in the Deque. 3. There are two operations for adding elements to a Deque: enqueueFront(D, x) and enqueueBack(D, x)4. There are two operations for removing elements from a Deque: dequeueFront(D) and dequeueBack(D)5. After an element is added to a Deque, the element at the corresponding index will be the same as before. 6. If a Deque is empty, then calling any of the four operations will return an error. 7. enqueueFront(D,x) adds the element x to the front of the Deque D 8. enqueueBack(D,x) adds the element x to the back of the Deque D 9. dequeueFront(D) removes and returns the element at the front of the Deque D10. dequeueBack(D) removes and returns the element at the back of the Deque D