zurück zur Startseite der Softwaretechnik-Trends , zu Band 16 Heft 1

Dissertationen


Verfasser: Michael Mehlich, Institut für Informatik, Ludwig-Maximilians-Universität, München

Titel: Implementation of Combinator Specifications: Notions and Proving Techniques

Gutachter: Prof. Dr. M. Wirsing, Ludwig-Maximilians-Universität, München; Prof. Dr. F. Kröger

Datum der Prüfung: 13.12.1995

Zusammenfassung: Algebraische Spezifikationen haben sich seit ihrer Einführung als geeignetes Mittel zur abstrakten Beschreibung von Software--Systemen erwiesen.

Traditionell werden in diesen Spezifikationen ungeordnete Trägermengen (einfache Typen) und Funktionen erster Ordnung auf diesen beschrieben. In letzter Zeit gibt es aber einen Trend zu mächtigeren Konzepten, die den klassischen Ansatz nicht nur um geordneten Trägermengen und Funktionen höherer Ordnung erweitern, sondern auch um polymorphe Typen und Typklassen. Mit diesen Konzepten ist es möglich, sowohl Typen als auch getypte Kombinatoren bei der Beschreibung von Software--Systemen zu verwenden.

Um mit derartigen Spezifikationen korrekte Programme entwickeln zu können, ist es notwendig, die Spezifikationen mit einem Implementierungsbegriff zu unterlegen, und diesen mit einem Kalkül anzureichern, mit dem Implementierungsbeziehungen zwischen Spezifikationen formal sichergestellt werden können ohne auf semantischer, d.h. modelltheoretischer, Ebene argumentieren zu müssen.

In dieser Arbeit wird daher basierend auf logischen Relationen der zweiter Stufe ein Implementierungsbegriff eingeführt, der eine rein semantische Beziehung zwischen Spezifikationen (bzw. deren Modellen) beschreibt.

Ausgehend davon wird untersucht, wie die klassischen Implementierungsbegriffe Verfeinerung, Extend-Re-
name-Export- und Synthesize-Restrict-Identify-Implementierung an die mächtigeren Konzepte angepaßt werden können. Hierzu reicht es offensichtlich aus, deren Bestandteile Verfeinerung, persistente Erweiterung, Implementierung mit Restriktionen und Implementierung modulo Äquivalenzen zu betrachten.

Die einzelnen Bestandteile werden mit Beweisregeln unterlegt, die es in vielen Fällen ermöglichen, derartige Beziehungen zwischen Spezifikationen formal zu zeigen.


zurück zur Startseite der Softwaretechnik-Trends , zu Band 16 Heft 1