Abstract Data Types & Contracts

An abstract data type (ADT) answers what clients may observe. A data structure answers how one implementation realizes it. A stack is LIFO whether its elements live in a dynamic array or linked nodes; a priority queue returns an extremal-priority item whether it uses a heap, balanced tree, or buckets. Keeping those layers separate lets an implementation change without rewriting every client—and exposes when two containers with similar method names actually promise different behavior.

The separator is a proof boundary. Client code reasons from operations and laws. Implementation code preserves a representation invariant and shows that every operation realizes the same abstract transition.

An ADT is values, operations, and laws #

A useful specification has at least four parts:

1. Abstract states or values. A queue can be modeled as a finite sequence $q=\langle x_0,\ldots,x_{n-1}\rangle$.
2. Operations. empty, size, front, push_back, and pop_front.
3. Preconditions and results. Is front(empty) illegal, optional, blocking, or a sentinel?
4. Laws. For example, after pushing $x$ into an empty queue, front returns $x$; removing the front from $\langle x\rangle\mathbin{+}q$ yields $q$.

Guttag's algebraic view specifies an operation by equations over other operations rather than by exposing fields. For a FIFO queue:

$$\mathop{\mathrm{front}}(\mathop{\mathrm{push}}(\langle\rangle,x))=x,$$

$$\mathop{\mathrm{front}}(\mathop{\mathrm{push}}(q,x))=\mathop{\mathrm{front}}(q) \quad\text{when }q\ne\langle\rangle.$$

Those equations reject a stack implementation even if both containers happen to offer push and pop: the observable removal order differs.

A production contract is wider than method names #

Two APIs can expose insert, erase, and find yet be incompatible. Specify every observable axis that clients may rely on:

Complexity is part of the interface only when its quantifier is explicit. “Constant append” can mean worst-case $O(1)$ for a linked tail, amortized $O(1)$ for a growing vector, or expected $O(1)$ for a hash-backed structure. These promises are not interchangeable on a latency-critical path.

From abstract value to representation #

To implement an ADT rigorously, define:

• a concrete representation set $C$;
• a representation invariant $I(c)$ identifying valid concrete states;
• an abstraction function $\alpha:C\to A$ mapping a valid concrete state to its abstract value.

For a ring-buffer queue with array data, capacity $m>0$, logical length $n$, and head index $h$:

$$0\le n\le m,\qquad 0\le h<m,$$

$$\alpha(data,h,n)= \langle data[h],data[(h+1)\bmod m],\ldots,data[(h+n-1)\bmod m]\rangle.$$

The physical array may wrap, but the abstract queue is one sequence. push_back(x) writes at $(h+n)\bmod m; pop_front()` advances $h$ and decrements $n$. Correctness requires proving each operation:

1. accepts only its declared precondition;
2. preserves $I$;
3. produces the abstract transition required by the contract;
4. meets the declared cost and failure guarantee.

This distinction also prevents representation leakage. A client that depends on the ring buffer's current head index is no longer programming against the queue ADT.

One ADT can have several honest representations #

Assume a stack of $n$ elements:

All three can satisfy LIFO laws. They do not satisfy the same resource, stability, or failure contract. Representation selection is therefore a workload decision made after semantics are fixed.

template<class T>
class Stack {
public:
    [[nodiscard]] bool empty() const noexcept;
    [[nodiscard]] std::size_t size() const noexcept;

    // Preconditions: !empty(). Reference remains valid only under the
    // invalidation rules promised by this particular Stack type.
    T& top();
    const T& top() const;

    void push(T value);
    void pop();  // Preconditions: !empty().
};

The interface sketch is still incomplete until documentation states invalidation, exception, allocator, and concurrency behavior. Types encode some obligations; prose and tests must encode the rest.

Refinement tests exercise laws, not layouts #

An implementation test should not assert that a queue's head index equals three. It should assert observable laws across command sequences:

• pushing a,b,c then repeatedly reading/removing front yields a,b,c;
• size changes by exactly one after successful push/pop;
• wraparound produces the same sequence as a non-wrapped reference model;
• a failed growth operation leaves the queue in its promised state;
• retained handles behave according to the invalidation contract.

A small executable reference model—often a plain sequence—can generate expected results for randomized operation traces. This is refinement testing: the concrete implementation and the model must remain observationally equivalent.

Representation invariants still deserve internal assertions and targeted tests. They diagnose the concrete cause; ADT-law tests prove clients cannot see a semantic difference.

Abstraction boundaries fail in predictable ways #

Choosing and reviewing an ADT #

Before choosing a container or approving an interface, answer:

1. What mathematical value does one instance represent?
2. What does each operation observe or change?
3. What happens on empty, full, absent, duplicate, and invalid input?
4. Which ordering is observable?
5. Which complexity quantifier and cost model are promised?
6. What survives mutation: values, addresses, iterators, indices, or no handles?
7. Who owns each object and when may it be reclaimed?
8. What state remains after allocation, comparison, or user-callback failure?
9. Which concurrent histories are legal?
10. What invariant and abstraction function let an implementation prove refinement?

If those questions have crisp answers, selecting a data structure becomes engineering. Without them, switching containers is guesswork.

Exercises #

1. Specify a bounded queue whose push rejects when full. Give abstract states, operations, and two laws.
2. Define an abstraction function for a stack stored in data[0:size).
3. Explain why std::priority_queue and a sorted set are not the same ADT despite both returning a maximum.
4. Design a law-based test that distinguishes FIFO from LIFO without inspecting representation.