zurück zur Startseite der Softwaretechnik-Trends , zu Band 15 Heft 2

Dissertationen


Dieter Nazareth: A Polymorphic Sort System for Axiomatic Specification Languages

Anschrift: Fakultät für Informatik, Lehrstuhl Prof. Dr. M. Broy, 80290 München

1. Gutachter: Univ-Prof. T. Nipkow, Ph.D.
2. Gutachter: Univ-Prof. Dr. M. Broy
Datum des Rigorosums: 18.05.1995

Zusammenfassung:

Die Dissertation stellt ein neuartiges polymorphes Sortensystem für axiomatische Spezifikationssprachen vor. Das Sortensystem selbst kann durch eine eigene Spezifikationssprache dynamisch spezifiziert werden. Dieser Ansatz ermöglicht ein flexibles Sortensystem, das dynamisch an unterschiedliche Anwendungsgebiete angepaßt werden kann. Insbesondere erlaubt dieses Sortensystem unterschiedliche Polymorphiekonzepte zu modellieren. Die Arbeit untersucht die syntaktische und semantische Behandlung von axiomatischen Spezifikationssprachen basierend auf einem derartigen Sortenkonzept.

Das Sortensystem basiert auf dem Konzept der eingeschränkten Sorten. Es erlaubt mit Hilfe von Sortenvariablen von konkreten Sorten zu abstrahieren und die Sortenvariablen dann durch Sortenprädikate einzuschränken. Die verwendete Spezifikationssprache gliedert sich in zwei Ebenen. Die Beschreibung der Funktionen auf der Termebene basiert auf einer klassischen Prädikatenlogik 1. Stufe. Sie erlaubt die Verwendung von polymorphen Bezeichnern und die Deklaration von unsortierten Variablen. Die Eigenschaften der Sortenprädikate werden mit Hilfe einer eigenen Spezifikationssprache basierend auf Horn-Klauseln beschrieben.

Um die Wohlsortiertheit von Spezifikationen zu überprüfen, wird ein Sorteninferenzkalkül angegeben. Dieser Kalkül berechnet darüberhinaus die Instantiierung von polymorphen Bezeichnern sowie die Sortierung von unsortiert deklarierten Variablen. Dabei kann es zu einer Spezifikation mehrere Herleitungen geben. Ein erster Modellbegriff wird deshalb unter Betrachtung aller möglichen Sortenherleitungen definiert. Anschließend werden die semantischen Beziehungen zwischen unterschiedlichen Sortenherleitungen einer Spezifikation untersucht. Es wird gezeigt, daß syntaktisch allgemeinere Herleitungen weniger Modelle besitzen. Dieses Ergebnis erlaubt uns einen äquivalenten Modellbegriff zu definieren der nur auf einer allgemeinsten Sortenherleitung einer Spezifikation basiert.

Abschließend wird die Implementierbarkeit des Sorteninferenzkalküls untersucht. Es wird ein Inferenzalgorithmus vorgestellt, der sich in zwei Abschnitte gliedert. Im ersten Abschnitt wird die Wohlgeformtheit der Spezifikation untersucht und es werden die dazu notwendigen Sortenprädikatbeschränkungen berechnet. Darüberhinaus wird eine allgemeinste Sortenherleitung für die Spezifikation berechnet. Im zweiten Abschnitt werden dann mit Hilfe eines Resolutionsverfahrens die berechneten Beschränkungen gegenüber der Sortenspezifikation als korrekt bewiesen. Es wird gezeigt, daß der Inferenzalgorithmus korrekt und vollständig ist gegenüber dem Sorteninferenzkalkül.

Der Sorteninferenzalgorithmus terminiert im allgemeinen nur für wohlsortierte Spezifikationen, da das Problem für allgemeine Sortenspezifikationen lediglich semientscheidbar ist. Modelliert man jedoch spezielle Polymorphiekonzepte, wie beispielsweise das Sortenklassenkonzept von Haskell, dann wird das Problem entscheidbar und der angegebene Sorteninferenzalgorithmus terminiert für alle Spezifikationen.


zurück zur Startseite der Softwaretechnik-Trends , zu Band 15 Heft 2