In computer science, a formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not (necessarily) how the system should do it. Given such a specification, it is possible to use formal verification techniques to demonstrate that a candidate system design is correct with respect to the specification. This has the advantage that incorrect candidate system designs can be revised before a major investment has been made in actually implementing the design. An alternative approach is to use provably correct refinement steps to transform a specification into a design, and ultimately into an actual implementation, that is correct by construction.
A design (or implementation) cannot ever be declared “correct” in isolation, but only “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” theorems 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.
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 (Web services Quality of Service).
Other articles related to "formal specification, formal, specification":
... Business rules can be expressed in formal languages such as Unified Modeling Language, Z notation, Business Process Execution Language, Business Process ...
... Once a formal specification has been produced, the specification may be used as a guide while the concrete system is developed during the design process (i.e ... For example If the formal specification is in an operational semantics, the observed behavior of the concrete system can be compared with the behavior of the specification (which itself ... Additionally, the operational commands of the specification may be amenable to direct translation into executable code ...
... Formal ways for describing the syntax of the communications are Abstract Syntax Notation One (a ISO standard) or Augmented Backus-Naur form (a IETF standard) ...
Famous quotes containing the word formal:
“That anger can be expressed through words and non-destructive activities; that promises are intended to be kept; that cleanliness and good eating habits are aspects of self-esteem; that compassion is an attribute to be prizedall these lessons are ones children can learn far more readily through the living example of their parents than they ever can through formal instruction.”
—Fred Rogers (20th century)