A particular approach to writing abstract specifications for programs, modules, or data types. What distinguishes this approach is the fact that specifications are expressed purely in terms of the effects of operations characteristic of the system, and not in terms of their implementations or of the particular representation of any data involved. A specification in this style consists of a collection Σ‎ of operation names, together with a collection T of axioms that express how these operations combine with each other. The operation names can be thought of as comprising a signature, and the axioms are written in a formal logical language over the signature, such as first-order logic; thus T could be a first-order theory over Σ‎. An implementation of the operation names can be thought of as an algebra over that signature, satisfying the axioms. See also formal specification. Compare constructive specification.