Skip to content

Abstract Data Type Specification

Specification model — instantiates Representation-Independent Interface Contract

Specifies a type by its abstract values and operations, then pins any concrete storage to that meaning with a representation invariant and an abstraction function — so the storage can change without a client noticing.

An Abstract Data Type Specification describes a type by what its values mean and what its operations do, entirely apart from how it is stored. Its distinctive machinery is the pair that ties a chosen representation back to that meaning: a representation invariant — the predicate saying which concrete states are legal — and an abstraction function — the map from a legal concrete state to the abstract value it denotes.[1] Those two are what make this a model rather than a signature list: they let you prove that an implementation is faithful, and that swapping the storage preserves the type. Where the Interface Definition Language fixes the syntactic surface and the Design-by-Contract Clause states each operation's promise, this mechanism supplies the semantic value model both of those hang on.

Example

Consider a RationalNumber type. The abstract value is a mathematical rational; the operations are add, multiply, equals, numerator, denominator. The team picks a representation — a pair of integers (num, den) — and writes the two clauses that bind it to the meaning: the representation invariant is den > 0 and gcd(|num|, den) = 1 (always stored in lowest terms, positive denominator), and the abstraction function is AF(num, den) = num / den.

Now 1/2 and 2/4 are provably the same abstract value even though (2,4) is not even a legal representation — the invariant forbids it. Later the team can switch the internals to lazy, un-reduced pairs normalized on read, or to a big-integer continued-fraction form; as long as each operation preserves the invariant and the abstraction function still yields the same rational, no client can tell. When a bug surfaces where two equal rationals compare unequal, the specification localizes it instantly: someone constructed (2,4) without reducing — a representation-invariant violation inside the boundary — not a fault in any client.

How it works

  • Model the abstract value space and operation semantics first, with no mention of storage — what a value is and what each operation does to it.
  • Choose a representation, then write the representation invariant: the predicate that says which concrete states are valid.
  • Write the abstraction function: the map from each valid concrete state to the abstract value it stands for.
  • Discharge each operation against both: show it preserves the invariant and realizes the abstract semantics through the abstraction function.

The invariant-and-function pair is the part unique to this mechanism; without it you have a list of operations, not a specification that can certify a re-representation.

Tuning parameters

  • Abstraction level — how abstract the value model is (a "set of elements" versus an "insertion-ordered multiset"). More abstract leaves more implementation freedom but promises clients less.
  • Representation-invariant strictness — permissive versus a forced canonical form. Canonical forms make equality and reasoning trivial but push normalization work into every mutating operation.
  • Operation minimality — a small surface maximizes hiding and freedom; a rich one is convenient but pins down more behavior clients can come to rely on.
  • Specification formality — prose axioms through fully formal model-based notation (Z, VDM) or an algebraic axiom set. More formality enables proof but costs effort.
  • Checkability — whether the invariant is expressed so it can run as a checkRep assertion, trading a little speed for a guard that catches corruption at its source.

When it helps, and when it misleads

Its strength is a provable seam between meaning and storage: equality, correctness, and safe re-representation all anchor to the abstraction function and invariant, so a storage swap can be verified, not just hoped. Its failure modes are specific. An "abstraction function" that isn't actually a function — two concrete states that should denote different values collapsing to one, or a legal state mapping to nothing — silently corrupts every argument built on it. Over-specifying the value model bakes in incidental structure and removes the very freedom the exercise exists to protect. And the model can quietly drift from the code until the "specification" describes a type that no longer runs. The classic misuse is writing the spec after the fact to rationalize the current representation rather than to constrain it. The discipline that guards against all three: keep the invariant and abstraction function executable (checkRep), and treat any violation as a defect in the implementation, never a reason to loosen the model.

How it implements the components

This mechanism supplies the semantic model side of the archetype — the value meaning that the surface and the tests presuppose:

  • abstract_state_model — the abstract value space and operation semantics are this model, defined independent of storage.
  • representation_invariant — the predicate that declares which concrete states are legal representations.
  • abstraction_function_or_semantic_mapping — the map from a legal concrete state to the abstract value it denotes.

It does not declare the syntactic operation surface (that is the Interface Definition Language), state per-operation preconditions and error policy (the Design-by-Contract Clause), or provide an executable oracle that checks conformance (the Black-Box Contract Test Suite).

Notes

The representation invariant and abstraction function mention the representation — which looks like a contradiction of the archetype's "hide the representation" goal. The resolution is that they live strictly inside the boundary, as the implementer's correctness argument; they are never exposed to clients. Hiding the representation from clients and reasoning rigorously about it internally are the two halves of the same discipline.

References

[1] The representation invariant and abstraction function are the standard tools for relating a concrete data representation to the abstract value it implements, introduced in Hoare's "Proof of Correctness of Data Representations" (1972) and made central to abstract data types in Liskov's work. A representation is correct exactly when every operation preserves the invariant and commutes with the abstraction function. ↩