abstract-data-types
Specifications for ADTs
(from Composing Software by Eric Elliott)
Several criteria can be used to judge the fitness of an ADT specification. I call these criteria FAMED, but I only invented the mnemonic. The original criteria were published by Liskov and Zilles in their famous 1975 paper, “Specification Techniques for Data Abstractions.”
Formal Specifications must be formal. The meaning of each element in the specification must be defined in enough detail that the target audience should have a reasonably good chance of constructing a compliant implementation from the specification. It must be possible to implement an algebraic proof in code for each axiom in the specification.
Applicable ADTs should be widely applicable. An ADT should be generally reusable for many different concrete use-cases. An ADT which describes a particular implementation in a particular language in a particular part of the code is probably over-specifying things. Instead, ADTs are best suited to describe the behavior of common data structures, library components, modules, programming language features, etc. For example, an ADT describing stack operations, or an ADT describing the behavior of a promise.
Minimal ADT specifications should be minimal. The specification should include the interesting and widely applicable parts of the behavior and nothing more. Each behavior should be described precisely and unambiguously, but in as little specific or concrete detail as possible. Most ADT specifications should be provable using a handful of axioms.
Extensible ADTs should be extensible. A small change in a requirement should lead to only a small change in the specification. Declarative.
Declarative specifications describe what, not how. ADTs should be described in terms of what things are, and relationship mappings between inputs and outputs, not the steps to create data structures or the specific steps each operation must carry out.
A good ADT should include:
Human readable description ADTs can be rather terse if they are not accompanied by some human readable description. The natural language description, combined with the algebraic definitions, can act as checks on each other to clear up any mistakes in the specification or ambiguity in the reader’s understanding of it.
Definitions Clearly define any terms used in the specification to avoid any ambiguity.
Abstract signatures Describe the expected inputs and outputs without linking them to concrete types or data structures. Axioms. Algebraic definitions of the axiom invariants used to prove that an implementation has satisfied the requirements of the specification.