UNC-CH COMP 410
ADT Axiomatic Semantics
QUEUE of E (FIFO list)
QUEUE is the type we are defining
The list/queue contains elements of some type E
signatures (operations and types of parameters/return value)
new: --> QUEUE
enq: QUEUE x E --> QUEUE
deq: QUEUE --> QUEUE
front: QUEUE --> E
back: QUEUE --> E
size: QUEUE --> nat (naturals, int >=0 )
empty: QUEUE --> boolean
axioms (behavior)
empty(new) = true
empty(enq(Q,e)) = false
size(new) = 0
size(enq(Q,e)) = size(Q)+1
back(new) = error
back(enq(Q,e)) = e
front(new) = error
front(enq(Q,e)) = if (empty(Q)) then e
else front(Q)
deq(new) = new
deq(enq(Q,e)) = if (empty(Q)) then new
else enq(deq(Q),e)