Specification language: Difference between revisions
imported>Comp.arch No edit summary |
imported>Jpbowen Added ref, facts, tidying |
||
| Line 1: | Line 1: | ||
{{Short description|Formal language used in computer science}} | {{Short description|Formal language used in computer science}} | ||
{{Refimprove|date=August 2016}} | {{Refimprove|date=August 2016}} | ||
A '''specification language''' is a [[formal language]] in [[computer science]] used during [[systems analysis]], [[requirements analysis]], and [[systems design]] to describe a system at a much higher level than a [[programming language]], which is used to produce the executable code for a system.<ref>[[Joseph Goguen]] | A '''specification language''' is a [[formal language]] in [[computer science]] used during [[systems analysis]], [[requirements analysis]], and [[systems design]] to describe a system at a much higher level than a [[programming language]], which is used to produce the executable code for a system.<ref>[[Joseph Goguen]], | ||
"One, None, A Hundred Thousand Specification Languages" Invited Paper, [[IFIP]] Congress 1986 pp | "One, None, A Hundred Thousand Specification Languages" Invited Paper, [[IFIP]] Congress 1986, pp. 995–1004.</ref> | ||
==Overview== | ==Overview== | ||
Specification languages are generally not directly executed. They are meant to describe the ''what'', not the ''how''. It is considered an error if a requirement specification is cluttered with unnecessary implementation detail. | Specification languages are generally not directly executed. They are meant to describe the ''what'', not the ''how''.<ref>{{cite journal| date=November 1989 | title=Specifications are not (necessarily) executable | first1=I.J. | last1=Hayes | first2=C.B. | last2=Jones | author-link2=Cliff Jones (computer scientist) | journal=[[Software Engineering Journal]] | volume=4 | issue=6 | doi=10.1049/sej.1989.0045 | url=https://www.researchgate.net/publication/2632227 }}</ref> It is considered 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]]ic or [[model theory|model-theoretic]] structures that include a collection of [[set (mathematics)|sets]] of data values together with [[function (mathematics)|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. | A common fundamental assumption of many specification approaches is that programs are modelled as [[algebra]]ic or [[model theory|model-theoretic]] structures that include a collection of [[set (mathematics)|sets]] of data values together with [[function (mathematics)|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 [[Common Algebraic Specification Language|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. | In the ''property-oriented'' approach to specification (taken, e.g., by [[Common Algebraic Specification Language|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-based specification|model-oriented specification]] in frameworks like [[Vienna Development Method|VDM]] and [[Z notation | This is in contrast to so-called [[model-based specification|model-oriented specification]] in frameworks like [[Vienna Development Method|VDM]] and the [[Z notation]], 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 | 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.{{fact|date=June 2026}} | ||
An important use of specification languages is enabling the creation of [[Mathematical proof|proof]]s of [[program correctness]] (''see [[Automated theorem prover|theorem prover]]''). | An important use of specification languages is enabling the creation of [[Mathematical proof|proof]]s of [[program correctness]] (''see [[Automated theorem prover|theorem prover]]'').{{fact|date=June 2026}} | ||
==Languages== | ==Languages== | ||
| Line 26: | Line 27: | ||
* [[TLA+|TLA<sup>+</sup>]] | * [[TLA+|TLA<sup>+</sup>]] | ||
* FizzBee (Python'ish design specification language)<ref>{{cite web |url=https://fizzbee.io/ |title=Easiest-ever formal methods language for developers crafting distributed systems, microservices, and cloud applications |accessdate=May 28, 2024}}</ref> | * FizzBee (Python'ish design specification language)<ref>{{cite web |url=https://fizzbee.io/ |title=Easiest-ever formal methods language for developers crafting distributed systems, microservices, and cloud applications |accessdate=May 28, 2024}}</ref> | ||
* | * LePUS3 (a visual, object-oriented design description language){{fact|date=June 2026}} | ||
* [[Perfect Developer|Perfect]] | * [[Perfect Developer|Perfect]] | ||
* [[Alloy (specification language)|Alloy]] | * [[Alloy (specification language)|Alloy]] | ||
Latest revision as of 19:43, 19 June 2026
Template:Short description Template:Refimprove A specification language is a formal language in computer science used during systems analysis, requirements analysis, and systems design to describe a system at a much higher level than a programming language, which is used to produce the executable code for a system.[1]
Overview
Specification languages are generally not directly executed. They are meant to describe the what, not the how.[2] It is considered 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 algebraic 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 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 specification in frameworks like VDM and the Z notation, 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.Script error: No such module "Unsubst".
An important use of specification languages is enabling the creation of proofs of program correctness (see theorem prover).Script error: No such module "Unsubst".
Languages
<templatestyles src="Div col/styles.css"/>
- ACSL
- Attempto Controlled English[3]
- CASL
- VDM
- Z notation
- TLA+
- FizzBee (Python'ish design specification language)[4]
- LePUS3 (a visual, object-oriented design description language)Script error: No such module "Unsubst".
- Perfect
- Alloy
- LOTOS
- E-LOTOS
- MML
- Refine Language[5]
- Rosetta-lang
- SequenceL
- SMV
- SDL
- B-Method
Script error: No such module "Check for unknown parameters".
See also
- Formal specification
- Language-independent specification
- Pseudocode
- Specification and Description Language
- Unified Modeling Language
References
<templatestyles src="Reflist/styles.css" />
- ↑ Joseph Goguen, "One, None, A Hundred Thousand Specification Languages" Invited Paper, IFIP Congress 1986, pp. 995–1004.
- ↑ Script error: No such module "Citation/CS1".
- ↑ Script error: No such module "citation/CS1".
- ↑ Script error: No such module "citation/CS1".
- ↑ Script error: No such module "citation/CS1".
Script error: No such module "Check for unknown parameters".
External links
Script error: No such module "Navbox".