module specification A precise statement of the effects that a software module is required to achieve. It can be employed both by the implementer of the module, since it gives a definitive statement of the requirements that are imposed on the module, and by users of the module, since it gives a precise statement of what the module provides. A good module specification makes no commitment as to how the module's effects are achieved.

A variety of techniques have been developed for module specification. A functional specification identifies the operations that the module makes available and provides an individual specification for each operation, typically in the form of an input-output specification describing the mapping that the operation provides from a set of input values to a set of output values. In the typical case where a module has local data, a simple functional specification will need to refer to this local data when specifying each individual operation. This tends to obscure the specification, and also violates the principle that a specification should state what a module does but not how this is done.

The state machine model technique developed by Parnas treats the module as a finite-state machine and distinguishes operations that can observe the state of the machine from those that can alter the state of the machine. The specification is given by indicating the effect of each operation that can change the state on the result of each operation than can observe the state. This technique therefore avoids the need to refer to the module's local data.

The same applies to the technique of algebraic specification, largely due to Guttag and Horning. With this technique, which is tailored to the specification of abstract data type modules, the specification is given in two parts – a syntactic specification and a set of equations. The syntactic specification states the names, domains, and ranges of the operations provided by the module. Each equation specifies the net effect of some sequence of operations (or perhaps a single operation), and the complete set of equations must be sufficient to specify the effects of all operations under all conditions.

Because of the need for precision, module specifications are best given in some formal specification language. A variety of such languages have been developed, many drawing heavily on first-order predicate calculus. Specific examples include the SPECIAL language of the HDM system, which adopts the finite-state machine approach, and the language used by the AFFIRM system, which employs algebraic specification techniques.