Abstract
Nowadays, software engineering (SE) is considered more frequently an engineering discipline. Several definitions have been proposed by different authors, and many of them agree in affirming that SE is the application of principles and systematic practices for the development of software. That is—as it was established by the IEEE (1990)—SE is the application of engineering to the software. As a general rule all engineering applications use mathematics or mathematical tools as a basis for their development. However, software engineering is an exception to this rule. Not all the techniques and software development methods have a formal basis. Formal methods1 (FM) rely on mathematical foundations. FM are a collection of methodologies and related tools, geared to the production of software employing a mathematical basis. There are a number of different formal methods each having its own methodology and tools, specially a specification language. As it is expressed in Wikipedia (2006) and Foldoc (2006), we can say that FM are “mathematically based techniques for the specification, development and verification of software and hardware systems.” FM are based on the production of formal specifications— for which they have a formal language to express it. Sometimes there is also a method to use the language in the software development process. The aims of FM can vary according to the different methodologies, but they all shared a common goal: the production of software with the utmost quality mainly based on the production of software that is error free. To achieve this, the different FM have developed not only a theory, but also different tools to support the formal process. FM can cover all the steps of the life cycle of a software system development from requirement specification to deployment and maintenance. However, not all FM have that capacity, and not always it is convenient to apply them. It is necessary to make an evaluation between pros and cons before applying FM in the software development process.
TopIt is important to make a distinction between a formal notation or language and a formal system. A formal notation is used to produce a formal specification, and it has a formal syntax and semantics. A formal system, besides these two components, includes a proof system—the deductive mechanism of the formal system. The syntax is described by a grammar and defines the set of well-formed formulas of the language. The meaning of these formulas is given by the semantics of the language. Finally, the syntactic manipulations of these formulas are achieved by using the inference mechanism of the formal system, which allows the derivation of new well-formed formulas from those present in the language.
Alagar and Peruyasamy (1998) establish that the difference between a FM and a formal system is the automatic support for specification and the availability of mechanized proofs.
All FM are based on mathematical formalisms, but we can distinguish two different development approaches. On the one hand, we can find the transformational methods based in transformations and on the other hand, those based in the “invent and verify” principle. The former rely for development on a calculus or transformation, where the engineer starts with an expression and then following predefined rules applies them to obtain an equivalent expression. Successive calculations lead to implementation. In FM relying on “invent and verify” technique, the engineer starts by inventing a new design, which afterward needs to be verified as correct. From this verified design implementation follows.
There are several styles of formal specification. Some are mutually compatible, while others are not. Table 1 shows a possible classification of the different styles.
Key Terms in this Chapter
Semantics: In a language, it is the meaning of a string, as opposed to syntax, that describes how the symbols of the language are combined. Most programming languages have their syntax defined formally (traditionally in BNF), while formal specification languages have also their semantics defined formally.
Verification: The process of determining whether or not the products of a specification phase fulfill a set of established requirements. Sometimes this is also used to indicate the process of proving that a more concrete specification preserves the properties of a more abstract specification.
Applicative-Oriented Formal Specification Language: Does not allow the use of variables.
Specification: A document describing what a system should do, what a problem is, or what a domain is all about. In formal methods this document is written in a formal language.
Property-Oriented Formal Specification Language: Based on axiomatic definitions. Abstract.