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: -> Queue AddQ: Queue, Item -> Queue RearQ: Queue -> Queue FrontQ: Queue -> Item IsEmptyQ: Queue -> 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