This article needs additional citations for verification. (August 2016) (Learn how and when to remove this template message)
A specification language is a formal language in computer science used during systems analysis, requirements analysis, and systems design to describe a system at a much higher level than a programming language, which is used to produce the executable code for a system.
Specification languages are generally not directly executed. They are meant to describe the what, not the how. Indeed, it is considered as an error if a requirement specification is cluttered with unnecessary implementation detail.
A common fundamental assumption of many specification approaches is that programs are modelled as algebraic or model-theoretic structures that include a collection of sets of data values together with functions over those sets. 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.
In the property-oriented approach to specification (taken e.g. by CASL), specifications of programs consist mainly of logical axioms, usually in a logical system in which equality has a prominent role, describing the properties that the functions are required to satisfy - often just by their interrelationship. 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.
Specifications must be subject to a process of refinement (the filling-in of implementation detail) before they can actually be implemented. The result of such a refinement process is an executable algorithm, which is either formulated in a programming language, or in an executable subset of the specification language at hand. For example, Hartmann pipelines, when properly applied, may be considered a dataflow specification which is directly executable. Another example is the Actor model which has no specific application content and must be specialized to be executable.
- Fuchs, Norbert E., Uta Schwertel, and Rolf Schwitter. "Attempto Controlled English—not just another logic specification language." International Workshop on Logic Programming Synthesis and Transformation. Springer, Berlin, Heidelberg, 1998.
- Linden, Theodore; Lawrence Markosian (1989). "Transformational Synthesis Using Refine". In Mark Richer (ed.). AI Tools and Techniques. Ablex. pp. 261–286. ISBN 0-89391-494-0. Retrieved 6 July 2014.