program specification
   HOME

TheInfoList



OR:

In
computer science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied 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. 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.


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 Software engineering is a branch of both computer science and engineering focused on designing, developing, testing, and maintaining Application software, software applications. It involves applying engineering design process, engineering principl ...
reliability as once predicted. Other methods such as testing are more commonly used to enhance code quality.


Uses

Given such a
specification A specification often refers to a set of documented requirements to be satisfied by a material, design, product, or service. A specification is often a type of technical standard. There are different types of technical or engineering specificati ...
, it is possible to use
formal verification In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal ver ...
techniques to demonstrate that a system design is 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 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 Implementation is the realization of an application, execution of a plan, idea, scientific modelling, model, design, specification, Standardization, standard, algorithm, policy, or the Management, administration or management of a process or Goal ...
, 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. A good specification will have: * 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 perform proofs on software implementations. These proofs may be used to validate a specification, verify correctness of design, or to prove that a program satisfies a specification.


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 problem domain, and such an abstraction step is not amenable to formal proof. However, it is possible to validate a specification by proving “challenge”
theorem In mathematics and formal logic, a theorem is a statement (logic), statement that has been Mathematical proof, proven, or can be proven. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to esta ...
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 In computer science, formal methods are mathematics, mathematically rigorous techniques for the formal specification, specification, development, Program analysis, analysis, and formal verification, verification of software and computer hardware, ...
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. 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 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 * Complexity ** They require a high level of mathematical expertise and the analytical skills to understand and apply them effectively ** A solution to this would be to develop tools and models that allow for these techniques to be implemented but hide the underlying mathematics * Limited scope ** They do not capture properties of interest for all stakeholders in the project ** They do not do a good job of specifying user interfaces and user interaction * 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 Other limitations: * Isolation * Low-level ontologies * Poor guidance * Poor
separation of concerns In computer science, separation of concerns (sometimes abbreviated as SoC) is a design principle for separating a computer program into distinct sections. Each section addresses a separate '' concern'', a set of information that affects the code o ...
* Poor tool feedback


Paradigms

Formal specification techniques have existed in various domains and on various scales for quite some time. 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. These types of models can be categorized into the following specification paradigms: * History-based specification ** behavior based on system histories ** assertions are interpreted over time * State-based specification ** behavior based on system states ** series of sequential steps, (e.g. a financial transaction) ** languages such as Z, VDM or B rely on this paradigm * Transition-based specification ** 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 * Functional specification ** specify a system as a structure of mathematical functions ** OBJ, ASL, PLUSS, LARCH, HOL or PVS rely on this paradigm * Operational Specification ** early languages such as Paisley, GIST, Petri nets or process algebras rely on this paradigm * 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. They do so by applying a divide-and-conquer approach.


Software tools

The
Z notation The Z notation 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 In 1974, Jean-Raymond Abria ...
is an example of a leading formal
specification language 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 exec ...
. 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 A web service (WS) is either: * a service offered by an electronic device to another electronic device, communicating with each other via the Internet, or * a server running on a computer device, listening for requests at a particular port over a n ...
area, formal specification is often used to describe non-functional propertiesS-Cube Knowledge Model
Formal Specification
/ref> (Web services
quality of service Quality of service (QoS) is the description or measurement of the overall performance of a service, such as a telephony or computer network, or a cloud computing service, particularly the performance seen by the users of the network. To quantitat ...
). Some tools are: * Algebraic *# Larch *# OBJ *# Lotos * Model-based *# Z *# B *# VDM *# CSP *# Petri Nets *#
TLA+ TLA+ is a formal specification language developed by Leslie Lamport. It is used for designing, modelling, documentation, and verification of programs, especially concurrent systems and distributed systems. TLA+ is considered to be exhaustively-te ...
*# FizzBee


References


External links

*
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 Formal methods Formal specification