An Abstract Data Type (ADT) is a set of values, a set of functions that operate on the values, and a set of axioms.
From a programmer’s perspective:
- A set of values is the values of a data type such as boolean or an enum.
- A function would be a function without side effects: no globals, no parameter modification.
- An axiom would be a boolean expression that the data and functions must uphold.
The canonical example is the Stack of Items:
- // Function signatures
- new() -> Stack<Item>
- empty(Stack<Item>) -> boolean
- push(Stack<Item>, Item) -> Stack<Item>
- top(Stack<Item>) -> Item
- pop(Stack<Item>) -> Stack<Item>
- // Axioms
- for all s and i: !empty(push(s, i))
- for all s and i: top(push(s, i)) = i
- for all s and i: pop(push(s, i)) = s
The lines 3-8 define the call interfaces of the functions available for objects of type Stack<Item>:
- new(), which creates a new Stack<Item> out of thin air;
- empty(), which checks some property of a Stack<Item> and returns a boolean result;
- push(), which combines a Stack<Item> and an Item into a new Stack<Item>;
- top(), which retrieves an Item out of a Stack<Item>;
- pop(), which retrieves a Stack<Item> out of a Stack<Item>.
Since ADTs in their original definition do not allow modifying an existing stack, push() and pop() do not modify the stack but return a new stack. This can be inefficient, so in practice, programmers usually build a MutableStack class (and name it Stack because an immediate use for an immutable stack does not present itself).
However, mutable data can considerably complicated things, so I’ll stick with the immutable case for now and explore the effects of mutability in a later section.
The last four lines specify the axioms:
- empty(new()) tells us that the empty function will give us true for whatever the new function is returning;
- !empty(push(s, i)) tells us that the result of a push is never empty;
- top(push(s, i)) = i tells us that top will always return the Item that was last added via push;
- pop(push(s, i)) = s tells us that pop will always return the Stack as it was before the last push.
The last two axioms are the characteristic ones that make Stack a stack: they guarantee that a caller will get Items back in the reverse order in which they were added.
Note what is not defined in the axioms: The result of applying top or pop to an empty stack.
In general, if cases are left unspecified, it can be an oversight of the ADT’s author, or it could have been intentionally left open to further specification elsewhere (such as in a subtype or an implementation), or such a call would be in error.
In the Stack case, it is the latter, so we should reword the last two axioms:
- for all s, i where !empty(s): top(push(s, i)) = i
- for all s, i where !empty(s): pop(push(s, i)) = s
Or we could add the condition as a precondition to “top” and “pop”:
- top(Stack<Item> s) -> Item
- require !empty(s)
- pop(Stack<Item> s) -> Stack<Item>
- require !empty(s)