same information in English
Ansprechpartner:
Dr. Radu Grosu
Dr. Rudi Hettler
Dr. Dieter Nazareth
Dr. Franz Regensburger
Dipl.-Inform. Oscar Slotosch
Teilprojekt des BMFT-Verbundvorhabens KORSO, "Korrekte Software". Unter KORSO-Bremen finden sie einen weiteren KORSO-Partner.
Methodisches Programmieren verlangt ausdrucksfähige Sprachmittel. Die Sprache SPECTRUM ist zur Spezifikation und Entwicklung von Software- und Hardwaresystemen entworfen worden. Systeme werden mit SPECTRUM eigenschaftsorientiert beschrieben. Der zugrundeliegende logische Kalkül erlaubt es, die gängigen Beweisverpflichtungen deduktiv zu behandeln. Es ist ein Kalkül des natürlichen Schließens für dreiwertige Logik erster Stufe mit Induktionsprinzipien. Im Unterschied zu anderen algebraischen Methoden sind partielle Funktionen, auch nicht strikte, sowie Funktionen höherer Ordnung und nichtstetige Operationen zugelassen. SPECTRUM verwendet einen offenen prädikativen Polymorphismus mit Typklassen. Durch Typklassen können sowohl Überladung als auch viele Formen der Parameterisierung modelliert werden. Die Konzepte dienen insbesondere der Spezifikation funktionaler Systeme. SPECTRUM enthält als ausführbare Teilsprache eine funktionale Sprache. Die Semantik einer Spezifikation ist lose, gegeben durch die Klasse sämtlicher Modelle. Die Hinzunahme neuer Eigenschaften im Verlauf einer schrittweisen Verfeinerung, spiegelt sich daher in der Einengung dieser Modellklasse wider.
Die Sprache ist speziell auf die Modularisierung großer Projekte ausgelegt. Die Verknüpfungen von Spezifikationen geschieht durch Kombination in Verbindung mit Umbenennung und Hiding. Komplexe Spezifikationen lassen sich so hierarchisch strukturieren. Die Sprache ist mächtig genug, um die Implementierung von Spezifikationen durch primitivere Spezifikationen ausdrücken zu können. Mit den Mitteln logischer Deduktion können daher formale Beziehungen zwischen den Komponenten einer Projektdokumentation hergestellt werden. Ziel ist es, routinemäßige Komponenten automatisch zu generieren. Für die Arbeit am Rechner entsteht dazu eine Sammlung von Werkzeugen; für Deduktionsaufgaben ist der ISABELLE-Theorembeweiser verfügbar.
Englische Papiere zum SPECTRUM-Projekt sind hier.