Specification language
A specification language is a formal language used in computer science. Unlike programming languages, which are directly executable formal languages used to implement a system, specification languages are used during system analysis and design. They 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.
A important use of specification languages is enabling the creation of proofs of program correctness (see theorem prover).
Specification languages
