 |
 |
 |
|
| 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- Mathematical Specification,
- Axiomatic Specification (Algebraic Specification),
- Algorithmic Specification,
- Specification by Traces and
- Specification by Temporal Logic
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 |
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 |