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.
|Versandkostenfrei innerhalb Deutschlands|
Wollen auch Sie Ihre Dissertation veröffentlichen?