7.2. Universelle Entwicklungsumgebung (UniHB)

Als Basis für die konkrete Kombination von Entwicklungswerkzeugen (s.u. Abschnitt 7.3) soll einerseits eine Universelle Entwicklungsumgebung für Formale Methoden gemäß den Vorgaben des KORSO Systemarchitektur-Rahmens ([KM 94], vgl. Abschnitt 5.3) realisiert werden, andererseits je ein generisches Transformations-Entwicklungs- und Anwendungssystem (Abschnitt 7.2.5, Abschnitt 7.2.6).

Architektur der UniForM Workbench

Die UniForM Workbench umfaßt daher, wenn sie noch nicht durch spezielle Werkzeuge erweitert ist, folgende Systemteile (im Vergleich dazu die Schichten desReferenz-Modells für Entwicklungsumgebungen, vgl. Abb. 5.3-2):

* den User Interaction Manager als Benutzerschnittstelle,

* den Development Manager als Kombination der Schichten für die Software-Entwicklungs-Steuerung und die Sicherheits- und Qualitätsanforderungen,

* in der Schicht für die Software-Erstellung:

* das generische Transformations-Anwendungssystem, das später mit entsprechenden Regeln und Taktiken zu spezialisierten Transformation Systems instantiiert wird,

* das generische Transformations-Entwicklungssystem,

* den Integration Manager zur Erweiterung des Systems selbst,

* in der Schicht für die Qualitätssicherung:

* das generische Beweissystem Isabelle,

* den Repository Manager für die Objektverwaltung einschließlich der Versions- und Konfigurationsverwaltung,

* den Subsystem Interaction Manager als höhere Schnittstelle, auch zu kommerziellen Tool-Bus Systemen.

Der so entstandene Prototyp, die UniForM Workbench, siehe Abb. 7.2-1 wird nach Beendigung des Projekts als Public-Domain System der Öffentlichkeit zur Verfügung gestellt (Isabelle ist getrennt als Public-Domain System zu beziehen). Die weiteren während des Projektes in der Workbench integrierten Werkzeuge (s. Abschnitt 7.3.1) unterliegen größtenteils den Lizenzbestimmungen der Hersteller; sie können daher nicht frei verfügbar gemacht werden.



Abbildung 7.2-1: Die UniForM Workbench ohne weitere Entwicklungswerkzeuge

Drei Ebenen der Entwicklung

Die UniForM Workbench unterstützt die einheitliche Behandlung von drei Ebenen der korrekten Entwicklung (vgl. [KKLT 91, KKT 92]):

(1) die korrekte Entwicklung von Programmen,

(2) die korrekte Entwicklung von spezialisierten Transformationswerkzeugen,

(3) die korrekte Entwicklung des Systems selbst durch Integration weiterer Werkzeuge.

So folgt die formale Entwicklung von Regeln, Taktiken, Transformationsprogrammen etc. auf Ebene (2) demselben Schema wie die von Programmen auf Ebene (1). Diese Objekte werden daher ebenso in einem Entwicklungsgraphen verwaltet, die UniForM Workbench wird quasi neu für diese Art der Entwicklung instantiiert. Als Besonderheit werden z.B. spezielle Transformationswerkzeuge für die Entwicklung von Taktiken und Transformationsprogrammen für dieser Ebene generiert.

Ebenso ist es wichtig, die Fortentwicklung des Systems selbst mit allen Aspekten der Korrektheit, der Versionsverwaltung etc. mit der UniForM Workbench zu unterstützen. Hier kommen auch Aspekte der Konformität zu dem Vorgehensmodell zum tragen.

Abb. 7.2-2 bis 7.2.4 zeigen die Instantiierungen der UniForM Workbench für die drei Ebenen.


Abbildung 7.2-2: Die UniForM Workbench mit Werkzeugen für die Programmentwicklung


Abbildung 7.2-3: Die UniForM Workbench mit Werkzeugen für die Transformationsentwicklung


Abbildung 7.2-4: Die UniForM Workbench mit Werkzeugen für die Systementwicklung
Verfeinerte Systemarchitektur (UniHB)
Die Systemarchitektur der UniForM Workbench wurde verfeinert (siehe Abb. 7.2-5). Die Verwendung von Fenstern, Schriftarten etc. wird ganz auf das international weit verbreitete und frei im public domain verfügbare Softwarepaket Tcl/Tk abgestellt (vgl. Abschnitte 7.2.3 und 7.2.5). Ein Werkzeug kommuniziert mit dem Subsystem Interaction Manager und verfügt so indirekt über eine eigene Tcl/Tk Wish, um Parallelverarbeitung zu ermöglichen.

Abbildung 7.2-5: Die (verfeinerte) Systemarchitektur der UniForM Workbench

7.2.1. User Interaction Manager als gemeinsame Benutzungsoberfläche
(UniHB, Elpro)

Mit daVinci (vgl. Abschnitt 5.3.2, Abschnitt 5.3.3) soll ein User Interaction Manager als gemeinsame Benutzungsoberfläche realisiert werden. Dabei geht es nicht nur um eine Benutzungsschnittstelle mit Fenstern, Menüs etc. (sie werden ohnehin mit einem Standardprodukt realisiert) sondern um die Verwendung eines generischen Visualisierungswerkzeugs, das sich, instantiiert mit entsprechenden Visualisierungsdefinitionen, sowohl zur grafischen Darstellung der Datenbasis (d.h. eines Projektgraphen, vgl. Abschnitt 5.3.2, Abschnitt 7.2.2) als auch ihrer Inhalte einsetzen läßt. Dabei ist immer die Interaktion mit der eigentlichen Applikation gewährleistet, auch bei gleichzeitiger Darstellung eines Objekts in verschiedenen Sichten.

Grafische Darstellung von Termen, Regeln

Die Inhalte von Knoten des Projektgraphen (Einheiten) werden in der Regel von den Werkzeugen, die damit arbeiten, dargestellt. Für einige von ihnen sollen exemplarisch Visualisierungsdefinitionen für daVinci entwickelt werden, so daß ein einheitliches Werkzeug zur Darstellung und zum strukturierten Editieren zur Verfügung steht. Im Vordergrund steht die Darstellung von Termen einer Spezifikation als eingerückte Texte, Formeln in mathematischer Notation, Transformationen in Regelschreibweise; diese Liste ist je nach Bedarf erweiterbar.

Benutzerführung

Die eigentliche Benutzungsschnittstelle mit einheitlichem "look and feel" der Benutzerführung wird bereits von daVinci zur Verfügung gestellt; hier sind einige kleine Erweiterungen geplant. Eine Portierung von OpenLook nach Motif soll an den de-facto Industriestandard anpassen.

Visualisierung und Animation von Objekten

Werte in einer Spezifikation bzw. einem Programm sollen mit daVinci grafisch dargestellt werden, z.B. ein sich dynamisch verändernder Stapel; hier wird derzeit im Rahmen einer Diplomarbeit vorgearbeitet. Allgemeiner soll hier ein Werkzeug entstehen, das sich zur Validation einer formalen Spezifikation durch Animation eines Modells eignet (vgl. die Anwendung in Abschnitt 7.4.2). Ein Beispiel wäre die Darstellung eines kleinen Schienennetzes mit darauf bewegten Objekten, Signalen etc.
Ergebnisse
* User Interaction Manager durch Einbindung von daVinci in UniForM Workbench,

* Instantiierungen von daVinci für die grafische Darstellung von Termen, Regeln sowie die Visualisierung und Animation von Objekten.
Grafische Darstellung von Termen, Regeln (UniHB)
1995 standen bezüglich der Entwicklung eines generischen Text-Layout-Moduls für daVinci Analyse, Konzeption und Entwurf im Vordergrund. Ergebnisse:

- Analyse des benötigten Funktionsumfangs zur Darstellung strukturierter Texte (Formeln, Regeln, Programme, etc.).

- Entwicklung einer Sprache zur regelbasierten Layout-Definition eines strukturierten Textes.

- Entwurf eines Integrationsrahmens zur späteren Einbettung in daVinci .

- Konzeption der Interaktionsmöglichkeiten, insbesondere für strukturiertes Editieren.

Aus pragmatischen Gesichtspunkten wurde die Implementation dieses Arbeitspaketes gegenüber dem Arbeitsplan auf das 1. Halbjahr 1996 verschoben, damit die aus der Motif-Portierung von daVinci (siehe nächsten Absatz) resultierenden Verbesserungen von vornherein berücksichtigt werden können. Ferner wurde auf diesem Gebiet eine Diplomarbeit begonnen, die im Frühjahr 1996 abgeschlossen sein wird. Weil beide Arbeitspakete zeitlich ausgetauscht wurden, hat diese Umstellung keinerlei Auswirkung auf die Zielerreichung.
Vereinheitlichung der Benutzerführung in daVinci V2 (UniHB)
Die vollständige Umstellung der Benutzungsoberfläche von daVinci auf den im UNIX-Umfeld vorherrschenden Industriestandard "Motif" wurde im Berichtszeitraum abgeschlossen. Hierzu wurde das international weit verbreitete Softwarepaket Tcl/Tk eingesetzt ([Ous 94], vgl. auch Abschnitt 7.2.5); es ist frei verfügbar und wird fortwährend an alle gängigen Betriebssysteme angepaßt. Durch diese Lösung ist die Portierbarkeit von daVinci auf alle marktgängigen UNIX-Plattformen gewährleistet. Ergebnisse:

- Portierung der vorhandenen Benutzungsoberfläche von daVinci V1.4 nach Tcl/Tk. Darüberhinaus geplante Erweiterungen am Funktionsumfang für daVinci V2 werden im 1. Halbjahr 1996 realisiert.

- Die Grundlagen für einen Mehrfensterbetrieb (d.h. die Verteilung einer Graph-Visualisierung auf mehrere Fenster) wurden dabei bereits berücksichtigt und implementiert.

- Die Applikationsschnittstelle von daVinci wurde um das Tcl/Tk Protokoll erweitert, so daß jetzt integrierte Benutzungsschnittstellen-Programmierung auf sehr einfache Weise möglich ist. Dadurch kann von nun an daVinci V2 im Rahmen der UniForM Workbench als einheitlicher User Interaction Manager zur Darstellung und Verwaltung von Benutzungsoberflächen eingesetzt werden.

Es ist beabsichtigt, nach Abschluß der Restarbeiten und Qualitätssicherungsphase im 1. Halbjahr 1996 daVinci V2 weltweit im Internet verfügbar zu machen, wie es auch schon mit der z.Z. verfügbaren Vorversion daVinci V1.4 praktiziert wurde (vgl. auch http://www.informatik.uni-bremen.de/~davinci ).
Aufwände
Plan: UniHB: 19 PM, Elpro: 1 PM

7.2.2. Repository Manager für die Objektverwaltung
(UniHB, Elpro)

Entwicklungsgraph und Grafische Darstellung

Die Objekte (z.B. Spezifikationen, Beweisverpflichtungen und Beweise, Lemmata, Transformationen, Entwicklungsskripte) sowie die strukturellen und methodischen Relationen (z.B. Vererbung, Verfeinerung) in einem Entwicklungsgraphen (vgl. Abschnitt 5.3.2) sollen repräsentiert und mit einem Repository Manager nach PCTE Richtlinien verwaltet werden. Auf diese Weise wird eine verallgemeinerte Versionskontrolle sowie eine Konfigurationsverwaltung erreicht. Die Realisierung orientiert sich an dem einheitlichen Rahmen für die Integration, vgl. Abschnitt 5.3.4., Abschnitt 7.2.3. Die Objekte und Relationen in einem Entwicklungsgraphen sollen mit daVinci visualisiert werden.
Ergebnisse
* Repository Manager samt Einbindung in die UniForM Workbench,

* Instantiierungen von daVinci für die grafische Darstellung von Objekten und Relationen in einem Entwicklungsgraphen .
Aufwände
Plan: UniHB: 13 PM, Elpro: 1 PM

7.2.3. Subsystem Interaction Manager und Integration Manager
(UniHB)

Einheitlicher Rahmen für Interaktion und Integration (UniHB)

Es soll ein einheitlicher Rahmen für die Integration von Subsystemen und Werkzeugen, Verkapselung und Interaktion (z.B. mit loser aber getypter Kopplung) entwickelt werden, bei der eine funktionale Programmiersprache als Skript-Sprache dient. Basis dafür sind die in Abschnitt 5.3.4 beschriebenen Arbeiten zur Architektur und denKonzepten von Messenger. In diesem Zusammenhang wird ein Subsystem Interaction Manager realisiert sowie ein Integration Manager.

Es soll untersucht werden, inwieweit die Installation und Integration neuer Werkzeuge (halb-) automatisch aus der Schnittstellenspezifikation generiert werden kann, ähnlich wie RPCs (remote procedure calls) aus reinen C-Funktionen in einer verteilten Umgebung automatisch generiert werden [OSF 92]. Schließlich muß das Problem der Heterogenität und Offenheit gelöst werden, d.h. der Zugriff aus dem Subsystem Interaction Manager auf Systeme, die z.B. unter der HP SoftBench integriert wurden, und umgekehrt. UniHB entwirft eine unterliegende Standard-Schnittstelle für die Werkzeug-Kommunikation, so daß an einen, evtl. sogar beliebige kommerzielle Tool-Busse angekoppelt werden kann.
Ergebnisse
* Basis-Schnittstelle für die Werkzeug-Kommunikation,

* Subsystem Interaction Manager samt Einbindung in die UniForM Workbench,

* Integration Manager samt Einbindung in die UniForM Workbench.
Basis-Schnittstelle für die Werkzeug-Kommunikation (UniHB)
Die Systemarchitektur der UniForM Workbench wurde verfeinert (siehe Abb. 7.2-5). Der Subsystem Interaction Manager erscheint als ein gemensamer "Bus", auf dem allen globalen Änderungen des Gesamtsystemzustands kommuniziert werden, d.h. solche, die für die anderen Werkzeuge bzw. das Repository relevant sind. Dies kann auch bedeuten, daß ein eigener "Kanal" für die Kommunikation eines Werkzeuges mit dem Repository eröffnet bzw. geschlosssen wird, über den eine direkte (und damit effiziente) Kommunikation abläuft.

Die Arbeiten an der Basis-Schnittstelle sind in der funktionalen Programmiersprache Haskell inzwischen soweit fortgeschritten, daß mit einem Abschluß im Frühjahr 1996 gerechnet wird.
Integration Manager (UniHB)
Zum Integration Manager wurde konzeptionelle Vorarbeit geleistet. Die Beschreibung von Datenobjekten und der Verkapselung von Werkzeugen zu ihrer Integration in der UniForM Workbench soll in einer Teilsprache von Haskell erfolgen, die damit die Funktion der international verbreiteten Beschreibungssprache IDL (Interface Definition Language) übernimmt. Aus dieser Beschreibung sollen Anknüpfungen ("stubs") automatisch generiert werden. Damit wird die Arbeit an der Integration aufgrund der höheren Abstraktion und Generierung wesentlich erleichtert.

Durch die vorgezogenen Arbeiten am Integration Manager, die erst für 1996 vorgesehen waren, hat sich die Fertigstellung des Subsystem Interaction Managers etwas verzögert; insgesamt tritt aber kein Verzug ein.
Aufwände
Plan: UniHB: 13 PM

7.2.4. Development Manager zur Verwaltung von Entwicklungen
(UniHB)

Entwicklungsskripte, Wiederverwendung von formalen Entwicklungen

Es soll ein Development Manager gemäß Abschnitt 5.3.5 realisiert werden, der Entwicklungsskripte aufzeichnet und sie durch "lifting" einer formalen Behandlung als Enwicklungen zugänglich macht, damit mit den Konzepten zur Wiederverwendung von formalen Entwicklungen experimentiert werden kann.

Eine Entwicklung wird formal als Komposition von Transformationen dargestellt, vgl. Abschnitt 5.1.4. Im System entspricht eine solche abstrakte Entwicklung einem Entwicklungsskript, d.h. einer Folge von System-Aktionen (vgl. Abschnitt 5.3.5). Die wechselseitige Umwandlung, Abstraktion im Transformationskalkül etc. (vgl. Abschnitt 5.1.4) als Grundlage für die Wiederverwendung von formalen Entwicklungen soll fortentwickelt und im System realisiert werden, so daß dieser Ansatz bei der Entwicklung der Fallstudie experimentell eingesetzt werden kann.

Kontrolle der Korrektheit bei Interaktionen

Exemplarisch soll gezeigt werden, wie Interaktionen im Development Manager auf ihre Korrektheit hin überprüft werden.

Kontrolle in Bezug auf ein Vorgehensmodell

Es soll ferner untersucht werden, ob man syntaktische oder semantische (d.h. dynamisch zu überprüfende) Kriterien aufstellen kann, die die Konformität einer Entwicklung zu einem gegebenen (instantiierten) Vorgehensmodell garantieren (siehe Abschnitt 5.3.5), und inwieweit der Transformationsansatz hierfür eingesetzt werden kann (Steuerung eines Vorhabens nach den Regelungen des V-Modells durch Einschränkung des Satzes von anwendbaren Transformationen im nächsten Entwicklungsschritt, Entwicklung schematischer Entwicklungsskripte, etc.; siehe auch Abschnitt 7.1.3).
Ergebnisse
* Development Manager samt Einbindung in die UniForM Workbench,

* Dokument "Wiederverwendung von Entwicklungen in der UniForM Workbench",

* Dokument "Anwendung des Transformationsansatz auf die Realisierung des V-Modells".
Aufwände
Plan: UniHB: 17 PM

7.2.5. Transformations-Entwicklungssystem
(UniHB / UniOL)

Im Bereich der Transformationssysteme soll mehrgleisig verfahren werden. Einerseits soll das in der Forschung weitverbreitete Beweissystem Isabelle (siehe Abschnitt 5.2.1) verwendet werden, um den in Bremen entwickelten Transformationskalkül zu realisieren und die Korrektheit von Transformationen beweisen zu können, andererseits sollen fertige entwickelte Transformationsprogramme in einer speziellen Ausführungsumgebung effizient ausgeführt werden (s. Abschnitt 7.2.6).

Zur Realiserung des Transformations-Entwicklungssystems soll der in Abschnitt 5.1.4 zitierte Transformationskalkül in dem Beweissystem Isabelle repräsent werden; mit diesen Arbeiten wurde bereits im Ansatz begonnen. Damit steht die gesamte Methodik der Programmentwicklung durch Transformation zur Verfügung. Durch die Technik der Logik-Repräsentation (siehe Abschnitt 5.1.3, Abschnitt 7.1.1) entsteht ein Multi-Logik System mit mehreren Objekt-Logiken; so kann die Korrektheit von Transformationen bzw. Übersetzungen bewiesen werden. In diesem System ist dann natürlich auch die Ausführung von Transformationen möglich; für eine konkrete Entwicklung muß man es aber als eher ineffizienten Prototyp betrachten, etwa so effizient wie die immer noch sehr mühsame interaktive Durchführung von formalen Beweisen, mit der zusätzlich notwendigen Überprüfung von hier meist aufwendigen Anwendungsbedingungen.

Im Transformationsentwicklungssystem werden Taktiken spezifiziert und zu korrekten, operationell ausführbaren, optimierten Transformationsprogrammen entwickelt (vgl. Abschnitt 5.1.4, Abschnitt 7.1.2). Ein Teilaspekt hierbei ist die Darstellung und ggf. Weiterentwicklung von semantischen Bereichen. Die formale Entwicklung von Regeln, Taktiken, Transformationsprogrammen etc. folgt demselben Schema wie die von Programmen. Diese Objekte werden daher ebenso in einem Entwicklungsgraphen verwaltet, die UniForM Workbench wird quasi neu für diese Art der Entwicklung instantiiert. Insbesondere wird der Entwicklungsgraph ebenso grafisch dargestellt.

Fertig entwickelte Transformationsprogramme werden in einem zweiten Schritt in das Transformationsausführungs-system (Abschnitt 7.2.6) übertragen. Soweit möglich soll dies durch automatische Querübersetzung erfolgen.

Da das Transformations-Entwicklungssystem es erlaubt, über die Korrektheit von Taktiken Aussagen zu machen und sie formal zu manipulieren, wird auch die Wiederverwendung von Entwicklungen ermöglicht (vgl. Abschnitt 5.1.4, Abschnitt 5.3.4, Abschnitt 7.2.4).
Ergebnisse
* Transformation Development System samt Einbindung in die UniForM Workbench,

* Dokument "Entwicklung von korrekten, effizienten Transformationsprogrammen mit dem Transformation Development System der UniForM Workbench",

* Dokument "Übertragung von Transformationsprogrammen in das Transformation Application System der UniForM Workbench".
Taktische Transformation und taktisches Beweisen als Deduktionsprozesse
Die einheitliche Sicht von taktischer Transformation und taktischem Beweisen als Deduktionsprozesse in einem einheitlich formalisierten Entwicklungsprozeß wurde in [BK 96] untersucht. Auf dieser Basis soll im Transformationssystem eine Transformationsregel zunächst als Basisregel ("logischer Kern") bewiesen werden, aus der dann mit verschiedenen Anwendungstaktiken die für den Benutzer verwendbaren Regeln gewonnen werden.
Schnittstelle zum User Interaction Manager (UniHB)
Implementierung von "sml_tk", einer abstrakten, funktionalen Schnittstelle zum User Interaction Manager. (Online-Dokumentation: http://www.inforatik.uni-bremen.de/~bu/isa_contrib/DOC). Diese Schnittstelle stellt einen freien abstrakten Datentyp für grafische Objekte (genannt "Widgets", das sind Knöpfe, Unter-Fenster mit Textinhalt, Menüs etc.) zur Verfügung (vgl. Abschnitt 7.2.1). An die Varianten dieses Typs können sowohl Darstellungsattribute (Font, Größe, etc.) als auch deskriptive Layoutinformation (z. B. "dieses Objekt ist links neben jenem zu plazieren") eingefügt werden. Ein besonderer Aspekt sind sogenannte "Bindings", das sind ML-Funktionen vom Typ unit -> unit, die zusammen mit einem "Event" (z.B. Doppelklick auf Maustaste) an ein Widget "angeheftet" werden, und die ausgeführt werden, wenn der Cursor auf das betreffende Widget zeigt und das "Event" eintritt. Eine (kleinere) Bibliothek von Standard-Komponenten ergänzt die Basisschnittstelle.

Der Datentyp wird von der Schnittstelle auf einen Interpreter der Kommandoscriptsprache Tcl/Tk [Ous 94] abgebildet, die ein sehr populär gewordenes X-Window-Toolkit zur grafischen Darstellung ansteuert. Es besteht die Hoffnung, daß Tk die Entwicklung von hochwertigen Oberflächen sowohl für akademische Prototypen als auch Anwendungen aus dem industriellen Umfeld in so entscheidender Weise vereinfacht, wie LATEX und Word die Produktion hochwertigen Layouts von (wissenschaftlichen) Texten. Der Benutzer kann durch sml_tk in einem sehr abstrakten, funktionalen und modularen Stil Benutzerschnittstellen schreiben, ohne auch nur eine einzige Zeile in Tcl schreiben zu müssen, das keine Modularisierungskonzepte kennt.

Die Schittstelle sml_tk, die für die Anbindung von Isabelle in der funktionalen Programmiersprache SML zur Verfügung steht, wird im weiteren Projektverlauf erweitert und auf die funktionale Programmiersprache Haskell portiert werden. Ein technischer Bericht über diese Schnittstelle, die wesentlich für die Integration einzelner Systemteile der UniForM Workbench mit der grafischen Oberfläche des User Interaction Manager ist, wird zu einem späteren Zeitpunkt vorgelegt.
Erster Prototyp eines generischen Transformationsentwicklungssystems (UniHB)
Der erste Prototyp eines generischen Transformationsentwicklungssystems wurde unter dem Namen ISAWIN auf der Basis des generischen Theorembeweisers Isabelle ( http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html, siehe auch [Pau 95]) sowie der Schnittstelle sml_tk realisiert. Kerngedanke ist dabei, Transformationen als Zusammensetzung aus "logischem Kern" und "taktischem Zucker" aufzufassen. Der logische Kern ("Synthese-Theorem") besteht aus einem Theorem in einer speziellen Form, das aus einer Objektlogik folgt, und dessen Anpassung an einen Anwendungskontext durch ein taktisches Anwendungsprogramm, den "taktischen Zucker" vorgenommen werden kann. Da Isabelle generisch ist, d.h. mit mehreren Objektlogiken (=Spezifikationssprachen) arbeiten kann (also z.B. Logik höherer Stufe (HOL), aber auch: CSP oder Z), ist auch ISAWIN in Bezug auf die Objektlogik generisch. Folglich können in jeder dieser Spezifikationssprachen entsprechende Transformationen entwickelt werden.

Aus der Auffassung von Transformationen als Synthese-Theoremen resultiert die Möglichkeit, die Korrektheit einer Transformation in Isabelle formal zu beweisen (Transformationsentwicklung). Ebenso besteht die Möglichkeit, Transformationen einfach axiomatisch zu fordern (was einer unbewiesenen Implementierung entspricht). ISAWIN ist nun ein parametrisierter Datentyp (ein ML-Funktor), der mit einer Liste von Transformationen (also Paaren aus Synthese-Theoremen und taktischen Zuckerfunktionen) instantiiert werden kann. In jeder Instanz des Funktors sind Steuerfunktionen vorhanden, die die Kreierung eines Transformationssystems über diesen Transformationen samt entsprechender Benutzungsoberfläche ermöglichen.

Das System YATS (Yet Another Transformation System) ist eine Instanz von ISAWIN mit der formal bewiesenen Transformation "Global Search" (vgl. [Smi 91] sowie [SD 95]). Dieses nichttriviale Beispiel wurde vor allem gewählt, um die Machbarkeit und Vielseitigkeit des Ansatzes zu demonstrieren. Technisch kann diese Instantiierung (damit Erzeugung eines Transformationssystems!) in wenigen Sekunden durchgeführt werden. Je nach Grad des formalen Nachweises der Korrektheit der Darstellung der Objektlogik (also Konservativität der logischen Einbettung), der Korrektheit der Synthese-Theoreme, der technischen Unterstützung von Fehlermeldungen etc. kann ein beliebiger Übergang zwischen einem "Transformations-Entwicklungssystem" und einem "Transformations-Anwendungssystem" im Sinne des UniForM Projekts erreicht werden.
Arithmetik-Bibliothek (UniHB)
Implementierung (d.h. Mechanisches Beweisen in Isabelle) einer erheblich erweiterten Arithmetik-Bibliothek für Isabelle/HOL zur besseren maschinellen Unterstützung von Arithmetik-Beweisen in den natürlichen Zahlen.

Online-Dokumentation: http://www.infrmatik.uni-bremen.de/~bu/isa_doc/OWN/Arith.

Überblick über verfügbare Isabelle-Theorien: http://ww.informatik.uni-bremen.de/~bu/isa_doc/OWN/index.html.

Andere Bremer HOL-Theorie-Beiträge: http://ww.informatik.uni-bremen.de/~bu/isa_doc/OWN/index.html.

Die Bibliothek umfaßt viele Theoreme über die Subtraktion und die Vereinfachung von Gleichungen und Ungleichungen (z.B. A+add_right_cancel_less = "(n+m < k+m) = (n<k)" A+diff_add_swap = "m <= n ==> k=n-m = k+m=n"), die sich zum Aufbau von Entscheidungsprozeduren durch Termersetzung ("rewriting") eignen. Eine verbesserte Version und ein technischer Bericht werden zu einem späteren Zeitpunkt vorgelegt.
Aufwände
Plan: UniHB: 14 PM, UniOL: 1 PM

7.2.6. Transformations-Anwendungssystem
(UniHB / UniOL)

Das Transformations-Anwendungssystem soll eine benutzungsfreundliche Umgebung für die Ausführung von Transformationen bieten; dabei ist vor allem an diejenigen Benutzer gedacht, die nicht neue Regeln oder Taktiken entwickeln wollen oder können (vgl. Abschnitt 7.1.2 bzw. Abschnitt 7.2.5), sondern lediglich interaktiv Transformationen zur Entwicklung von Spezifikationen und Programmen anwenden wollen.

In der Benutzungsoberfläche sollen die zu transformierenden Terme, Anwendungsstellen, anwendbare Transformationen, Parameter, generierte Anwendungsbedingungen etc. mit daVinci grafisch dargestellt werden (siehe Abschnitt 7.2.1). Hier finden die Erfahrungen Eingang, die mit dem im Projekt PROSPECTRA entwickelten Protypsystem gesammelt wurden.

Die Methodik der Entwicklung effizienter Transformationsprogramme ist bereits im Transformations-Entwicklungssystem (s. Abschnitt 7.2.6) realisiert. Parallel dazu wird auf eine effiziente Anwendung bzw. Ausführung von Transformationen hingearbeitet. Es soll eine Art Laufzeitsystem (d.h. Kollektion von Systemprogrammteilen in einer funktionalen Programmiersprache bzw. C) für die Ausführung von Transformationen entstehen, das Basis-Mechanismen für "extended matching", automatische Überprüfung statisch-semantischer Anwendungsbedingungen etc. umfaßt. Dazu soll ein Beweissystem für die Verifikation von Anwendungsbedingungen angekoppelt werden (z.B., aber nicht notwendigerweise, Isabelle).

Exemplarische Anwendungen des so entstandenen generischen (Beweis- und) Transformationssystems sind für Nebenläufigkeit und Realzeit geplant (siehe Abschnitt 7.3.2). Daneben sollen (außerhalb des eigentlichen Projektes) die bereits im Rahmen der Projekte PROSPECTRA und KORSO entwickelten und teilweise als korrekt bewiesenen Transformationen für die Entwicklung und Optimierung sequentieller Programme (bzw. Abstrakter Datentypen, vgl. Abschnitt 5.1.4) in das System integriert werden, so daß auch mit ihnen ggf. experimentiert werden kann.
Ergebnisse
* Transformation Application System samt Einbindung in die UniForM Workbench,

* Dokument "Programm-Entwicklung durch Transformation mit dem Transformation Application System der UniForM Workbench".
Generisches Transformationsentwicklungssystem als Transformationsanwendungssystem (UniHB)
Erste Anwendungen wurden mit dem Prototyp eines generischen Transformationsentwicklungssystems (siehe oben) realisiert.
Effiziente Matching-Algorithmen (UniHB)
Im Vordergrund der beiden Arbeiten [CQS 96] und [Shi 96] stehen effiziente Algorithmen für das Matching zweiter Stufe bzw. das semantische Matching. Die Algorithmen wurden im Beweissystem Isabelle implementiert und ausführlich getestet, so daß sie leicht in das prototypische Transformations-Anwendungssystem integriert werden können. Ziel ist die Formalisierbarkeit, Kompaktheit und Wiederverwendbarkeit von Transformationsregeln und die Automatisierbarkeit von Transformations-Anwendungen.
Aufwände
Plan: UniHB: 28 PM, UniOL: 1 PM