FB 3 | ||||||
AG BKB > Forschung > Formale Methoden > | ||||||
Spezifikationssprache SPECTRAL |
||||||
Die Bremer Entwicklung der Spezifikationssprache SPECTRAL fußt einerseits auf ExtendedML [ST 91], anderseits auf langjährigen Erfahrungen beim Sprachentwurf (diverse Systemprogrammiersprachen, die Breitbandsprache CIP-L, Ada, PAnndA-S im ESPRIT Projekt PROSPECTRA) und wurde im Rahmen der ESPRIT WG COMPASS durchgeführt. Beim Entwurf von SPECTRAL wurde besonderer Wert darauf gelegt, mit möglichst wenigen, aber in ihrer Kombination mächtigen Konzepten sowohl Spezifikation im kleinen (einzelne Moduln, Abstrakte Datentypen) als auch Spezifikation im großen (Komposition von Moduln) zu behandeln. Durch die besondere Trennung der Strukturierung von Spezifikationen ("Klassen") und Programmen sowie die mächtigen Strukturierungsmöglichkeiten (Unterklassen mit Vererbung, abhängige Klassen, schrittweise Parametrisierung von Spezifikationen und Programmen durch höhere Funktionen) wird nicht nur eine neuartige Basis für die Entwicklung "im großen" gelegt, sondern vor allem die Wiederverwendung von Moduln, die in der Praxis außerordentlich wichtig ist, unterstützt. Die formale Spezifikation eines Moduls erlaubt die abstrakte Definition der Semantik des Moduls, ohne Details über die Realisierung als Programm preisgeben zu müssen. Durch die sogenannte lose Spezifikation wird nur die Spezifikation der notwendigen Anforderungen verlangt und Überspezifikation vermieden, die zur unerwünschten Einschränkung von effizienten Realisierungsmöglichkeiten führen kann. Eigentlich handelt es sich bei SPECTRAL um eine Sprachfamilie, da die einzelnen Moduln prinzipiell in verschiedenen Logiken formuliert sein können. Damit stellt sich das Problem der theoretischen Grundlagen für die heterogene Kombination. |
||||||
Autor: n/a |
||||||
AG BKB |
|