A specification language is a

formal language In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules. The alphabet of a formal language consists of s ...

computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includin ...

used during

systems analysis Systems analysis is "the process of studying a procedure or business to identify its goal and purposes and create systems and procedures that will efficiently achieve them". Another view sees system analysis as a problem-solving technique tha ...

requirements analysis In systems engineering and software engineering, requirements analysis focuses on the tasks that determine the needs or conditions to meet the new or altered product or project, taking account of the possibly conflicting requirements of the ...

, and

systems design Systems design interfaces, and data for an electronic control system to satisfy specified requirements. System design could be seen as the application of system theory to product development. There is some overlap with the disciplines of system an ...

to describe a system at a much higher level than a

programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming l ...

, which is used to produce the executable code for a system.

Joseph Goguen __NOTOC__ Joseph Amadee Goguen ( ; June 28, 1941 – July 3, 2006) was an American computer scientist. He was professor of Computer Science at the University of California and University of Oxford, and held research positions at IBM and SRI ...

"One, None, A Hundred Thousand Specification Languages" Invited Paper, IFIP Congress 1986 pp 995-1004

Overview

Specification languages are generally not directly executed. They are meant to describe the ''what'', not the ''how''. Indeed, it is considered as an error if a requirement specification is cluttered with unnecessary implementation detail. A common fundamental assumption of many specification approaches is that programs are modelled as

algebra Algebra () is one of the areas of mathematics, broad areas of mathematics. Roughly speaking, algebra is the study of mathematical symbols and the rules for manipulating these symbols in formulas; it is a unifying thread of almost all of mathem ...

ic or model-theoretic structures that include a collection of sets of data values together with functions over those sets. This level of abstraction coincides 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 An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy o ...

s, usually in a

logical system A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A for ...

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 {{Infobox programming language , name = Pipelines , logo = image:pipjarg1.jpeg , paradigm = Dataflow programming , year = 1986 , developer = IBM , designer = John P. Hartmann ( IBM) , latest_release_version = 1.1.12/0012 , latest_release_date = ...

s, when properly applied, may be considered a

dataflow In computing, dataflow is a broad concept, which has various meanings depending on the application and context. In the context of software architecture, data flow relates to stream processing or reactive programming. Software architecture Da ...

specification which ''is'' directly executable. Another example is the

actor model The actor model in computer science is a mathematical model of concurrent computation that treats ''actor'' as the universal primitive of concurrent computation. In response to a message it receives, an actor can: make local decisions, create mor ...

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 Proof most often refers to: * Proof (truth), argument or sufficient evidence for the truth of a proposition * Alcohol proof, a measure of an alcoholic drink's strength Proof may also refer to: Mathematics and formal logic * Formal proof, a con ...

s of

program correctness In theoretical computer science, an algorithm is correct with respect to a specification if it behaves as specified. Best explored is ''functional'' correctness, which refers to the input-output behavior of the algorithm (i.e., for each input it ...

(''see theorem prover'').

Languages

References

External links

* {{Computer language Computer languages Scientific modelling Formal specification

Overview

Languages

See also

References

External links