Double ended queue data abstraction and axioms I am trying to show the data abstraction for a double ended queue along with the axioms. A double ended queue is a queue where items can be added to and remove from either end of the queue.  I have already got the abstraction and axioms for a normal queue but looking at it, it looks to me like it would also work for a double ended queue. If this isn't the case what changes need to be made to make it work for a double ended queue?

Specification Queue: 
Provides: Queue 
Other abstractions used: Item, Boolean 

Operations: NewQ: -&gt; Queue
AddQ: Queue, Item -&gt; Queue 
RearQ: Queue -&gt; Queue 
FrontQ: Queue -&gt; Item 
IsEmptyQ: Queue -&gt; Boolean

Axioms: 
RearQ(NewQ) := NewQ
RearQ(AddQ(q, i)) := If IsEmptyQ(q) then NewQ
           otherwise AddQ(RearQ(q), i) 
FrontQ(NewQ) := Error 
FrontQ(AddQ(q, i)) := If IsEmptyQ(q) then i
           otherwise FrontQ(q)
IsEmptyQ(NewQ) :- True
IsEmptyQ(AddQ(q, i)) := False 

Where: 
   i is of type Item,
   q is of type Queue
Like you say items can be added to a double ended queue on both sides, yet you have only a single AddQ operator. More substantial is the change to the axioms. An item added at the end can (after several operations) be retrieved from the front.