It is considered an error if a requirement specification is cluttered with unnecessary implementation detail.
This level of abstraction coincides with the view that the correctness of the input/output behaviour of a program takes precedence over all its other properties.
This is in contrast to so-called model-oriented specification in frameworks like VDM and Z, which consist of a simple realization of the required behaviour.
For example, Hartmann pipelines, when properly applied, may be considered a dataflow specification which is directly executable.
An important use of specification languages is enabling the creation of proofs of program correctness (see theorem prover).