ADT Axiomatic Specifications

This is individual work.

Specify the behavior using Guttag's axiomatic method. Use ML as a specification language, and test your specs by executing them on some test data.

Include your test data as ML code at the end of each ADT. Use this example as a guide... you will see at the end of the ML function definitions there is some test data (ML expressions to be evaluated) to exercise the operations of the ADT.


This item (0) is just practice.
Work it out to get used to using ML as a specification notation. You can start with the ML given for SET and make changes.

(0) multi-set (bag)

    A multi-set is a set that can have an item added to it more than once, 
    so every item in a set has a value and a count.  Here are the operations:  

      add : put an item in the set... this will increase the count by 1 for 
            an item already in the set
      rem : take an item out of the set
      in  : boolean... tells is an item is in the set (count above 0) or not
      n   : return the number of times an element is in the set (0 for 
            elements not in the set)
      empty : is the set empty?
      size : tell how many unique items are in the set
      num :  tell how many total items are in the set
      

Do these next 3 items to hand in

  1. ring

    This is a form of bounded queue; if the ring is full, and you add an item, then it over-writes the oldest item (the one at the front). You can think of the finite number of elements as being in a circle (the ring), and you keep adding around the ring. Operations will be new, add, rem, next (or front), size, max, empty, full.

  2. stomp stack

    This is a form of bounded stack; when you push an item on a full stack, it "mashes" the bottom item out of the stack to make room at the top. Operations are new, push, pop, top, size, max, empty, full. Remember you can create internal operations if they help you define the "public" operations.

  3. priority stack

    This will be an unbounded stack, and the stack contains elements that are "pairs": a value of some type, and an integer priority (with 0 as low priority). When you push an element, it percolates down toward the stack bottom until it hits an element with priority equal to or lower... and it stays there on top of that element. So within priority categories, it maintains stack order of the element values. Operations are new, push, pop, size, empty, topv, topp. We implement the "pair" concept by asking separately what value is on top (topv) and what priority the top element has (topp). This is just a suggestion; you may do it differently if you wish, such as creating a pair type with its own operations.