Specification language
Encyclopedia
A specification language is a formal language
used in computer science
.
Unlike most programming language
s, which are directly executable formal languages used to implement a system, specification languages are used during systems analysis
, requirements analysis
and systems 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.
A common fundamental assumption of many specification approaches is that programs are modelled as algebra
ic 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 axiom
s, 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 pipeline
s, 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 proof
s of program correctness (see theorem prover).
Formal language
A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
used in computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
.
Unlike most programming language
Programming language
A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....
s, which are directly executable formal languages used to implement a system, specification languages are used during systems analysis
Systems analysis
Systems analysis is the study of sets of interacting entities, including computer systems analysis. This field is closely related to requirements analysis or operations research...
, requirements analysis
Requirements analysis
Requirements analysis in systems engineering and software engineering, encompasses those tasks that go into determining the needs or conditions to meet for a new or altered product, taking account of the possibly conflicting requirements of the various stakeholders, such as beneficiaries or users...
and systems design
Systems design
Systems design is the process of defining the architecture, components, modules, interfaces, and data for a system to satisfy specified requirements. One could see it as the application of systems theory to product development...
.
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 algebra
Algebra
Algebra is the branch of mathematics concerning the study of the rules of operations and relations, and the constructions and concepts arising from them, including terms, polynomials, equations and algebraic structures...
ic or model-theoretic
Model theory
In mathematics, model theory is the study of mathematical structures using tools from mathematical logic....
structures that include a collection of sets of data values together with functions
Function (mathematics)
In mathematics, a function associates one quantity, the argument of the function, also known as the input, with another quantity, the value of the function, also known as the output. A function assigns exactly one output to each input. The argument and the value may be real numbers, but they can...
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
Common Algebraic Specification Language
The Common Algebraic Specification Language is a general-purpose specification languagebased on first-order logic with induction. Partial functionsand subsorting are also supported....
), specifications of programs consist mainly of logical axiom
Axiom
In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...
s, 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
Model-based specification
Model-based specification is an approach to formal specification where the system specification is expressed as a system state model. This state model is constructed using well-understood mathematical entities such as sets and functions...
in frameworks like VDM
Vienna Development Method
The Vienna Development Method is one of the longest-established Formal Methods for the development of computer-based systems. Originating in work done at IBM's Vienna Laboratory in the 1970s, it has grown to include a group of techniques and tools based on a formal specification language - the VDM...
and Z
Z notation
The Z notation , named after Zermelo–Fraenkel set theory, is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.-History:...
, 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 pipeline
Hartmann pipeline
A Hartmann pipeline is an extension of the Unix pipeline concept, providing for more complex paths, multiple input/output streams, and other features. It is an example and extension of Pipeline programming....
s, when
properly applied, may be considered a dataflow
Dataflow
Dataflow is a term used in computing, and may have various shades of meaning. It is closely related to message passing.-Software architecture:...
specification which is directly executable. Another example is the Actor model
Actor model
In computer science, the Actor model is a mathematical model of concurrent computation that treats "actors" as the universal primitives of concurrent digital computation: in response to a message that it receives, an actor can make local decisions, create more actors, send more messages, and...
which has no specific application content and must be specialized to be executable.
An important use of specification languages is enabling the creation of proof
Mathematical proof
In mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...
s of program correctness (see theorem prover).
Languages
- CASLCommon Algebraic Specification LanguageThe Common Algebraic Specification Language is a general-purpose specification languagebased on first-order logic with induction. Partial functionsand subsorting are also supported....
- VDMVienna Development MethodThe Vienna Development Method is one of the longest-established Formal Methods for the development of computer-based systems. Originating in work done at IBM's Vienna Laboratory in the 1970s, it has grown to include a group of techniques and tools based on a formal specification language - the VDM...
- Z notationZ notationThe Z notation , named after Zermelo–Fraenkel set theory, is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.-History:...
- LePUS3Lepus3LePUS3 is a language for modelling and visualizing object-oriented programs and design patterns. It is defined as a formal specification language, formulated as an axiomatized subset of First-order predicate logic. A diagram in LePUS3 is also called a Codechart...
(a visual, object-oriented design description language) - PerfectPerfect DeveloperPerfect Developer is a tool for developing computer programs in a rigorous manner. It is used to develop applications in areas including IT systems and airborne critical systems. The principle is to develop a formal specification and refine the specification to code...
See also
- Formal specificationFormal specificationIn computer science, 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 how the system should do it...
- Language-independent specificationLanguage-independent specificationA language-independent specification is a programming language specification providing a common interface usable for defining semantics applicable toward arbitrary language bindings. LISs are language-agnostic...
- Unified Modeling LanguageUnified Modeling LanguageUnified Modeling Language is a standardized general-purpose modeling language in the field of object-oriented software engineering. The standard is managed, and was created, by the Object Management Group...
- SDL