Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Specification language
open-in-new
<h2 id="overview">Overview</h2> <p>Specification languages are generally not directly executed. They are meant to describe the <i>what</i>, not the <i>how</i>. It is considered an error if a requirement specification is cluttered with unnecessary implementation detail. </p><p>A common fundamental assumption of many specification approaches is that programs are modelled as <a href="/facts/Algebra/nMdqczjo">algebraic</a> or <a href="/facts/Model_theory/vLWVV8sQ">model-theoretic</a> structures that include a collection of <a href="/facts/Set_(mathematics)/BfucfHMq">sets</a> of data values together with <a href="/facts/Function_(mathematics)/CdReEKCh">functions</a> 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. </p><p>In the <i>property-oriented</i> approach to specification (taken e.g. by <a href="/facts/Common_Algebraic_Specification_Language/DzHEY8Uu">CASL</a>), specifications of programs consist mainly of logical <a href="/facts/Axiom/mLjP14Mc">axioms</a>, usually in a <a href="/facts/Logical_system/KaeDAjK7">logical system</a> 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 <a href="/facts/Model-based_specification/UWM5zGme">model-oriented specification</a> in frameworks like <a href="/facts/Vienna_Development_Method/ormJgInD">VDM</a> and <a href="/facts/Z_notation/5mUjpTvv">Z</a>, which consist of a simple realization of the required behaviour. </p><p>Specifications must be subject to a process of <i>refinement</i> (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, <a href="/facts/Hartmann_pipeline/vweBvBn1">Hartmann pipelines</a>, when properly applied, may be considered a <a href="/facts/Dataflow/jea04eH2">dataflow</a> specification which <i>is</i> directly executable. Another example is the <a href="/facts/Actor_model/MJ49opnU">actor model</a> which has no specific application content and must be <i>specialized</i> to be executable. </p><p>An important use of specification languages is enabling the creation of <a href="/facts/Mathematical_proof/7ECDrU80">proofs</a> of <a href="/facts/Program_correctness/m4yxw3gw">program correctness</a> (<i>see <a href="/facts/Automated_theorem_prover/vKGvuKFI">theorem prover</a></i>). </p> <h2 id="languages">Languages</h2> <p class="note">Main page: Category:Formal specification languages</p> <ul><li><a href="/facts/ANSI/ISO_C_Specification_Language/kLPNR3E7">ACSL</a></li> <li><a href="/facts/Attempto_Controlled_English/21K4T1e1">Attempto Controlled English</a><a class="footnote-ref" id="fnref:2" href="#fn:2"><sup>2</sup></a></li> <li><a href="/facts/Common_Algebraic_Specification_Language/DzHEY8Uu">CASL</a></li> <li><a href="/facts/Vienna_Development_Method/ormJgInD">VDM</a></li> <li><a href="/facts/Z_notation/5mUjpTvv">Z notation</a></li> <li><a href="/facts/TLA%2B/cy4IfLBa">TLA+</a></li> <li>FizzBee (Python'ish design specification language)<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a></li> <li>LePUS3 (a visual, object-oriented design description language)</li> <li><a href="/facts/Perfect_Developer/aoh6twha">Perfect</a></li> <li><a href="/facts/Alloy_(specification_language)/Bdk1fLBJ">Alloy</a></li> <li><a href="/facts/Language_Of_Temporal_Ordering_Specification/UH9FXwDu">LOTOS</a></li> <li><a href="/facts/E-LOTOS/pwvyk46M">E-LOTOS</a></li> <li><a href="/facts/MML_(programming_language)/uThlhnpC">MML</a></li> <li>Refine Language<a class="footnote-ref" id="fnref:4" href="#fn:4"><sup>4</sup></a></li> <li><a href="/facts/SequenceL/TQWzwxGP">SequenceL</a></li> <li><a href="/facts/Symbolic_Model_Verification/FwvKMlw9">SMV</a></li> <li><a href="/facts/Specification_and_Design_Language/dW7Q5zIe">SDL</a></li> <li><a href="/facts/B-Method/qkkqG05M">B-Method</a></li></ul> <h2 id="see-also">See also</h2> <ul><li><a href="/facts/Formal_specification/4q2oDkvS">Formal specification</a></li> <li><a href="/facts/Language-independent_specification/cLfKVJcx">Language-independent specification</a></li> <li><a href="/facts/Specification_and_Description_Language/dW7Q5zIe">Specification and Description Language</a></li> <li><a href="/facts/Unified_Modeling_Language/3tlNS0tH">Unified Modeling Language</a></li></ul> <h2 id="external-links">External links</h2> <ul><li> Media related to Specification languages at Wikimedia Commons</li></ul> <h2 id="references">References</h2> <ol> <li id="fn:1"><p>Joseph Goguen "One, None, A Hundred Thousand Specification Languages" Invited Paper, IFIP Congress 1986 pp 995-1004 <a href="/wiki/Joseph_Goguen" target="_blank">/wiki/Joseph_Goguen</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li> <li id="fn:2"><p>Fuchs, Norbert E.; Schwertel, Uta; Schwitter, Rolf (1998). "Attempto Controlled English—not just another logic specification language" (PDF). International Workshop on Logic Programming Synthesis and Transformation. Lecture Notes in Computer Science. Vol. 1559. Springer. pp. 1–20. doi:10.1007/3-540-48958-4_1. ISBN 978-3-540-65765-1. <a href="978-3-540-65765-1" target="_blank">978-3-540-65765-1</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li> <li id="fn:3"><p>"Easiest-ever formal methods language for developers crafting distributed systems, microservices, and cloud applications". Retrieved May 28, 2024. <a href="https://fizzbee.io/" target="_blank">https://fizzbee.io/</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li> <li id="fn:4"><p>Linden, Theodore; Lawrence Markosian (1989). "Transformational Synthesis Using Refine". In Richer, Mark (ed.). AI Tools and Techniques. Ablex. pp. 261–286. ISBN 0-89391-494-0. Retrieved 6 July 2014. <a href="0-89391-494-0" target="_blank">0-89391-494-0</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li> </ol>