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, requirements analysis and design.
An example of a specification language is the Unified Modelling Language.

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.

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 is commensurate 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 specifications 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.

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

Types Of Specification Language:-
1) Formal Specification
2) Language independent Specification

1) Formal Specification:-
A formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not (necessarily) how the system should do it. Given such a specification, it is possible to use formal verification techniques to demonstrate that a candidate system design is correct with respect to the specification. This has the advantage that incorrect candidate system designs can be revised before a major investment has been made in actually implementing the design. An alternative approach is to use provably correct refinement steps to transform a specification into a design, and ultimately into an actual implementation, that is correct by construction.
It is important to note that a design (or implementation) cannot ever be declared “correct” in isolation, but only “correct with respect to a given specification”. Whether the formal specification correctly describes the problem to be solved is a separate issue. It is also a difficult issue to address, since it ultimately concerns the problem constructing abstracted formal representations of an informal concrete problem domain, and such an abstraction step is not amenable to formal proof. However, it is possible to validate a specification by proving “challenge” theorems concerning properties that the specification is expected to exhibit. If correct, these theorems reinforce the specifiers understanding of the specification and its relationship with the underlying problem domain. If not, the specification probably needs to be changed to better reflect the domain understanding of those involved with producing (and implementing) the specification.

Example
The Z notation is an example of a leading formal specification language. Others include the Specification Language(VDM-SL) of the Vienna Development Method and the Abstract Machine Notation (AMN) of the B-Method.

2) Language Independent Specification
A language-independent specification (LIS) is a programming language specification providing a common interface usable for defining semantics applicable toward arbitrary language bindings; in other words, LISs are language-agnostic. LISs also mitigate the risk that a certain language binding might reduce compatibility with other languages; an ideal LIS allows the language bindings to take advantage of features of a programming language uncompromisingly.