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

  FS - Formale Spezifikation

Contents  
  • 5.3.1 Overview
  • 5.3.1.1 Appraisal Criteria
  • 5.3.1.2 Individual Methods
  • 5.3.1.3 Comparison of the 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
  • 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:

    5.3.1.2 Individual Methods

    The individual methods of FS
    1. Mathematical Specification,
    2. Axiomatic Specification (Algebraic Specification),
    3. Algorithmic Specification,
    4. Specification by Traces and
    5. 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

    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

    Previous Next Last Updated 01.Jan.2002