UNC-CH COMP 410

ADT Axiomatic Semantics

We have said in class that an ADT is

For example, the type INT is You should see some similarity here to the class in OO languages. A class is a collection of data (the fields of an object) and a collection of operations on that data (the methods). This is why classes are types in an OO language.

We define the meaning, or behavior, of an ADT using a formal/mathematical notation called axiomatic semantics. The method here is attributed to John Guttag, who not only pioneered the notation/approach, but also defined the systematic procedure of applying the notation so that we are sure all possible important behavior of the type gets defined in the axioms.

We will illustrate Guttag's method by defining the semantics for the STACK ADT (a special form of list where we add and delete and find only at the first position of the list).

Guttag's Method

Examples of Full Definitions

STACK of E (LIFO list)

A stack is a special form of list where the add, remove, and find operations all deal with only the first position of the list. We are not allowed to add items down in the list or look for them anyplace but at the beginning. We call it a LIFO list (Last In First Out) because the most recently added item will be the one you get when you get/find an item.

QUEUE of E (FIFO list)

A queue is a special form of list where we add items in the first position, but we remove an item only from the last position. As with stack, we do not manipulate or search any items in the interior of the list. We call it a FIFO list (First In First Out) because the oldest added item will be the one you get when you remove an item.

LISP LIST of E

An entire programming language called LISP was based on the LIST data structure. It was the first functional programming language, and it remains heavily used today (as the variant called Scheme).
A Lisp list could be used to program any list behavior you needed, but there were only a few basic operations that needed to be combined recursively to make general behavior happen. In Lisp, these operation were called "car" "cdr" and "cons" for historical reason related to the names of registers in the machine Lisp was first implemented on. "car" gave the first item on the list. "cdr" gave the list that remained if you removed the first item. "cons" was used to add an item onto the head of a list.
These axioms define the behavior of a Lisp List. Do they look familiar?

Bounded Stack of E (BST)

Here is a Bounded Stack (BST), where there is a limit to how many items the stack can hold. This limit is passed as a parameter to "new" when the stack is created, and then the push operation must make sure the limit is not exceeded. The behavior when pushing something onto a full BST is to just do nothing... the element is not addded, and nothing already in the stack is removed. It is treated basically like a no-op.
This semantic definition is given in ML syntax, so it can be executed by an ML interpreter for testing.

Bounded Stomp Stack of E (BSS)

Here is a variant of the BST that we call the Bounded Stomp Stack (BSS). It is bounded, but the behavior when trying to push onto a full BSS is not a no-op. Instead, the item at the bottom of the stack is tossed to make room for the new item at the top.
This semantic definition is given in ML syntax, so it can be executed by an ML interpreter for testing. Note that we do the "stomp"ing with a "helper" operation (here called stomp). The helper operation is not part of the public interface for the type, but it does allow us to write the axioms with more clarity.