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, although research has been done in this area. They describe the system at a much higher level than a programming language, and thus must be subject to a process of refinement (the filling-in of implementation detail) before they can actually be implemented.

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

Specification languages

• Alloy language
• Assertion definition language
• B specification language
• Extended ML
• SDL
• Unified Modeling Language
• VDM specification language
• Z specification language