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)