KORSO Schlußbericht

1. Aufgabenstellung

Die Korrektheit von Software gewinnt immer stärkere Bedeutung im internationalen Wettbewerb, vor allem auch bei der Erschließung neuer Anwendungsgebiete. Die wirtschaftliche und gesellschaftliche Bedeutung der Korrektheit komplexer Systeme ergibt sich aus der Notwendigkeit der Qualitätssicherung, Fragen der Haftung, Wirtschaftlichkeit, Sicherheit (sowohl gegenüber unerlaubtem Zugriff als auch für "Leib und Leben") und Wiederverwendbarkeit.

Die Zielsetzung des BMFT Verbundprojekts KORSO bestand in der Vervollständigung der theoretischen Grundlagen und der Verbesserung der Entwicklungskonzepte und Methoden unter Einschluß von Werkzeugkonzeptionen für die Erstellung korrekter Software. Fernziel ist, eine konsequent auf Korrektheit ausgerichtete Software-entwicklung praktikabel und wirtschaftlich einsatzfähig zu machen und deren Tauglichkeit an Fallbeispielen zu demonstrieren.

Im Bremer Teilvorhaben sollten im Rahmen der Programmentwicklung durch Spezifikation und Transformation grundlegende Fragstellungen zur Strukturierung von Spezifikationen, zur Automatisierung und effizienten Realisierung von Transformationen, zur Formalisierung von Methoden sowie zur Wiederverwendbarkeit von Software-Moduln untersucht werden.

2. Voraussetzungen

An der Universität Bremen existierte bereits vor Projektbeginn eine Arbeitsgruppe, die im Rahmen des EG-Projekts PROSPECTRA (u.a. in Zusammenarbeit mit der AG Broy an der TU München) wesentliche Erfahrungen gesammelt hatte.

3. Planung und Ablauf

Durch Absprache mit der Projektleitung und den anderen Teilvorhaben kristallisierten sich im Laufe der Zeit konkrete Schwerpunkte der Arbeit heraus, ferner wurde in den Arbeitsgruppen und Querschnittsvorhaben Methodik und Fallstudien sowie maßgeblich an einem Konzept für Werkzeuge mitgearbeitet. Besonders die letzteren Tätigkeiten führten zu einer Erweiterung des ursprünglich geplanten Arbeitsumfangs; diese Erweiterung konnte aber durch zusätzlich von seiten der Universität Bremen zur Verfügung gestelltes Personal (aus der Grundausstattung der AG Krieg-Brückner) sowie Umschichtung der Tätigkeitsbereiche aufgefangen werden.

4. Wissenschaftlich-technischer Ausgangspunkt

4.1. Programm-Entwicklung durch Transfomation

Im Zentrum der Arbeiten steht die Methodik und Technik der "Programm-Entwicklung durch Spezifikation und Transformation". Aus einer formalen Anforderungsspezifikation wird ein ausführbares Programm schrittweise durch Verfeinerung und Detaillierung konstruiert und optimiert. In jedem Entwicklungsschritt wird eine Transformation angewandt, die die Korrektheit erhält; bei einigen Schritten muß noch die Anwendbarkeit bewiesen werden. Dies entspricht dem Arbeiten eines Ingenieurs, der ausgehend von einem mathematischen Modell (d.h. der Spezifikation) Formeln, etwa zum Lösen von Differentialgleichungen, verwendet, deren Korrektheit bewiesen wurde. Transformationen sollen systemunterstützt, interaktiv durch den Entwickler aufgrund seiner Zielvorgaben und Erfahrung, angewandt werden. Korrektheitserhaltende Transformationsregeln zerlegen den Programmentwicklungs- und Beweisprozess in einzelne beherrschbare Schritte und bieten die Möglichkeit der Mechanisierung und Systemunterstützung, ohne die Benutzersteuerung zu verlieren. Wesentliche Vorarbeiten wurden im Rahmen des CIP-Projekts an der TU München geleistet (vgl. [BW 82], [CIP 85, 87], [B+ 89]).

4.2. PROSPECTRA

Das zu diesem Themenkreis von der EG im Rahmen des ESPRIT Programms von März 1985 bis März 1990 geförderte Projekt PROSPECTRA hatte als Ergebnis einen in sich geschlossenen Ansatz ([Kri 89, 90], [HK 93]). Es zeichnet sich im internationalen Vergleich zu anderen Arbeiten durch die Vereinheitlichung von Programm- und Meta-Programm-Entwicklung sowie ersten Ansätzen zur Formalisierung des Programmentwicklungs-Prozesses aus (vgl. auch [Wile 86], [JHW 86], [Pep 87], [Smi 88, 91] ).

Für den praktischen Einsatz beim Entwickler ist es sehr wichtig, daß der Begriff der Transformation nicht nur die einzelne Transformationsregel, sondern auch umfassende Transformationsprogramme mit effizienten, automatisierten Anwendungstaktiken umfaßt. Eine große Herausforderung ist die Methodik der Abstraktion von konkreten Entwicklungen zu einer Klasse von Entwicklungen, zu einem schematischen Lösungsansatz; er kann dann auch zum "Nachspielen" der Entwicklung einer geringfügig abgeänderten ("ähnlichen") Spezifikation eingesetzt werden. Damit werden nicht nur Spezifikationen und Programme, sondern auch Entwicklungen wiederverwendbar. Ein besonderes Problem für die Abstraktion ist die positionelle Arbeitsweise: der Benutzer zeigt am Bildschirm auf die Anwendungsstelle für eine Transformation, die sich bei Nachspielen oder Verallgemeinerung verändern würde.

Diese grundlegenden Fragestellungen waren in PROSPECTRA (oder anderen Entwicklungen), wenn überhaupt, nur ansatzweise gelöst. Für keines der existierenden Systeme wurde die Korrektheit der Regeln und Taktiken formal bewiesen.

4.3. SPECTRAL

Ein anderer Ausgangspunkt für die Strukturierung von Spezifikationen sollte die gemeinsam mit Sannella entwickelte Spezifikationssprache a href="/home/inform/www/Forschung/Entwicklungsumgebungen.html#SPECTRAL">SPECTRAL sein (vgl. [KS 91]). Dieser Ansatz wurde allerdings im Rahmen des KORSO Projekts nicht weiter verfolgt, da hier andere Sprachen als sog. Referenzsprachen ausgewählt wurden. Stattdessen wurden Beispiele und Transformationen in Spectrum [Spec 93] formuliert.

4.4. Literatur

[B+ 89] Bauer, F.L., Möller, B., Partsch, H., Pepper, P.: Formal Program Construction by Stepwise Transformations - Computer-Aided Intuition-Guided Programming. IEEE Trans. on SW Eng. 15: 2 (1989) 165-180.

[BW 82] Bauer, F.L., Wössner, H.: Algorithmic Language and Program Development. Springer 1982.

[CIP 85] Bauer, F.L., Berghammer, R., Broy, M., Dosch, W., Gnatz, R., Geiselbrechtinger, F., Hangel, E., Hesse, W., Krieg-Brückner, B., Laut, A., Matzner, T.A., Möller, B., Nickl, F., Partsch, H., Pepper, P., Samelson, K., Wirsing, M., Wössner, H.: The Munich Project CIP, Vol. 1: The Wide Spectrum Language CIP-L. LNCS 183, 1985.

[CIP 87] Bauer, F.L., Ehler, H., Horsch, B., Möller, B., Partsch, H., Paukner, O., Pepper, P.,: The Munich Project CIP, Vol. 2: The Transformation System CIP-S. LNCS 292, 1987.

[HK 93] Hoffmann, B., Krieg-Brückner, B. (eds.): PROgram Development by Specification and Transformation, The PROSPECTRA Methodology, Language Family, and System. LNCS 680 (1993) 623p.

[JHW 86] Jähnichen, S., Hussain, F.A., Weber, M.: Program Development Using a Design Calculus. in: Rogers, M. W. (ed.): Results and Achievements, Proc. ESPRIT Conf. '86. North Holland (1987) 645-658.

[Kri 89] Krieg-Brückner, B.: Algebraic Specification and Functionals for Transformational Program and Meta-Program Development. In J. Diaz, F. Orejas (eds.): Proc. TAPSOFT 89, LNCS 352 (1989).

[Kri 90] Krieg-Brückner, B.: PROgram development by SPECification and TRAnsformation. in: Kahn, G. (ed.): Proc. Summer School on Programming Environments in ESPRIT (Sophia Antipolis). also in: Baader (ed.): Werkzeuge der Software-Verifikation (1990).revised version in: Technique et Science Informatiques Special Issue on Advanced Software Engineering in ESPRIT (1990) 134-149 (invited paper).

[KS 91] Krieg-Brückner, B., Sannella, D.: Structuring Specifications in-the-Large and in-the-Small: Higher-Order Functions, Dependent Types and Inheritance in SPECTRAL. Proc. TAPSOFT '91, LNCS 494 (1991) 313-336.

[Pep 87] Pepper, P.: A Simple Calculus for Program Transformation (Inclusive of Induction) Science of Computer Programming 9 (1987) 221-262.

[Smi 88] Smith, D. R.: KIDS: a Knowledge-Based Software Development Environment. Proc. Workshop on Automating Software Design (St. Paul, Minn.) (1988) 129-136.

[Smi 91] D. R. Smith: KIDS - a Knowledge-based Software Development System. In: M.M. Lowry, R. D. McCartney (eds.): Automating Software Design. AAAI Press / MIT-Press (1991) 483 - 514.

[Spec 93] The Munich Spectrum Group: Broy, M., Facchi, C., Grosu, R., Hetler, R., Hussmann, H., Nazareth, D., Regensburger, F., Stoelen, K.: The Requirement and Design Specification Language SPECTRUM: An Informal Introduction. Institut für Informatik, Technical University Munich, Internal Report 1993.

[Wile 86] Wile, D. S.: Program Developments: Formal Explanations of Implementations. CACM 26: 11 (1983) 902-911. also in [Agresti 86] 239-248.

5. Zusammenarbeit mit anderen Stellen

5.1. COMPASS

Die Arbeitsgruppe COMPASS (COMPrehensive Algebraic approach to System Specification and development) wird von B. Krieg-Brückner koordiniert und von der EG im Rahmen des ESPRIT Basic Research Programms unterstützt. Hier sind 20 Universitäten mit führenden Vertretern auf dem Gebiet der Spezifikation in Europa versammelt (darunter mehrere Mitglieder anderer Teilvorhaben von KORSO), um mit ihren Arbeitsgruppen die verschiedenen theoretischen Ergebnisse zu konsolidieren und zu integrieren, und sie auf die Praxis der Software-Entwicklung zu übertragen. COMPASS wurde als Forum für die Diskussion und den Austausch von Ideen genutzt.

5.2. Andere Teilvorhaben

Innerhalb des KORSO Projekts wurde mit anderen Teilvorhaben vor allem an dem Beweis der Korrektheit von Transformationen (GMD FIRST, Berlin), am Fallbeispiel (TU Berlin und andere), zu Themen der Wiederverwendung (Uni Karlsruhe/Menzel) und besonders an der gemeinsamen KORSO Systemkonzeption (Uni Karlsruhe/Menzel, LMU München, TU Berlin, Uni Oldenburg, Uni Ulm, FZI Karlsruhe u.a.) zusammengearbeitet. Das in Bremen entwickelte daVinci-System zur Visualisierung von Termen, insbesondere der Entwicklungsbibliothek, wurde u.a. an der Uni Karlsruhe/Menzel sowie der GMD FIRST (Berlin) eingesetzt.

6. Ergebnisse

6.1. Zusammenfassung der Ergebnisse

Schwerpunkte des KORSO-Teilvorhabens an der Universität Bremen (vgl. [BJ 94], [KLSW 94]) im Rahmen der Methodik der Programmentwicklung durch Spezifikation und Transformation waren: die Untersuchung der Strukturierung von Spezifikationen, Entwicklungen und Beweisen; die Entwicklung eines einheitlichen semantischen Rahmens für Transformation und Verifikation bzw. einer Meta-Sprache für die Transformation und die Formalisierung von Entwicklungsmethoden; die Entwicklung von Techniken zur Wiederverwendbarkeit von Spezifikationen und Entwicklungen; die Unterstützung des Entwicklungsprozesses durch Visualisierung der methodischen Relationen in der Entwicklungsbibliothek.

Daneben wurde maßgeblich an der Konzeption einer KORSO-Systemarchitektur (mit anderen) gearbeitet [KM+ 4] sowie Beiträge zum Methodikrahmen ([W+ 92], [PW 94]) und den Fallbeispielen ([Shi 94a], [KWL 94]) geleistet.

6.2. Transfer der Ergebnisse aus PROSPECTRA

Nach Beendigung des ESPRIT Projekts PROSPECTRA konnten einige hochqualifizierte Mitglieder von ehemaligen Partner-Organisationen für kurz- und längerfristige Aufenthalte an der Universität Bremen gewonnen werden (Dr. Owen Traynor, Einar Karlsen). Diese Zusammenarbeit hat sich als sehr effektiv erwiesen.

Der Transfer der Ergebnisse aus dem Vorprojekt PROSPECTRA war von besonderer Bedeutung, da ein Systemprototyp vorhanden war, mit dem Spezifikationen und Transformationen experimentell entwickelt und generelle praktische Erfahrungen gesammelt werden konnten. Die Darstellung der Ergebnisse im Sinne einer Gesamtschau (siehe [HK 93], [Kri 93], [LLT 93]) und die Überarbeitung einzelner Teile (wie z.B. des Katalogs von implementierten Transformationen [LK 93]) erbrachte wesentliche Erkenntnisse für das hier beschriebene Vorhaben. So wurden die Vorteile der Vereinheitlichung von Entwicklung und Meta-Entwicklung (von Transformationsprogrammen) in einem gemeinsamen Rahmen für Methodik und System herausgearbeitet (vgl. [KKLT 91, 93], [KKT 92]).

Die Erfahrungen mit der Anwendung des Transformations-Paradigmas auf die Beweistechnik im Rahmen des PROSPECTRA Beweis- und Taktik-Editors (vgl. [TLK 92], [MTD 93], [Tra 93]) waren die Basis für die spätere vereinheitlichte Sicht von Beweis und Transformation als zwei Instanzen des allgemeinen Begriffs der transformationellen Entwicklung und der Behandlung von Entwicklungsskripten (mit Taktiken) als Objekten. Das in diesem Zusammenhang auftretende "lifting" von Gleichungen bzw. terminierenden Termersetzungssystemen aus der Objektsprache zu Transformationen in der Meta-Sprache, das diskret programmiert werden mußte und z.T. sehr aufwendig war, konnte später als Beispiel in der Transformations-Meta-Sprache formuliert werden (s.u. bzw. [KLSW 94]).

6.3. Korrekte, objektsprachen-unabhängige Transformationsregeln

Aufbauend auf den Erfahrungen des Projekts PROSPECTRA wurde nun ein einheitlicher semantischer Rahmen für Transformation und Verifikation entwickelt, der nicht nur den Beweis der Korrektheit einer Transformationsregel (analog zu einer Beweisregel) auf der Meta-Ebene erlauben soll, sondern auch eine Strukturierung durch Abstraktion von der unterliegenden speziellen Semantik/Logik der Objektsprache [Liu 93] [Liu 94]; Ziel ist, daß so nicht der gesamte Satz von Transformationsregeln für jede Objektsprache neu entwickelt und bewiesen werden muß, sondern nur die korrekte Instanziierung bzgl. einer speziellen Objektsprache. Diese mehr deduktiv orientierte, strukturierte Semantik und Beweistechnik wurde teilweise in generischen Beweisystemen ("logical frameworks") wie Isabelle bzw. LEGO realisiert und zum Beweis von komplexeren Transformationsregeln benutzt ([Wolff 94a], [Liu 95]), u.a. angeregt durch ihre Verwendung im KORSO-Fallbeispiel LEX [KWL 94]. Die Arbeiten zur Unifikation höherer Ordnung ([NQ 91, 92], [Qian 91, 93, 94], [QW 92, 94], [Wang 94] sind ein Beispiel für die Strukturierung ausführbarer Spezifikationen im Sinne der Logik-Unabhängigkeit; gleichzeitig dienten sie als Basis für die Arbeiten zum Matching höherer Ordnung (s.u.).

6.4. Formalisierung transformationeller Entwicklungen, Wiederverwendbarkeit von Entwicklungsprozessen

Im Vordergrund steht die Formalisierbarkeit von transformationellen Entwicklungen: Nur ein sehr leistungsfähiger Transformationsbegriff ermöglicht es, durch Abstraktion von der Transformations-Anwendungsstelle die Wiederverwendbarkeit von Entwicklungen mit dem Ziel des späteren "Nachspielens" für ähnliche Fälle und der Verallgemeinerung zu einer Entwicklungs-Methode zu unterstützen. Damit werden auch Entwicklungsprozesse wiederverwendbar. Die unten geschilderten Ergebnisse finden Eingang in einem Kapitel [BK 95] der Sammlung von Übersichtsbeiträgen [AKK 95].

Es wurde eine Transformations-(Meta-)Sprache mit einem vereinheitlichten Transformationsbegriff entwickelt, der verallgemeinerte strukturelle Anwendung ("higher-order pattern matching") zur Abstraktion, automatische Überprüfung kontext-sensitiver Vorbedingungen zur Steigerung der Effizienz sowie (higher-order-) Taktiken der Anwendung und Strategien der Auswahl bei mehrfacher Anwendbarkeit zur Definition von Methoden erlaubt ([KLWS 93], [KLSW 94], [WS 94]).

choose : Bool -> (a, a) -> a
choose true (X, Y) = X, choose false (X, Y) = Y

MORGAN ==
not (choose C (and,or) (X, Y)) =>
(choose C (or,and)) (not X, not Y)

Abbildung 1: Definition und Anwendung eines Matching-Kombinators

for all X: T . L = R =>
( L | (X, V) => R | (X, V) such that TypeOf V = T )

for all a:Bool . not (not a) = a -- wird transformiert zu
not (not V) => V such that TypeOf V = Bool

Abbildung 2: (higher-order) Transformationsregel ("lifting")und Anwendung

Abstraktion von der Transformations-Anwendungsstelle wird einerseits durch (im Kalkül definierbare) Fokussier-Transformationen in einem Anwendungskontext, andererseits durch sog. Matching-Kombinatoren erreicht. Sie sind mit primitiv rekursiven (higher-order) Gleichungen definierbar, erlauben so die Definition komplexer (Programm-) Schemata und tragen wesentlich zur verallgemeinerten, kompakten und besser lesbaren Definition von Transformationsregeln bei (vgl. [SW 93, 94], [Shi 94b]). Abb. 1 zeigt ein Beispiel für eine kompakte Kombination mehrerer ähnlich strukturierter Regeln: Der Kombinator choose erlaubt die Auswahl; der Parameter C kann lokal durch den Matching-Algorithmus, durch eine Anwendungs-Strategie oder durch Benutzungsinteraktion festgelegt werden. Der Substitutions-Kombinator | in Abb. 2 ist ein Beispiel für Abstraktion und bessere Lesbarkeit.

Eine Transformationsregel ist eine Relation; Definitionen werden durch den Pfeil => gebildet, der geschachtelt sein kann. Damit werden Regeln höherer Ordnung möglich; Abb. 2 zeigt ein solches Beispiel: eine (higher-order) Transformationsregel, die wieder eine Transformationsregel als Ergebnis hat: eine Gleichung kann zu einer Transformationsregel angehoben werden ("lifting"), in der die Typüberprüfung durch eine Kontextbedingung ausgedrückt ist. Taktiken (höherer Ordnung) können durch taktische Kombinatoren beschrieben werden. Es zeigt sich, daß einige wenige geeignet vordefinierte Kombinatoren (wie Rekursion, Komposition, Vereinigung u und sequentielle Auswahl R else S "wenn R anwendbar, dann R sonst S") ausreichen, um die üblichen Anwendungstaktiken beschreiben zu können [KLSW 94], [WS 94]. Zusammengefaßt ergibt sich eine Sprache, in der transformationelle Entwicklungsprozesse formal dargestellt werden können.

6.5. Meta-Entwicklung, effiziente Transformationsprogramme

Erfahrungen mit einem recht umfangreichen Satz von Transformationen zeigen, daß die Effizienz beim interaktiven Einsatz entscheidend ist [LK 93], [KWL 94]. Einerseits sollen Kontextbedingungen effizient durch inkrementelle Berechnung von Attributen in Regeln und taktischen Termen überprüft werden ([Mey 94], [Wolff 94b]), andererseits sind Transformationsregeln und geeignete Anwendungs-Taktiken, analog zu Spezifikationen, Ausgangspunkt für die korrekte Entwicklung von effizienten Transformations-Programmen in dem Transformations-Kalkül selbst. Abb. 3 zeigt eine Transformationstaktik für die Erlangung der Disjunktiven Normalform und eine effiziente Version: aus einer allgemeine Normalisierungs-Strategie ("wende eine der Regeln irgendwo an, solange möglich") wird "wende in einem Durchgang über den Term "von unten nach oben" ("leftmost-innermost") an allen möglichen Stellen eine der Regeln, die paßt, an, solange möglich". Bei der Entwicklung werden geeignete algebraische Eigenschaften der taktischen Kombinatoren und auch hier wieder Transformationen, auf einer Meta-Ebene, eingesetzt.

( ABSORB u MORGAN u DISTRIB )~^
= (Fli ( ABSORB else MORGAN else DISTRIB )) ^

Abbildung 3: allgemeine Normalisierungs-Strategie und effiziente Taktik

In [Sei 93] wurde u.a. die automatische Analyse von Terminationseigenschaften und die Berechnung von Komplexitätsmaßen zur Steuerung von zielgerichteten, optimierenden Transformationstaktiken zur Erreichung von Effizienz untersucht und implementiert.

Abbildung 4: Der KORSO Systemarchitektur-Rahmen

6.6. KORSO Systemarchitektur

In [KM+ 94] wurde eine KORSO-Systemarchitektur konzipiert, die die besonderen Belange des Einsatzes formaler Methoden berücksichtigt. Besonderer Wert wird auf die globale Erhaltung der Korrektheit des Vorgehens (correctness management) sowie die Erweiterbarkeit des Systems gelegt.

Die Entwicklungsgeschichte nimmt bei der Konzeption eines Systemarchitektur-Rahmens eine zentrale Rolle ein [KM+ 94], vgl. Abb. 4. Sie soll auch technisch als Basis für die die Wiederverwendbarkeit von Teil-Entwicklungen sowie die Definition von geeigneten Protokollen für den Datenaustausch und die Integration von (fest oder lose gekoppelten) Systemkomponenten bzw. "externen" Subsystemen dienen. Erste Untersuchungen zur Realisierung einer solchen Systemarchitektur wurden durchgeführt und als Prototyp implementiert [KW 94], [Karl 94a, b]. Dabei zeigt sich, daß eine funktionale Sprache mit Persistenz zur Realisierung von Subsystem-Interaktion, Integration und Verwaltung der Datenbasis besonders gut geeignet ist.

6.7. Grafische Darstellung der Datenbasis

Der Entwicklungsprozeß soll durch geeignete grafische Darstellung der Einheiten (z.B. Spezifikationen, Programme, Beweise, Transformationen) in der Entwicklungs-Datenbasis unterstützt werden, um sich auf das wesentliche konzentrieren zu können und die Übersicht nicht zu verlieren. Dabei spielen die methodischen Relationen (z. B. Verfeinerung, Modifikation, strukturelle Abhängigkeit, Konfiguration) in einem Entwicklungsgraphen eine wesentliche Rolle. Mit einer Visualisierung der Datenbasis wird es überhaupt erst möglich, sich auch bei sehr großen Programmentwicklungen im System zurechtzufinden. So können Strukturen besser und schneller erkannt werden, wodurch beispielsweise der Vorgang der Wiederverwendung erheblich unterstützt werden kann. Abb. 5 zeigt die Visualisierung eines Entwicklungsgraphen für das Fallbeispiel [KWL 94] (in einem frühen Stadium) mit dem in Bremen entwickelten Visualisierungssystem daVinci, z.B. die Anwendung der Transformationsregel SplitOfPostcondition mit assoziierter (generierter) Anwendungsbedingung ScanSplit.

Abbildung 5: Entwicklungsgraph, visualisert mit daVinci

Mit daVinci [FW 93, 94a, b, c] ist die interaktive Bearbeitung komplexer Graph-Strukturen möglich. Derzeit ist daVinci in der Lage, zyklische oder azyklische gerichtete Graphen automatisch in hoher Qualität zu visualisieren. Dabei werden verschiedene ästhetische Kriterien wie z.B. die Minimierung von Kantenkreuzungen berücksichtigt. Mit Hilfe von Knoten- und Kanten-Attributen kann Einfluß auf die Art der Visualisierung genommen werden (z.B. durch Einsatz von Farben, geometrischen Objekten, Füllmustern, unterschiedlichen Schriftsätzen usw.). Die errechnete Visualisierung kann nachträglich vom Benutzer interaktiv verfeinert werden. Durch jederzeit verfügbare Skalierungsfunktionen kann die Darstellung stufenlos verkleinert bzw. die momentan verwendete Zeichensatzgröße eingestellt werden. Interaktive Abstraktionsoperationen bieten u.a. die Möglichkeit, Teilgraphen zur Steigerung der Übersichtlichkeit zeitweise auszublenden. Künftig werden auch verschiedenartige kontextsensitive grafische Darstellungen (z.B. Teilgraphen als geschachtelte "Boxen"), die über Beschreibungsdefinitionen generiert werden, gleichzeitig in verschiedenen Sichten möglich sein. daVinci kann an vorhandene Applikationen (z.B. Transformations- oder Beweissysteme) angeschlossen werden und bietet dem Benutzer die Möglichkeit, diese Systeme auf Basis der Visualisierung bedienen zu können (als graph-orientierte Benutzungsoberfläche, vgl. User Interaction Manager in Abb. 4). Über die Applikationsschnittstelle kann ein angebundenes Programm Objekte zur Visualisierung versenden, Menüs in daVinci hinzufügen oder Benutzerdialoge durchführen. daVinci informiert eine Applikation dabei über Selektions- und Eingabe-Ereignisse. Im Rahmen des KORSO Projektes wurde daVinci beispielsweise in das Beweissystem KIV der Arbeitsgruppe Uni Karlsruhe (Menzel) sowie das Synthesesystem IOSS der GMD FIRST (Berlin) integriert: mithilfe von daVinci werden Programmbeweise in Entwicklungsgraphen auf anschauliche Weise dargestellt.

7. Nutzen und Verwertbarkeit

Zusammengefaßt läßt sich sagen, daß die ursprünglichen Ziele voll erreicht wurden: die Weiterentwicklung des Ansatzes der Programmentwicklung durch Spezifikation und Transformation durch Beantwortung einiger grundlegender Fragstellungen. Einige Aspekte, die für die Praxis der Entwicklung korrekter Software besonders wesentlich sind, sollen im folgenden noch einmal herausgegriffen werden.

Der allgemeine Ansatz zum strukturierten Beweis der Korrektheit von Transformationsregeln und Taktiken im System selbst bewirkt, daß die Erweiterbarkeit des Systems (durch neue Transformationsregeln, neue Taktiken und Methoden, neue Logiken) ebenso sicher ablaufen kann (auf der Meta-Ebene) wie die Softwareentwicklung (auf der Objekt-Ebene) und ebenso durch ein Entwicklungssystem unterstützt wird (z.B. die Darstellung und Überwachung der komplizierten Abhängigkeiten und Entwicklungen in einem Projektgraphen); die Meta-Entwicklung wird sogar wieder durch Transformationen formalisiert. Allgemeine Taktiken können im System selbst optimiert und zu effizienten Transformationsprogrammen entwickelt werden. Somit rückt die vollständig formale Entwicklung der Unterstützungswerkzeuge selbst in greifbare Nähe, ein Wunsch, wenn nicht eine Forderung, bei der Abnahme sicherheitsrelevanter Software. Derzeit ist kein Transformationssystem bekannt, dessen Regeln und Taktiken formal bewiesen wären; ebenso sind die in Beweissystemen verwendeten Taktiken oft nicht als korrekt bewiesen, so daß alle elementaren Beweisschritte explizit nachvollzogen werden müssen. Hier ist ein drastischer Effizienzgewinn möglich.

Der entwickelte Transformationskalkül erlaubt die Abstraktion von einer konkreten Entwicklung zu einem schematischen Lösungsansatz; "Nachspielen" und Verallgemeinerung zu einer Methode werden möglich, effiziente Taktiken können formal bewiesen werden. Es konnte insbesondere das Problem der Abstraktion von der positionellen Arbeitsweise gelöst werden: die verallgemeinerte strukturelle Anwendung (extended "higher-order" pattern matching) mit sog. Matching-Kombinatoren führt nicht nur zu verallgemeinerten, kompakten Transformationsregeln sondern auch zu Taktiken, in denen von der konkreten Anwendungsstelle durch Angabe von allgemeinen Mustern mit spezifischen Nebenbedingungen abstrahiert werden kann. Der implementierte Matching-Algorithmus ist effizient genug, um in taktischen Theorembeweisern oder für eine neue Art von ausführbaren Spezifikationen (eine Art funktionaler Programme mit der zusätzlichen Verwendung von Matching-Kombinatoren in der linken Seite von Definitionsgleichungen) verwendet zu werden. Somit werden nicht nur Spezifikationen und Programme, sondern auch Entwicklungen wiederverwendbar; der Nutzen ist evident, da so z.B. nicht nur ein Programmodul, sondern auch seine Entstehungsgeschichte für die Wiederverwendung zugänglich wird. Es ist zu erwarten, daß es sich mittelfristig lohnen wird, nicht nur Spezifikations- oder Programmoduln nach der Erstentwicklung zu generalisieren, um sie später besser durch Spezialisierung besser wiederverwenden zu können, sondern auch in die Verallgemeinerung von Erstentwicklungen selber zu investieren, um sie später in ähnlicher Situation nachvollziehen zu können.

(Formale) Methoden können zwar auch auf dem Papier angewandt werden; in der Regel steht und fällt aber ihr Erfolg mit den zur Verfügung stehenden Werkzeugen und dem Grad der automatischen Unterstützung bei der Software-Entwicklung. Die Entwicklung eines Transformationssystems war in diesem Vorhaben nicht geplant. Es wurden aber erste Schritte auf die Entwicklung eines ersten Prototyps hin durchgeführt, der mit dem generischen Beweissystem (logical framework) Isabelle realisert ist und sowohl den Beweis der Korrektheit als auch die prototypische Anwendung einer Regel oder Taktik erlaubt (einschließlich der Verwendung von Matching-Kombinatoren und der Erzeugung von kontext-sensitiven Anwendungsbedingungen). Eine Vereinbarung zur Entwicklung eines solchen Transformationssystems mit einem interessierten Industriepartner steht kurz vor dem Abschluß. Mehr noch, die entwickelte generelle KORSO Systemarchitektur soll als "Blaupause" für die gemeinsame Entwicklung einer Universellen Entwicklungsumgebung für Formale Methoden dienen, unter Einhaltung der Vorgaben des Vorgehensmodells für die Planung und Durchführung von IT-Vorhaben des Bundesministers des Innern. Ein Industriepartner aus einem Anwendungsbereich für sicherheitskritische Software ist beteiligt; mit anderen wird verhandelt.

Das Graph-Visualisierungssystem daVinci, ursprünglich nur für die Darstellung der semantischen Relationen in einem Entwicklungsgraphen konzipiert, kann als generelle Schnittstelle für die Benutzungsinteraktion verwendet werden. Es wird weltweit in mehreren Hundert Installationen für die verschiedensten Anwendungen eingesetzt.

8. Fortschritt bei anderen Stellen

Der Fortschritt bei den anderen Teilvorhaben im Rahmen des KORSO-Projekts kann als bekannt vorausgesetzt werden. Besonders interessant ist hier der transformationelle Ansatz zur Entwicklung reaktiver Systeme (Uni Oldenburg); hier soll in Zukunft, als konkrete Anwendung, enger kooperiert werden.

Im engeren Bereich der Entwicklung durch Transformation gibt es, über die Weiterentwicklung bestehender Ansätze hinaus, keine wesentlichen neuen Erkenntnisse. Ähnlich ist es bei dem Bereich der Formalisierung von Entwicklungen. Abgesehen von den Projektpartnern Uni Ulm und GMD FIRST (Berlin), mit denen kooperiert wurde und wird, konnte in jüngster Zeit eine Brücke zu dem Bereich der Programmsynthese mithilfe von logical frameworks geschlagen werden (vgl. [BK 95]).

9. Veröffentlichungen

[AKK 95] Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B.(eds.): Algebraic Foundations of System Specification. Chapman Hall (in preparation).

[BJ 94] Broy, M., Jähnichen, S. (Hrsg.): Korrekte Software durch formale Methoden, Abschlußbericht des BMFT-Verbundprojekts "KORSO". GMD FIRST, Berlin, 1994.

[BJ 95] Broy, M., Jähnichen, S. (eds.): KORSO, Correct Software by Formal Methods, LNCS

[BK 95] Basin, D., Krieg-Brückner, B.: Formalization of the development process. In: [AKK 95], Chapter 13.

[FW 93] Fröhlich, M., Werner, M.: Das interaktive Graph-Visualisierungssystem daVinci V1.2. FB3 Informatik, Universität Bremen, 1993. auch in [Kri 94a].

[FW 94a] Fröhlich, M., Werner, M.: Perspektiven der Graph-Visualisierung: daVinci V1.3 und zukünftige Entwicklungen. KORSO Bericht, in [Kri 94a].

[FW 94b] Fröhlich, M., Werner, M.: The interactive Graph-Visualization System daVinci - A User Interface for Applications. Informatik Bericht Nr. 5/94, Universität Bremen, 1994. (submitted to: Journal of Visual Languages and Computing - Special Issue on Graph Visualization).

[FW 94c] Fröhlich, M., Werner, M.: Demonstration of the interactive Graph-Visualization System daVinci. Inforin: R. Tamassia, I. G. Tollis (eds.): Proc. DIMACS Workshop on Graph Drawing '94, LNCS.(to appear).

[Ger 92] Gersdorf, B.: Entwurf, formale Definition und Implementierung der funktional-logischen Programmiersprache ET. Dissertation, Universität Bremen, 1992.

[HK 93] Hoffmann, B., Krieg-Brückner, B. (eds.): PROgram Development by Specification and Transformation, The PROSPECTRA Methodology, Language Family, and System. LNCS 680 (1993) 623p.

[Karl 94a] Karlsen, W.: Tool Integration in a Persistent Functional Setting. KORSO Bericht, in [Kri 94a].

[Karl 94b] Karlsen, W.: A Framework for Control Integration in a Functional Setting. KORSO Bericht, in [Kri 94b].

[KKLT 91] Krieg-Brückner, B., Karlsen, E.W., Liu, J., Traynor, O.: The PROSPECTRA Methodology and System: Uniform Transformational (Meta-) Development. in: Prehn, S., Toetenel, W. J. (eds.): VDM'91, Formal Software Development Methods; Vol. 2: Tutorials. LNCS 552 (1991) 363-397.

[KKLT 93] Krieg-Brückner, B., Karlsen, E.W., Liu, J., Traynor, O.: Uniform Transformational Development. in: [HK 93] pp. 317-330.

[KKT 92] Karlsen, E.W., Krieg-Brückner, B., Traynor, O.: The PROSPECTRA System: A Unified Development Framework. In: M.Nivat, C. Rattray, T. Rus, G. Scollo (ed.): Algebraic Methodology and Software Technology (AMAST'91), Workshop in Computing Springer-Verlag, London (1992) 421 - 433.

[KLSW 94] Krieg-Brückner, B., Liu, J., Shi, H., Wolff, B.: Towards Correct, Efficient and Reusable Transformational Developments. in [BJ 95], erweitert in [Kri 94a].

[KLWS 93] Krieg-Brückner, B., Liu, J., Wolff, B., Shi, H.: Towards Correctness, Efficiency and Reusability of Transformational Developments. in: H. Reichel (ed.): Informatik - Wirtschaft - Gesellschaft, 23. GI Jahrestagung 1993, Dresden, Fachgespräch "Spezifikation und Semantik", Reihe Informatik Aktuell, Springer Verlag (1993) 241-252 (Extended Abstract).

[KM+ 94] Krieg-Brückner, B., Menzel, W. (eds.), Reif, W., Ruess, H., Santen, Th., Schwier, D., Schellhorn, G., Stenzel, K., Stephan, W.: System Architecture Framework for KORSO. in [Kri 94a].

[Kri 93] Krieg-Brückner, B.: Introduction [to PROgram development by SPECification and TRAnsformation] in: [HK 93] pp. 3-34.

[Kri 94a] Krieg-Brückner, B. (Hrsg.): Programmentwicklung durch Spezifikation und Transformation - Bremer Beiträge zum Verbundprojekt KORSO (Korrekte Software). Informatik Bericht Nr. 1/94, Universität Bremen, 1994.

[Kri 94b] Krieg-Brückner, B. (Hrsg.): Programmentwicklung durch Spezifikation und Transformation - Bremer Beiträge zum Verbundprojekt KORSO (Korrekte Software); Band 2. Informatik Bericht Nr. 10/94, Universität Bremen, 1994.

[KS 91] Krieg-Brückner, B., Sannella, D.: Structuring Specifications in-the-Large and in-the-Small: Higher-Order Functions, Dependent Types and Inheritance in SPECTRAL. Proc. TAPSOFT '91, LNCS 494 (1991) 313-336.

[KW 94] Karlsen, W., Wu, Y.: Incorporating Persistence in a Strictly Evaluated Purely Functional Language. KORSO Bericht, in [Kri 94a].

[KWL 94] Kolyang, Wolff, B., Liu, J.: Transformational Development of the LEX Example. KORSO Bericht, in [Kri 94b].

[Liu 93] Liu, J.: A Semantic Basis for Logic-Independent Transformations. In F. Orejas (eds.): Proc. 9th WADT-COMPASS Workshop, LNCS 785 (1994) 268-279. auch in [Kri 94a].

[Liu 94] Liu, J.: Higher-Order Structured Presentations in a Logical Framework. Dissertation, Universität Bremen, 1994.

[Liu 95] Liu, J.: Formal Correctness Proof of a Transformation Rule in LEGO: Split of Postcondition, Universität Bremen (in preparation).

[LK 93] Liu, J., Krieg-Brückner, B.: Transformation. in: [HK 93] pp. 99-127.

[LLT 93] Liu, J., Traynor, O., Lynenskjøld, S.: Guided Tour of the PROSPECTRA System. in: [HK 93] pp. 331-366.

[Mey 94] Meyer, Th.: Generierung inkrementeller Evaluatoren für modulare und parametrisierte Attributierungen. Diplomarbeit, Universität Bremen, 1994 (erscheint als Informatik Bericht).

[MTD 93] McGettrick, A., Traynor, O., Duffy, D.: Verification. in: [HK 93] pp. 129-144.

[NQ 91] Nipkow, T., Qian, Z.: Modular Higher-Order E-Unification, Proc. 4th Int. Conf. Rewriting Techniques and Applications, 1991, LNCS 488, 200-214.

[NQ 92] Nipkow, T., Qian, Z.: Reduction and Unification in Lambda Calculi with Subtypes, Proc. 11th Int. Conf. Automated Deduction, 1992, LNCS 607, 66-78. also: J. Automated Reasoning, to appear.

[PW 94] Pepper, P., Wirsing, M.: A Methodology for the Development of Correct Software. in [BJ 95].

[Qian 91] Qian, Z.: Unification in Combinations of Second Order Types and Linear Shallow Algebraic Theories, Proc. 2nd International Workshop on Conditional and Typed Rewriting Systems, LNCS 516, 1991, 448-453.

[Qian 93] Qian, Z.: Linear Unification of Higher-Order Patterns, Proc. TAPSOFT'93,391-405, 1993, LNCS 668. also in: J. Logic and Computation, to appear.

[Qian 94] Qian, Z.: Higher-Order Equational Logic Programming, Proc. 21st ACM Symp. Principles of Programming Languages, ACM Press, 1994.

[QW 92] Qian, Z., Wang, K: Higher-Order E-Unification for Arbitrary Theories, Proc. Joint Int'l Conf. and Symp. on Logic Programming, 1992, MIT Press, 52-66.

[QW 94] Qian, Z., Wang, K: Modular AC Unification of Higher-Order Patterns, Proc. Int. Conf. on Constraints in Computational Logics, LNCS 845, 1994.

[Sei 93] Seifert, R.: Property Analysis of Term Rewriting Systems. Dissertation, Universität Bremen, 1993.

[Shi 94a] Shi, H.: Benutzer-Schnittstelle und -Interaktion für die HK-Untersuchung. KORSO Bericht, in [Kri 94a].

[Shi 94b] Shi, H.: Extended Matching and Application to Program Transformation. Dissertation, Universität Bremen, 1994.

[Spec 93] The Munich Spectrum Group: Broy, M., Facchi, C., Grosu, R., Hetler, R., Hussmann, H., Nazareth, D., Regensburger, F., Stoelen, K.: The Requirement and Design Specification Language SPECTRUM: An Informal Introduction. Institut für Informatik, Technical University Munich, Internal Report 1993.

[SW 93] Shi, H., Wolff, B.: Second-Order Matching with Matching Combinators. KORSO Bericht, FB3 Informatik, Universität Bremen, 1993.

[SW 94] Shi, H., Wolff, B.: A Finitary Matching Algorithm for Constructor Based Theories. KORSO Bericht, in [Kri 94a].

[TL 91] Traynor, O., Liu, J.: The Development of Correct Programs by Specification and Transformation. in Proc. ICYCS Conf., Beijing (1991).

[TLK 92] Traynor, O., Liu, J., Krieg-Brückner, B.: Knowledge-Based Transformational Programming. In Proc. of 4th International Conf. on Software Engineering and Knowledge Engineering, Capri, Italy, (1992).

[Tra 93] Traynor, O.: Proof Subsystem. in: [HK 93] pp. 495-521.

[W+ 92] Wirsing, M., et al.: A Framework for Software Development in KORSO. Ludwig-Maximilians-Universität München, Institut für Informatik, Bericht 9205, 1992.

[Wang 94] Wang, K.: Higher-Order Constraint Logic Programming. Dissertation, Universität Bremen, 1994.

[Wolff 94a] Wolff, B.: Proving Transformations in Isabelle. KORSO Bericht, in [Kri 94b].

[Wolff 94b] Wolff, B.: SPEC - A Unified Approach to Modularisation, Parametrisation, and Views in Attributations, KORSO Bericht. in [Kri 94b].

[WS 94] Wolff, B., Shi, H.: A Calculus of Transformation. KORSO Bericht. in [Kri 94b].