Formal specification

{{Short description|Aspect of computer science}} {{How-to|date=January 2026}} In [[computer science]], '''formal specifications''' are mathematically based techniques whose purpose is to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools.<ref name="a9-hierons">{{Cite journal | last1 = Hierons | first1 = R. M. | last2 = Bogdanov | first2 = K. | last3 = Bowen | first3 = J. P. | author-link3=Jonathan Bowen | last4 = Cleaveland | first4 = R. | last5 = Derrick | first5 = J. | last6 = Dick | first6 = J. | last7 = Gheorghe | first7 = M. | last8 = Harman | first8 = M. | author-link8=Mark Harman (computer scientist) | last9 = Kapoor | first9 = K. | last10 = Krause | first10 = P. | last11 = Lüttgen | first11 = G. | last12 = Simons | first12 = A. J. H. | last13 = Vilkomir | first13 = S. A. | author-link13=Sergiy Vilkomir | last14 = Woodward | first14 = M. R. | last15 = Zedan | first15 = H. | author-link15=Hussein Zedan | title = Using formal specifications to support testing | journal = [[ACM Computing Surveys]] | volume = 41 | issue = 2 | pages = 1 | year = 2009 | doi = 10.1145/1459352.1459354 | citeseerx = 10.1.1.144.3320 | s2cid = 10686134 }}</ref><ref name ="p223-gaudel">{{Cite book | last1 = Gaudel | first1 = M.-C. | chapter = Formal specification techniques | doi = 10.1109/ICSE.1994.296781 | title = Proceedings of 16th International Conference on Software Engineering | pages = 223–227 | year = 1994 | isbn = 978-0-8186-5855-6 | s2cid = 60740848 }}</ref> These specifications are ''formal'' in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.<ref name="lamsweerde-roadmap">{{Cite book | last1 = Lamsweerde | first1 = A. V. | chapter = Formal specification | doi = 10.1145/336512.336546 | title = Proceedings of the conference on the future of Software engineering - ICSE '00 | pages = 147–159 | year = 2000 | isbn = 978-1581132533 | s2cid = 4657483 }}</ref>

==Motivation== In each passing decade, computer systems have become increasingly more powerful and, as a result, they have become more impactful to society. Because of this, better techniques are needed to assist in the design and implementation of reliable software. Established engineering disciplines use mathematical analysis as the foundation of creating and validating product design. Formal specifications are one such way to achieve this in [[software engineering]] reliability as once predicted. Other methods such as [[Software testing|testing]] are more commonly used to enhance code quality.<ref name=a9-hierons />

==Uses== Given such a [[Specification (technical standard)|specification]], it is possible to use [[formal verification]] techniques to demonstrate that a system design is [[correctness (computer science)|correct]] with respect to its specification. This allows incorrect system designs to be revised before any major investments have been made into an actual implementation. Another approach is to use provably correct [[Program refinement|refinement]] steps to transform a specification into a design, which is ultimately transformed into an implementation that is ''correct by construction''.

A formal specification is ''not'' an [[implementation]], but rather it may be used to develop an implementation. Formal specifications describe ''what'' a system should do, not ''how'' the system should do it.

A good specification must have some of the following attributes: adequate, internally consistent, unambiguous, complete, satisfied, minimal.<ref name=lamsweerde-roadmap />

A good specification will have:<ref name=lamsweerde-roadmap /> * Constructability, manageability and evolvability * Usability * Communicability * Powerful and efficient analysis

One of the main reasons there is interest in formal specifications is that they will provide an ability to [[automated theorem proving|perform proofs]] on software implementations.<ref name=p223-gaudel /> These proofs may be used to validate a specification, verify correctness of design, or to prove that a program satisfies a specification.<ref name=p223-gaudel />

==Limitations== A design (or implementation) cannot ever be declared “correct” on its own. It can only ever be “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 [[domain (software engineering)|problem domain]], and such an abstraction step is not amenable to formal proof. However, it is possible to [[verification and validation|validate]] a specification by proving “challenge” [[theorem]]s concerning properties that the specification is expected to exhibit. If correct, these theorems reinforce the specifier's 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.

[[Formal methods]] of software development are not widely used in industry. Most companies do not consider it cost-effective to apply them in their software development processes.<ref name=Ch_27_Formal_spec>{{cite web| last=Sommerville | first=Ian | author-link=Ian Sommerville (academic) | title=Formal Specification | url=https://ifs.host.cs.st-andrews.ac.uk/Books/SE9/WebChapters/PDF/Ch_27_Formal_spec.pdf | work=Software Engineering | access-date=3 February 2013 | year=2009}}</ref> This may be for a variety of reasons, some of which are:

* Time ** High initial start-up cost with low measurable returns * Flexibility ** A lot of software companies use [[Agile software development|agile methodologies]] that focus on flexibility. Doing a formal specification of the whole system up front is often perceived as being the opposite of flexible. However, there is some research into the benefits of using formal specifications with "agile" development<ref name="p14-nummenmaasen">{{cite journal|last=Nummenmaa|first=Timo|author2=Tiensuu, Aleksi |author3=Berki, Eleni |author4=Mikkonen, Tommi |author5=Kuittinen, Jussi |author6= Kultima, Annakaisa |title=Supporting agile development by facilitating natural user interaction with executable formal specifications|journal=ACM SIGSOFT Software Engineering Notes|date=4 August 2011|volume=36|issue=4|pages=1–10|doi=10.1145/1988997.2003643|s2cid=2139235}}</ref> * Complexity ** They require a high level of mathematical expertise and the analytical skills to understand and apply them effectively<ref name=p14-nummenmaasen/> ** A solution to this would be to develop tools and models that allow for these techniques to be implemented but hide the underlying mathematics<ref name=p223-gaudel /><ref name=p14-nummenmaasen /> * Limited scope<ref name=lamsweerde-roadmap /> ** They do not capture properties of interest for all [[Requirements analysis#Stakeholder identification|stakeholders]] in the project<ref name=lamsweerde-roadmap /> ** They do not do a good job of specifying user interfaces and user interaction<ref name=Ch_27_Formal_spec /> * Not cost-effective ** This is not entirely true; by limiting their use to only core parts of critical systems they have shown to be cost-effective<ref name=Ch_27_Formal_spec />

Other limitations:<ref name=lamsweerde-roadmap /> * Isolation * Low-level ontologies * Poor guidance * Poor [[separation of concerns]] * Poor tool feedback

==Paradigms== Formal specification techniques have existed in various domains and on various scales for quite some time.<ref name="p179-vanderpoll">{{cite journal|last=van der Poll|first=John A.|author2=Paula Kotze|title=What design heuristics may enhance the utility of a formal specification?|journal=Proceedings of the 2002 Annual Research Conference of the South African Institute of Computer Scientists and Information Technologists on Enablement Through Technology|year=2002|series=SAICSIT '02|pages=179–194|isbn=9781581135961|url=http://dl.acm.org/citation.cfm?id=581506.581533}}</ref> Implementations of formal specifications will differ depending on what kind of system they are attempting to model, how they are applied and at what point in the software life cycle they have been introduced.<ref name=p223-gaudel /> These types of models can be categorized into the following specification paradigms:

* History-based specification<ref name=lamsweerde-roadmap /> ** behavior based on system histories ** assertions are interpreted over time * State-based specification<ref name=lamsweerde-roadmap /> ** behavior based on system states ** series of sequential steps, (e.g. a financial transaction) ** languages such as [[Z notation|Z]], [[Vienna Development Method|VDM]] or [[B-Method|B]] rely on this paradigm<ref name=lamsweerde-roadmap /> * Transition-based specification<ref name=lamsweerde-roadmap /> ** behavior based on transitions from state-to-state of the system ** best used with a reactive system ** languages such as Statecharts, PROMELA, STeP-SPL, RSML or SCR rely on this paradigm<ref name=lamsweerde-roadmap /> * Functional specification<ref name=lamsweerde-roadmap /> ** specify a system as a structure of mathematical functions ** OBJ, ASL, PLUSS, LARCH, HOL or PVS rely on this paradigm<ref name=lamsweerde-roadmap /> * Operational Specification<ref name=lamsweerde-roadmap /> ** early languages such as [[Paisley (programming language)|Paisley]], GIST, Petri nets or process algebras rely on this paradigm<ref name=lamsweerde-roadmap /> * Multi-paradigm languages ** FizzBee is a multi-paradigm specification language that allows for transition/action based specification, behavioral specifications with non-atomic transitions and also has actor model.

In addition to the above paradigms, there are ways to apply certain heuristics to help improve the creation of these specifications. The paper referenced here best discusses heuristics to use when designing a specification.<ref name=p179-vanderpoll /> They do so by applying a [[Divide and conquer algorithm|divide-and-conquer]] approach.

==Software tools== 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]]. In the [[Web services]] area, formal specification is often used to describe non-functional properties<ref>S-Cube Knowledge Model: [http://www.s-cube-network.eu/km/terms/f/formal-specification Formal Specification]</ref> (Web services [[quality of service]]).

==References== {{Reflist|30em}}

==External links== {{Commonscat}} * ''[http://kuro5hin.org/story/2005/7/29/04553/9714 A Case for Formal Specification (Technology)]'' {{Webarchive|url=https://web.archive.org/web/20051021002908/http://www.kuro5hin.org/story/2005/7/29/04553/9714 |date=2005-10-21 }} by Coryoth 2005-07-30

[[Category:Formal specification| ]] [[Category:Formal methods]] [[Category:Formal specification languages| Formal specification]]