queue: THEORY

 BEGIN

  QUEUE_ENTRY: TYPE

  QUEUE_TYPE: TYPE = [# head: nat, size: nat, entry: [nat -> QUEUE_ENTRY] #]

  queue: VAR QUEUE_TYPE

  qEntry: VAR QUEUE_ENTRY

  qPoint: VAR nat


  % Returns true if a queue is empty
  empty(queue): bool = size(queue) = 0

  % Pushes an entry onto a queue and returns the updated queue
  pushQentry(queue, qEntry): QUEUE_TYPE =
     queue WITH [size  := queue`size + 1,
                 entry := entry(queue)
                     WITH [(head(queue) + size(queue)) := qEntry]]

  % Pops an entry from a queue. It returns the new queue.
  popQentry(queue): QUEUE_TYPE =
      IF NOT empty(queue)
        THEN queue WITH [head := head(queue) + 1, 
                         size := size(queue) - 1]
      ELSE queue
      ENDIF

  % Returns true if entry qPoint of the queue is occupied,
  % that is, lies between the head and head + size
  occupied(queue, qPoint): bool =
      qPoint >= queue`head AND qPoint < queue`head + queue`size

  % Checks whether there is an occupied entry in the queue with value qEntry
  inQ(queue, qEntry): bool =
      EXISTS (index: nat):
        occupied(queue, index) AND queue`entry(index) = qEntry

  % If a queue is empty, no entries are occupied
  empty_no_occupied: LEMMA
    FORALL queue:
      empty(queue) IFF (FORALL qPoint: NOT occupied(queue, qPoint))

  % After pushing an entry onto a queue, the entry is in the queue
  pushed_entry_in_queue: LEMMA
    FORALL queue, qEntry: inQ(pushQentry(queue, qEntry), qEntry)

  % If one pushes an entry onto an empty queue, and then pops one off,
  % the queue is again empty.
  empty_push_pop_empty: LEMMA
    FORALL queue, qEntry:
      empty(queue) IMPLIES empty(popQentry(pushQentry(queue, qEntry)))

  

 END queue