UNC-CH COMP 410
ADT Axiomatic Semantics
We have said in class that an ADT is
- a collection of data values
- a collection of operations that manipulate or transform those data values
For example, the type INT is
the value set { ... -4, -3, -2, -1, 0, 1, 2, 3, ... } and
the operation set {+, -, /, *, factors, prime, (whatever) ... }.
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
- FIRST: We define the functional signatures of the operations in the type.
A signature is a function name, then the types of the parameters, then the type
of the return value.
Unlike OO classes, where we think of the object as performing methods on itself,
we are here thinking of an object as being one of the parameters passed to the
function, and perhaps a (transformed) object being returned by the function.
The operation "pop" (for example) takes a STACK as a parameter, and
returns a (transformed) STACK as return value.
Here are the signatures for STACK; we assume the elements in a stack are of some type E:
new: --> STACK
push: STACK x E --> STACK
pop: STACK --> STACK
top: STACK --> E
size: STACK --> nat (naturals, int >=0 )
empty: STACK --> boolean
The first operation "new" will be in most of the ADTs we look at, is some form or another.
It creates an element of type STACK out of nothing (it takes no arguments). It is like the
constructor methods you find in OO class definitions.
In this ADT notation, we call "push" and "pop" constructors as well,
since they return an element of type STACK. Unlike "new", these other constructors do take
arguments.
- SECOND: Pick canonical constructors.
Consider the operations that return a value of type STACK. These are new, push, and pop,
and we call them constructors.
Of these constructors, we ask which are necessary if we wish to build all values of type STACK.
Some will be necessary (canonical) and some just conveniences (non-canonical).
We can construct all elements of type STACK this way:
- first call new,
- then call a bunch of push operations in nested form to put the proper elements into the
stack in the proper order.
For example, the stack where 2 is on the bottom, then 8 appears on the 2, and finally 5 is on
top can be made this way:
push(push(push(new,2),8),5)
Since push takes a STACK as first argument, and also returns a STACK, we can feed the output
of one push as input to the next.
The operation pop is not needed as canonical. We reason this way: any stack that can
be made with a pop operation in the nested construction sequence, can also be
made with a shorter sequence containing only push and new. For example:
push(pop(push(push(new,2,),8)),5) is the same stack as
push(push(new,2,),5)
So we choose new and push as canonical constructors.
We now have our operations divided into 3 kinds:
-
canonical constructors: new, push
-
other (non-canonical) constructors: pop
-
examiners: size, empty, top
We have already said that constructors are operations that produce STACKS.
Examiners are what allow us to tell one element of type STACK from another.
Examiners are the only way we can get information about the structure and contents
of a STACK value. If A and B are two elements of type STACK, we can
tell that they are different, for example, if top(A) != top(B), or if
size(A) != size(B).
- THIRD: Write axioms to define behavior.
An axiom is a statement of equivalence. We write one by
calling an examiner operation on the STACK produced by a
canonical constructor (the Left Hand Side, or LHS), and
then creating a Right Hand Side (RHS) expression that
we will declare to be equal to (or the same as) the LHS.
For example,
size(new) = 0
new is a canonical constructor, it creates a STACK value. size is
an examiner, and we can apply it to the STACK value we created with "new".
The value for that size we set as RHS and declare the two expressions
to be "=". Another:
size(push(S,e)) = size(S) + 1
The LHS is the STACK made by push(S,e) passed to the examiner size.
Here, S and e are just variables representing some arbitrary other STACK value and
some arbitrary element of type E.
The RHS says that we get the same number if we ask the size of the STACK S we
did the push on, and then add 1.
Now for the real power of Guttag's method. To get a complete set of axioms, we make
all possible combinations of examiners/non-canonicals applied to all possible canonicals
as LHS. We then figure the correct RHS to equate with each LHS. Done.
For STACK we have 4 examiner/non-canonicals, and 2 canonicals. This is 4*2 or 8 combinations
for LHS. It looks like this:
LHS = RHS
size(new) = 0
size(push(S,e)) = size(S) + 1
empty(new) = true
empty(push(S,e)) = false
top(new) = error
top(push(S,e)) = e
pop(new) = new
pop(push(S,e)) = S
The LHS are generated systematically as combinations. The RHS are generated by thinking
over the behavior of the ADT and expressing the transformation as a simplified
expression using the operations on hand.
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.