Page 352 -

12.5 Formal specification 335

Increasing Contractor Involvement

Decreasing Client Involvement
User System
Formal
Requirements Requirements Architectural Specification High-Level
Design
Definition Specification Design

Specification

Design

The advantages of developing a formal specification and using this in a formal
Figure 12.12 Formal
specification in a development process are:
plan-based software
process 1. As you develop a formal specification in detail, you develop a deep and detailed
understanding of the system requirements. Even if you do not use the specifica-
tion in a formal development process, requirements error detection is a potent
argument for developing a formal specification (Hall, 1990). Requirements
problems that are discovered early are usually much cheaper to correct than if
they are found at later stages in the development process.
2. As the specification is expressed in a language with formally defined semantics,
you can analyze it automatically to discover inconsistencies and incompleteness.
3. If you use a method such as the B method, you can transform the formal speci-
fication into a program through a sequence of correctness-preserving transfor-
mations. The resulting program is therefore guaranteed to meet its specification.
4. Program testing costs may be reduced because you have verified the program
against its specification.

In spite of these advantages, formal methods have had limited impact on practical
software development, even for critical systems. Consequently, there is very little
experience in the community of developing and using formal system specifica-
tions. The arguments that are put forward against developing a formal system
specification are:

1. Problem owners and domain experts cannot understand a formal specification
so they cannot check that it accurately represents their requirements. Software
engineers, who understand the formal specification, may not understand the
application domain so they too cannot be sure that the formal specification is an
accurate reflection of the system requirements.

2. It is fairly easy to quantify the costs of creating a formal specification, but more
difficult to estimate the possible cost savings that will result from its use. As a
result, managers are unwilling to take the risk of adopting this approach.