Specification language

A specification language is a formal language used in computer science. Unlike most programming languages, which are directly executable formal languages used to implement a system, specification languages are used during system analysis and design.

Specification languages are generally not directly executed. They describe the system at a much higher level than a programming language. Indeed, it is considered as an error if a requirement specification is cluttered with unnecessary implementation detail, because the specification is meant to describe the what, not the how.

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.

An important use of specification languages is enabling the creation of proofs of program correctness (see theorem prover).

=Specification languages=

*Actor model *Alloy language *Assertion definition language *B specification language *Common Algebraic Specification Language (CASL) *Extended ML *Java Modeling Language (JML) *Object Z *Planguage *Specification and Design Language *Unified Modeling Language *VDM specification language *Z specification language *Hartmann pipeline