MENÜ MENÜ  

Formal Software Development using Generic Development Steps

Axel Dold

ISBN 978-3-89722-428-5
247 pages, year of publication: 2000
price: 40.50 €
Formal Software Development using Generic Development Steps
The methodology of the transformational approach to software engineering is to start from an abstract requirement specification of a given problem and to apply a series of correctness-preserving development steps to obtain an executable and efficient program. Each development step captures a design decision such as the choice of a specific algorithm or data structure representation.

This dissertation is concerned with a mechanized formal treatment of the transformational software development process in a unified framework. As a formal vehicle, the specification and verification system PVS is utilized to integrate development steps and development methods from different existing transformational approaches. Integration comprises the formalization (that is, a representation in the PVS specification language), the verification, and the correct application of the generic development steps. Transformations of different kind and complexity are integrated into this framework. They include well-known algorithmic paradigms and problem solving strategies such as global-search and divide-and-conquer, as well as transformations for the modification of functional specifications such as transformations from the Bird-Meertens Formalism like fusion or Horner's rule, transformation steps for optimizing recursive functions, transformations on the level of procedural programs, and implementations of data structures.

All software artifacts are represented generically within parameterized PVS theories which specify the semantic requirements on the parameters by means of assumptions and define the result of the transformation. Based on the semantic requirements, correctness of the generic step can be proved once and for all. Application of such a development step to a given problem is then carried out by providing a concrete instantiation for the parameters and verifying that it satisfies the theory requirements.

Some of the problem-solving strategies are organized by means of taxonomies (that is, hierarchies of specializations for specific problem classes and / or data structures). This approach greatly improves the applicability of the transformations and leads to an elegant structure of the algorithmic knowledge captured in the development steps.

As a basis for the realization of refinement hierarchies and for formal software development in PVS, a notion of refinement between parameterized PVS theories and a development methodology is presented which is based on correct partial instantiations of parameterized theories.

The usability of the approach is illustrated by many examples of different complexity. They include, among others, the derivation of several search and sorting algorithms, the derivation of a Prolog interpreter, the implementation of a symbol table used in compilers, and finally, as a larger non-trivial case-study: the construction of a compiler program from a given relational compiling specification specifying the translation of a Common Lisp-like language into a stack-based intermediate language.

Keywords:
  • formale Software-Entwicklung
  • transformationelle Software-Entwicklung
  • maschinelles Beweisen
  • generische Entwicklungsschritte
  • formale Verifikation

BUYING OPTIONS

40.50 €
in stock