Annex 1 5.3 Category of Methods "Formal Specification" (FS)

FS - Formale Spezifikation

#### 5.3.1 Overview

A Formal Specification is a specification in a formal notation the semantics of which are uniquely (formally) defined.

#### 5.3.1.1 Appraisal Criteria

The following contains a list of criteria helping to select individual methods:
• level abstraction of the specification,
• existence of parallelism,
• main emphasis of the specification (e. g. are characteristics or sequences to be described),
• is there planned a formal (program/design) verification?
• applied programming language,
• availability of tools.

#### 5.3.1.2 Individual Methods

The individual methods of FS

are presented in the following individual descriptions. In order to make it easier to distinguish between the individual methods these methods are first compared with each other.

#### 5.3.1.3 Comparison of the individual Methods

The objective of the FS methods is identical. The specification is done without a language which is easy to understand (like the informal specification). By means of the formal language uniqueness is reached in the statements (example for an ambiguity in natural language: "He likes her cooking").

Mathematical Specification Axiomatic Specification (Algebraic Specification) Algorithmic Specification Specification by Traces Specification by Temporal Logic
Sequences hardly describable Sequences hardly describable Sequences describable by computation rules Sequences describable by traces Sequences describable by temporal operators
Suitable for all levels of abstraction Especially suitable for the first levels of abstraction Especially suitable for the last levels of abstraction Suitable for all levels of abstraction Suitable for all levels of abstraction
Only suitable for terminating operations Also suitable for the description of non terminating operations Also suitable for the description of non terminating operations Also suitable for the description of non terminating operations Also suitable for the description of non terminating operations

Table 5.3: FS: Differences between Individual Methods

#### 5.3.2 Individual Descriptions

5.3.2.1 Mathematical Specification
5.3.2.2 Axiomatic Specification (Algebraic Specification)
5.3.2.3 Algorithmic Specification
5.3.2.4 Specification by Traces
5.3.2.5 Specification by Temporal Logic

 Last Updated 01.Jan.2002