What is Property-Oriented Formal Specification Language

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.