"Programmieren mit Vertrag"
JaWA
JaWA-Präcompiler
Der folgende Text beschreibt die Bedienung des JaWA-Präcompilers inklusive aller seiner Optionen und Konfigurationsmöglichkeiten. Nach einer thematischen Einführung werden die Erweiterungen der Sprache JaWA gegenüber Java erläutert. Ein einführendes Beispiel zeigt sowohl die Bedienung des JaWA-Präcompilers, wie auch die Methode zur systematischen Entwicklung von Software mittels abstrakter Datentypen, in der Praxis.
Die folgenden Begriffe sollen einen ersten Überblick geben. Eine ausführlichere Beschreibung ist als Einführung formuliert:
"Programmieren mit Vertrag"
JaWA
JaWA-Präcompiler
... die Anwendung des JaWA Präcompiler
an einem Beispiel sehen möchten,
... etwas über die Ziele der Sprache
JaWA erfahren möchten,
... wissen wollen, was ein Abstrakter Datentyp
(ADT) ist,
... die Erweiterungen der Sprache JaWA
gegenüber Java kennenlernen möchten,
... die möglichen Modi der Übersetzung
im Vergleich betrachten möchten,
... Informationen zur Bedienung benötigen,
... Sourcecodes oder Dokumentation
herrunterladen möchten,
In diesem Kapitel wird eine thematische Einführung in die Problematik der Entwicklung korrekter Software und dem Lösungsansatz der Sprache JaWA gegeben. Es dient nicht direkt der Beschreibung des JaWA-Präcompilers, sondern erläutert den Hintergrund, der zu seiner Entstehung im Rahmen einer Diplomarbeit führte. In den nachfolgenden Kapiteln wird dann konkret auf die Spracherweiterungen, die Bedienung und die Konfigurationsmöglichkeiten des JaWA-Präcompilers eingegangen.
Das Kapitel ist in die folgenden Abschnitte unterteilt:
Zum Seitenanfang
Zum Inhaltsverzeichnis
Obwohl bis zum heutigen Tage durch Entwurf und Einsatz von umfangreichen Softwaresystemen viele Erfahrungen und ein beträchtliches technisches Know-how im Bereich der elektronischen Datenverarbeitung angesammelt werden konnte, gelingt es oftmals nicht, Software fehlerfrei zu entwickeln. Dennoch werden Computer in Bereichen eingesetzt, in denen Fehler katastrophale Folgen haben können. Durch die in den letzten Jahren enorm gestiegene Komplexität von Computersystemen, die Teamarbeit und Projektmanagement erfordert, ist die Aufgabe der Entwicklung fehlerfreier Systeme noch erheblich erschwert worden. Dieses Problem wurde durch Forderungen nach Wiederverwendbarkeit sogar noch weiter verstärkt, die bei objektorientierten Methoden einen der wesentlichen Aspekte ausmacht.
Fehler in Programmen können sehr teuer sein, dennoch gibt es für die meisten Sprachen kein befriedigendes Konzept zur Entwicklung zuverlässiger Software. Formale Sprachen für die systematische Spezifikation aller Aufgaben einer Software können an dieser Stelle sinnvolle Dienste leisten. In der Industrie stoßen sie aber oftmals auf Ablehnung, da sie einen Mehraufwand erfordern, dessen Nutzen nur in sicherheitskritischen Bereichen als wirtschaftlich erachtet wird. Ohne eine formale Beschreibung kann aber die Gültigkeit bestimmter gewünschter Eigenschaften des Softwaresystems nicht bewiesen werden. Die Möglichkeit, daß sich auch nach umfangreichen Testdurchläufen immer noch Fehler in der Software befinden, kann nicht ausgeschlossen werden. Software zu entwickeln bedeutet daher oft, nach Kompromissen zu suchen und zwischen Kosten und Korrektheit abzuwägen.
Das Konzept des Programmierens mit Vertrag setzt genau an dieser Stelle an. Es versucht einen Beitrag zu leisten, der beiden Aspekten gerecht wird und zusätzlich Wiederverwendbarkeit fördert. Das Konzept wurde von Bertrand Meyer vorgeschlagen und bündelt eine Vielzahl von theoretischen und praktischen Erkenntnissen. Es vereint den objektorientierten Entwurf mit abstrakten Datentypen und Methoden aus der Programmverifikation.
Die Idee kann zu vier Hauptzielsetzungen zusammenfaßt werden:
Formale Spezifikation
Dokumentation
Debugging
Software-Toleranz
Die Sprache Eiffel wurde entworfen, um das Konzept praktisch zu verwirklichen. Sie ist objektorientiert, generisch, ermöglicht Mehrfachvererbung und besitzt einen Ausnahmemechanismus. Eiffel unterscheidet sich in großen Teilen kaum von heute aktuellen objektorientierten Sprachen. Die wesentlichen Sprachelemente für die Programmierung und auch die Mächtigkeit sind vergleichbar. Jedoch besitzt Eiffel einen methodischen Hintergrund, der sich von dem anderer Sprachen unterscheidet und gerade dieser Hintergrund eröffnet Perspektiven für die Entwicklung von Software höherer Qualität.
Auch wenn Eiffel eine große Schar von Anhängern gefunden hat und in einer Vielzahl kommerzieller Produkte verwendet wird, konnte sie sich nicht gegen eine Sprache wie C++ durchsetzen. Dies liegt sicherlich an der weiten Verbreitung dieser Sprache und ihrer langen Geschichte, in deren Anfängen mit C eine Standardsprache für die Systemprogrammierung auf unterschiedlichsten Plattformen entstand.
Mit Java wurde 1991 von dem Unternehmen Sun Microsystems eine Sprache veröffentlicht, die die Nachfolge von C++ antreten und vor allem im Bereich des Internet eingesetzt werden soll. Syntaktisch auf C++ aufbauend, enthält sie eine Reihe von Veränderungen und Erweiterungen. Java erfuhr einen regelrechten Boom. Die Sprache verbreitete sich rasant und entwickelte sich schnell zu einer der wichtigsten Sprachen für die praktische Softwareentwicklung, gerade auch im Bereich der verteilten Systeme. Durch die Unterstützung des dynamischen Nachladens von Klassen, können Systeme über das gesamte Internet verteilt, entwickelt und eingesetzt werden.
Im Rahmen einer Diplomarbeit wurde das Konzept des Programmierens mit Vertrag untersucht und auf die Sprache Java übertragen. Dazu werden Anweisungen in die Sprache aufgenommen, die die Formulierung von Zusicherungen in den Programmen ermöglichen. Damit ein so erweitertes Programm auch weiterhin ohne Probleme direkt vom Java-Compiler akzeptiert wird, besitzen diese Anweisungen die Form von Kommentaren. Diese Kommentare werden von einem Präcompiler in Anweisungen in normalem Java übersetzt, durch die dann zur Laufzeit die Zusicherungen geprüft und bei Verletzung Ausnahmen ausgelöst werden. Auf diese Ausnahmen kann im Programm selbst reagiert werden, um so ein robustes und fehlertolerantes Verhalten zu erzeugen.
Das Ergebnis dieser Arbeit ist die erweiterte Sprache JaWA (Java with Assertions) und der Präcompiler zur Übersetzung ihrer Erweiterungen. Der gewählte Ansatz bei der Übertragung auf Java sieht eine vollkommen transparente Handhabung für den Entwickler vor, ermöglicht aber zusätzlich eine Reihe von Optionen für den Präcompiler, mit dem der Grad der Übersetzung beeinflußt werden kann. Dies ermöglicht einen flexiblen und schrittweisen Übergang, so daß das Konzept des Programmierens mit Vertrag auch nachträglich in bereits bestehende Projekte aufgenommen werden kann. Mit dieser Arbeit stehen die oben genannten Vorteile nun auch dem Kreis der Softwareentwickler in Java zur Verfügung und können mit dem Präcompiler im praktischen Einsatz genutzt werden.
Es wurde in dieser Arbeit sehr viel Wert darauf gelegt, die Übergangsphase problemlos und schrittweise zu gestalten, da ein zu abrupter Wechsel der Methodiken oft auf Ablehnung trifft und so eher schadet als nutzt. Der Entwickler soll langfristig die neuen Methoden schätzen lernen, ihren Einsatz nach und nach intensivieren und so letztlich bei der Entwicklung qualitativ höherwertiger Software unterstützt werden.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Wenn Software entwickelt wird, so sind an diesem Prozeß immer mindestens zwei Gruppen von Personen beteiligt: Zum einen die Entwickler oder Hersteller, welche die Software produzieren, zum anderen die Benutzer oder Kunden, die die Software einsetzen, um mit ihr bestimmte Aufgaben zu erfüllen. Ist das Produkt eine Bibliothek von Softwarekomponenten, so soll der Programmierer, der diese Bibliothek für seine eigenen Programme benutzt, als Kunde dieser Komponenten verstanden werden.
Das Konzept des Programmierens mit Vertrag benutzt nun eine Metapher, wonach zwischen diesen beiden Gruppen ein Vertrag für die Benutzung der Software existiert. Der Vertrag beschreibt, unter welchen Bedingungen die Software eingesetzt werden darf und welche Leistungen sie zu erbringen hat. Diese Bedingungen und Leistungen können als Rechte und Pflichten für die beiden Vertragsparteien angesehen werden.
Was für die eine Gruppe ein Recht ist, ist für die jeweils andere eine Pflicht und umgekehrt. Der Hersteller verspricht die Erfüllung der von ihm angegebenen Leistung, solange der Benutzer die Einhaltung der Bedingungen verspricht. Er braucht diese also nicht mehr explizit zu prüfen, so daß eine einfache und effiziente Implementierung möglich ist. Der Benutzer bekommt diese Leistungen garantiert, sofern er nur die geforderten Bedingungen einhält. Der Vertrag kann somit als Spezifikation der Software aufgefaßt werden.
Ziel ist es nun, durch eine formale Beschreibung der Bedingungen und Leistungen, die Einhaltung des Vertrags prüfen zu können. Deshalb werden auf der Basis einer operationellen Semantik Korrektheitsformeln in die Softwarekomponenten aufgenommen. Eine Korrektheitsformel:
{p} S {q}
besteht aus einer Vorbedingung p, einem Programm S und einer Nachbedingung q. Sie besagt: Ein Programm S ist korrekt bzgl. p und q, wenn nach der Ausführung von S immer die Bedingung q gilt, solange S in einem Zustand gestartet wurde, der p erfüllte. Unter der Voraussetzung p garantiert das Programm die Erfüllung von q. Im Gegensatz zur Methode der Programmverifikation werden diese Korrektheitsformeln jedoch nicht statisch über dem Programmcode bewiesen, sondern dynamisch zur Laufzeit geprüft.
In objektorientierten Sprachen kann jeder Methodenaufruf einer Instanz als Ausführung eines eigenständigen Programms betrachtet werden, bei dem die Felder der zugehörigen Klasse globale Variablen darstellen. Die Vorbedingung der Korrektheitsformeln benennt die Bedingungen, unter denen der Methodenaufruf erlaubt ist, und die Nachbedingung stellt die Leistungen dar, die durch den Aufruf erbracht werden sollen.
Die in diesem Rahmen in den Korrektheitsformeln verwendeten Zusicherungen sind boolesche Ausdrücke, in denen Variablen und Methodenaufrufe enthalten sein können. Diese Zusicherungen können vom Compiler als bedingte Anweisungen übersetzt und so zur Laufzeit geprüft werden. Durch das Verwenden der Methoden können auch komplexe Bedingungen als Zusicherungen formuliert werden. Beispiele für Zusicherungen werden in 1.4 Was sind Zusicherungen? gegeben.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Im Abschnitt 1.1 Motivation wurden die vier Ziele des Programmierens mit Vertrag genannt. Sie sollen nun detaillierter beschrieben werden. Ihr gegenseitiger Einfluß aufeinander spielt dabei eine wichtige Rolle und stellt ein fünftes, indirektes Ziel dar.
Formale Sprache zur Spezifikation
Der wichtigste Aspekt ist die Möglichkeit zur formalen Spezifikation. Zusicherungen stellen einen direkt in die Sprache eingebundenen Mechanismus dar, mit dem dies erreicht werden kann. Es entsteht kein Methodenbruch, wie es der Fall wäre, wenn zunächst in einer formalen Sprache spezifiziert und dann in einer Programmiersprache implementiert würde. Bertrand Meyer schreibt zu diesem Thema:
"Die Vorteile genauer Spezifikationen und einer systematischen
Vorgehensweise bei der Programmentwicklung können gar nicht
überbetont werden. (...) Zusicherungen bieten eine dringend
benötigte Methode, exakt zu beschreiben, was von jeder Partei
in diesen Vereinbarungen erwartet und gewährleistet wird."
Dokumentationshilfe
Die Dokumentation des Softwaresystems gilt als Vertrag zwischen Benutzer und Entwickler. Alle Zusicherungen der Klasse müssen in ihr aufgenommen werden. Somit sind alle Rechte und Pflichten öffentlich bekannt. Das sie von den Benutzern verstanden werden, ist dadurch sichergestellt, daß in Zusicherungen nur boolesche Ausdrücke verwendet werden dürfen, die auch in den übrigen Anweisungen der Sprache verwendet werden. Dies ist wichtig, da der Benutzer möglicherweise formale Methoden nicht beherrscht.
Es wäre nicht sehr praktisch, wenn nach jeder Änderung in den Zusicherungen von Hand Änderungen in der Dokumentation durchführt werden müßte. Viele Softwareingenieure sind der Meinung ,daß die Dokumentation nicht vom Programm getrennt sein sollte. In Eiffel ist beides in derselben Datei enthalten und kann von einem Werkzeug namens "short" automatisch extrahiert werden. Auch Java unterstützt dieses Konzept. Hier heißt das Werkzeug "JavaDoc".
Durch die automatische Extraktion ergeben sich zwei augenfällige Vorteile: Das Entfallen der stupiden Kopierarbeit, die nötig wäre um alle gemachten Zusicherungen in die Dokumentation zu übernehmen und eine Spezifikation, die immer aktuell auf dem neuesten Stand ist. Diese garantierte Konsistenz ist wesentlich für das Konzept des Programmierens mit Vertrag und wird im fünften Punkt näher beschrieben.
Debugginghilfe
Bisher konnte man Zusicherungen nur in das Programm und damit auch in die Dokumentation hineinschreiben. Um zu garantieren, daß sie nicht verletzt werden, müssen die Zusicherungen zur Laufzeit geprüft werden. Erst dann kann man sicher sein, daß sich das System in einem definierten Zustand befindet. Diese Aufgabe wird vom Compiler unterstützt. Er generiert den Code, der eine Zusicherung unter Berücksichtigung der Vererbung prüft. Der Umfang der zu prüfenden Zusicherungen kann durch die in 6. Die Überpruefungsmodi (Checkmodes) angegebenen Modi bestimmt werden.
Die Wahl des geeigneten Modus ist eine Frage nach der Wichtigkeit von Effizienz und Sicherheit. Wenn Effizienz überwiegt, so schaltet man die Überprüfung mit der Option NOTHING für die jeweiligen Klassen aus. Man erzielt einen Speicherplatz- und Zeitvorteil, da der Compiler keinen Code für die Prüfungen erzeugt und daher zur Laufzeit auch keine Prüfungen gemacht werden. Überwiegt Sicherheit, so sollten alle Zusicherungen durch ALL aktiviert bleiben. Der Zeitaufwand kann anhand der Menge der verwendeten Zusicherungen abgeschätzt werden, indem diese als Ausdruck in einer bedingten Anweisung angesehen werden. Hierbei ist zu beachten, daß die Zusicherungen der Klasseninvariante zu Beginn und am Ende der Methode geprüft werden, inklusive der ererbten Zusicherungen. Werden Methodenaufrufe oder komplexe Ausdrücke in den Zusicherungen verwendet, so muß deren Ausführungszeit ebenfalls hinzuaddiert werden.
Die Option PRECONDITIONS stellt einen Kompromiß dar. Der Entwickler der Klasse geht davon aus, daß diese fehlerfrei ist. Dazu hat er sie ausgiebig getestet. Aber benutzt ein Kunde die Klasse vielleicht etwas leichtfertig? Da durch die Zusicherungen in der Vorbedingung keine Notwendigkeit für den Entwickler besteht, die Bedingungen nochmals abzutesten, könnten unvorhergesehene Ausnahmen wie die Division durch 0 auftreten und möglicherweise die Integrität des Systems zerstören. Der Modus PRECONDITIONS ist voreingestellt. Der zusätzliche Zeitaufwand liegt bei ca. 20%.
Unterstützung von Softwarefehler-Toleranz
Bisher kann man mit Zusicherungen beschreiben, was ein Programm leisten soll, und diese Angaben zur Laufzeit überwachen. Aber es ist nicht befriedigend, wenn sich das Programm mit einem Laufzeitfehler beendet.
Eiffel bietet für diesen Fall einen besonderen Ausnahmemechanismus. Man kann am Ende eines Methodenrumpfs einen rescue-Block angeben. Diese wird aufgerufen, wenn der Rumpf eine Ausnahme auslöst. Sinn dieser Klausel ist es, das System in einem stabilen Zustand, der als Klasseninvariante formuliert ist, zu hinterlassen. Das besondere an dieser Art der Fehlerbehandlung ist, daß jeder Methodenaufruf entweder erfolgreich ist oder scheitert und dem Aufrufer dies in jedem Fall gemeldet wird. 1.6 Vertragsverletzungen: Erfolg oder Scheitern geht auf diesen Punkt ausführlicher ein.
Ohne weitere Vorkehrungen führt der Fehler zwar immer noch zur Beendigung des Systems, aber Katastrophen werden verhindert, da sich der Fehler nicht ausbreiten kann. Die Klasseninvariante wird in 2.2 Die Klasseninvariante: 'invariant' beschrieben, die rescue-Anweisung in 2.5 Der Rescue-Block: 'rescue'.
Eine weitere Möglichkeit im Zusammenhang mit Ausnahmen stellt die retry-Anweisung dar. Sie wird dazu innerhalb des rescue-Blocks oder einer von dort aufgerufenen Methode angegeben. Mit ihrer Hilfe kann eine erneute Ausführung des Methodenrumpfs angestoßen werden, die möglicherweise den Vertrag doch noch erfüllen kann. Der Aufrufer erfährt hiervon nichts, außer das der Aufruf etwas länger gedauert hat. Eine detailiertere Beschreibung der retry-Anweisung erfolgt in 2.6 Die Retry-Anweisung: 'retry'.
Mit diesen Sprachelementen kann die Robustheit eines Systems erheblich gesteigert werden. Man erhält ein System, daß selbst in Ausnahmesituationen noch kontrolliert reagiert und somit die Daten des Benutzers bestmöglich schützt.
Synergien
Im vorigen Abschnitt wurden die Vorteile des Programmierens mit Vertrag ausführlich erläutert. Sie stellen ein mächtiges Werkzeug bei der Entwicklung großer Softwaresysteme dar. Aber sobald man einen erfahrenen Entwickler fragt, bekommt man eine Antwort im Sinne von "Ich habe im Laufe meiner Arbeiten einen Entwurfsstil entwickelt, der diese Konzepte bereits beinhaltet. Warum sollte ich also umsteigen und eine neue Methode erlernen, wenn sie mir keine Vorteile mehr bringen kann?".
Eine solche Antwort ist durchaus verständlich. Durch diszipliniertes Arbeiten entstehen Softwareprodukte, die hohen Qualitätsansprüchen gerecht werden. Denn natürlich versucht man in seiner Spezifikation alle Bedingungen zu formulieren, die beim Aufruf einer Methode erfüllt sein müssen. Und natürlich versucht man alle Situationen abzufangen, die zu Fehlern oder gar Abstürzen führen können. Aber die Erfahrungen mit Softwaresystemen lehrt, daß dies in den meisten Fällen nicht gelingt. Auch wenn die Folgen nur selten ein Ausmaß wie im Ariane-Beispiel annehmen, müssen wir uns die Frage stellen: "Warum ist das so? Warum schleichen sich immer wieder Fehler in mein Programm ein?"
Die Antwort lautet: Konsistenz. Heutige Programme besitzen eine so enorme Komplexität, daß man sie nur selten überschauen kann und gleichzeitig jedes Detail im Auge behält. Das Arbeiten im Team erschwert diese Problematik. Innerhalb der Software entstehen Teile, die man vielleicht niemals zu Gesicht bekommt. Man muß sich auf die in der Dokumentation zu den Schnittstellen gemachten Angaben verlassen, ohne wirklich sicher zu sein, daß diese auch eingehalten wurden.
Doch wie oft werden wir über einige Eigenschaften der Software im unklaren gelassen? Die berühmten "undokumentierten Funktionen" sind ein Beispiel dafür. Es ist schade, diese Funktionen nicht zu benutzen, wenn dies eine elegantere oder effizientere Implementierung ermöglicht. Den Satz: "It's not a bug, it's a feature" kennt wahrscheinlich jeder.
Doch was nicht entdeckt wurde, sind die Synergien. Immer dann, wenn durch das Zusammenfassen von Komponenten mehr entsteht, als die Summe ihrer Einzelteile, spricht man von Synergien. Die vier bisher genannten Vorteile besitzen Synergien. Jede formal spezifizierte Eigenschaft wird automatisch dokumentiert, geprüft und kann vom Programm selbst behandelt werden. Der Vertrag und auch die Fehlerbehandlung sind immer auf dem aktuellen Stand. Würde versucht, die Ziele durch vier getrennte Methoden zu erreichen, so würden sich Fehler durch Inkonsistenzen einschleichen. Programmieren mit Vertrag vermeidet dies durch ein einheitliches Konzept. Somit kann bei gleichem Aufwand Software von höherer Qualität, oder anders formuliert, mit weniger Aufwand die gleiche Qualität, erreicht werden.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Zusicherungen sind Aussagen über den Zustand von Programmobjekten. Sie beschreiben Eigenschaften dieser Objekte, die zu bestimmten Zeitpunkten während der Ausführung des Programmes gelten müssen und sind entweder wahr oder falsch.
In der erweiterten Sprache JaWA können zusätzlich zu den Java-Anweisungen auch Zusicherungen in die Programme eingefügt werden. Z. B. könnte zu Beginn eines Methodenaufrufs von einer Parameter 'a' vom Typ Integer gefordert werden, daß sein Wert ungleich 0 ist. Diese Eigenschaft stellt eine Zusicherung dar und kann in JaWA durch eine require-Anweisung in den Quellcode der Methode aufgenommen werden:
/** require a!=0 **/
Ist in der Klasse eine Methode 'IsEven' formuliert, welche einen Integer-Wert übergeben bekommt und einen booleschen Wert zurückliefert, so könnte als zweite Bedingung gefordert werden, daß der Wert des Parameters 'a' gerade sein muß:
/** require a!=0; IsEven(a) **/
In diesem Zusammenhang sind auch verschachtelte Methodenaufrufe wie 'f(g(h(s)))' und qualifizierte Zugriffe über Referenzen wie 'a.f(x)' erlaubt. Jeder boolesche Ausdruck, der innerhalb eines Programms formuliert werden kann, kann auch als Zusicherung verwendet werden.
Wird zu einem Methodenaufruf einer Instanz eine Vor- und eine Nachbedingung formuliert, so entsteht eine Korrektheitsformel, wie sie in 1.2 Programmieren mit Vertrag beschrieben wurde. Auf der Basis einer operationellen Semantik können somit Aussagen zur Korrektheit der Software gemacht werden. Es werden jedoch vom JaWA-Präcompiler keine Beweise über dem Programmcode durchgeführt werden, sondern eine Übersetzung der Zusicherungen in Java-Anweisungen, welche die Einhaltung der angegebenen Bedingung zur Laufzeit prüfen.
Eine Zusicherung steht nie allein, sondern immer in einer der folgenden Anweisungen:
In Java gibt es eine neue Art von Kommentaren, die Dokumentationskommentare. Diese können von dem Werkzeug JavaDoc automatisch aus dem Quellcode extrahiert werden. Alle Zusicherungen, die Teil des Vertrages sind, werden deshalb als Dokumentationskommentar angegeben. Dies sind Vor- und Nachbedingungen zu Methoden und die Klasseninvariante. Die übrigen Zusicherungen in Schleifen und der check-Anweisung werden als normale Kommentare angegeben. Sie dienen zum Verständnis der eigenen Implementierung und sind nicht direkt Bestandteil des Vertrags.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Abstrakte Datentypen (ADT)
ADT's stellen ein geeignetes Werkzeug zur Modellierung von eigenständigen Softwaremoduln dar. Sie abstrahieren völlig von einer möglichen Realisierung, insbesondere auch von der Sprache, und beschreiben lediglich ein Verhalten einer Komponente. Sie ermöglichen die exakte Definition aller Eigenschaften, die eine Modul ausmachen, ohne das dieser durch Implementierungsfeinheiten überspezifiziert wird.
Wichtig im Rahmen des Konzeptes des Programmierens mit Vertrag ist, wie durch ADT's direkt die Entwicklung von Softwaremoduln unterstützt wird. Dazu wird eine Beschreibung benutzt, die in vier Abschnitte gegliedert. Sie sollen anhand eines Beispiels verdeutlicht werden. Das Beispiel beschreibt den ADT Stack, der einen Stapel über beliebige Elementen darstellt. Die Kapitel 2 werden die Spracherweiterungen ebenfalls an Methoden dieser Klasse erläutert:
Die vier Abschnitte des ADT Stack sollen nun genauer besprochen werden.ADT Stack[X]
TYPES
Stack[X] , X , BooleanFUNCTIONS
new : --> Stack[X] empty : Stack[X] --> Boolean push : X x Stack[X] --> Stack[X] pop : Stack[X] --> Stack[X] top : Stack[X] --> XPRECONDITIONS
Für alle s: Stack[X] gilt: pop : pre pop(s) = not empty(s) top : pre top(s) = not empty(s)AXIOMS
Für alle x: X und s: Stack[X] gilt: empty(new()) not empty(push(x,s)) top(push(x,s)) = x pop(push(x,s)) = s
Der Abschnitt TYPES
In diesem ersten Abschnitt wird der Name des ADT's festgelegt. Er ist gleichzeitig auch die Bezeichnung für die Menge, auf der der ADT durch die im folgenden Abschnitt definierten Funktionen operiert. Diese Menge wird Wertebereich des ADT genannt. Es dürfen weitere ADT's angegeben werden, die zur Definition benötigt werden.
Wenn die Struktur der Wertemenge nicht näher spezifiziert werden soll oder kann, so wird einfach nur ein Name angegeben. In diesem Zusammenhang wird auch Generizität unterstützt. Sie zeigt, daß ein ADT von einem weiteren abhängig ist und nur zusammen mit diesem sinnvoll beschrieben und eingesetzt werden kann. So wird im obigen Beispiel der ADT Stack als abhängig von einem weiteren ADT X spezifiziert. Es kann ein beliebiger ADT eingesetzt werden, der die Definitionen erfüllt, die zu X gemacht wurden. Da in diesem Fall keine Angaben existieren, ist jeder ADT möglich. So liefert Stack[Integer] einen Stapel für ganzzahlige Werte, Stack[Real] einen für reelle Zahlen und Stack[Quittungen] einen für Quittungen, wie auch immer diese letztlich aussehen mögen.
Der Abschnitt FUNCTIONS
Jede Funktion besitzt einen Definitionsbereich und einen Wertebereich. Das sogenannte Argument gibt das Element des Definitionsbereiches an, zu dem der entsprechende Wert des Wertebereichs geliefert werden soll. Zusammen mit dem Abschnitt 'TYPES' bilden sie die Signatur das ADT. In Zusammenhang mit Softwaremodulen spricht man von der Syntax des ADT.
Es ist wichtig, daß es sich hierbei um Funktionen im mathematischen Sinne handelt und nicht um eine Programmausführung. Ein Programm läuft ab und berechnet ein Ergebnis, aber eine Funktion, z. B. die Sinusfunktion, stellt einfach ihr Ergebnis zur Verfügung. Sie beschreibt den Zusammenhang zwischen zwei Werten innerhalb des Wertebereichs ihres Typs. Sie macht keine Angaben, wie sie zu diesem Ergebnis kommt, besitzt also auch keine Seiteneffekte, wie Programmroutinen diese haben können. Funktionen wie Sinus und Kosinus können sich gegenseitig nicht beeinflussen und bei veränderter Aufrufreihenfolge unterschiedliche Ergebnisse liefern.
Dieser Effekt ist gewünscht. Mit Blick auf das Ziel ergibt sich hier die Möglichkeit, einer mit Seiteneffekten behafteten Routine durch eine Funktion eine eindeutige Aufgabe zuzuordnen, ohne ihre Realisierung vorwegzunehmen. Bevor in den beiden folgenden Abschnitten 'PRECONDITIONS' und 'AXIOMS' gezeigt wird, wie die Semantik der Funktionen festgelegt wird, soll diese Idee noch ein wenig ausführlicher behandelt werden.
In der Definition der Funktion push taucht Stack zweimal auf. Auf der linken Seite wird der Stapel bezeichnet, auf den das Element gelegt werden soll und der der rechten Seite derjenige, der nach Anwendung der Funktion entstanden ist. Im mathematischen Sinne handelt es sich um zwei verschiedene Stapel, die lediglich durch eine Funktion zueinander in Beziehung gesetzt werden.
Wenn dieser ADT als Softwaremodul umgesetzt werden soll, so wird jeder Routine der Implementierung eine Funktion zugeordnet werden, um die Veränderung des jeweiligen Stapels durch den Aufruf zu beschreiben. Bei dieser Sichtweise handelt es sich nur um einen Stapel, der durch Dienste oder Operationen in Form von Programmroutinen verändert werden. Die erlaubten Veränderungen werden durch die assoziierten Funktionen eindeutig und nachweisbar definiert.
Wenn man das Programm vollständig durch ADT's definiert hat, kann jede Programmausführung als ein einziger großer verschachtelter Funktionsaufruf betrachtet werden, bei dem der Zustand, in dem das Programm gestartet wurde, zum Endzustand in Beziehung gesetzt ist.
Die Funktionen oder Dienste können in drei Arten gegliedert werden.
Konstruktorfunktionen
Zugriffsfunktionen
Transformationsfunktionen
Der Abschnitt PRECONDITIONS
Jede der Funktionen kann vollständig oder nur partiell definiert sein. Vollständig definierte Funktionen können immer aufgerufen werden und liefern stets ein Ergebnis.
Bei partiellen Funktionen ist dies nicht der Fall. Sie sind für bestimmte Argumente nicht definiert und liefern für diese kein oder ein beliebiges Ergebnis. Für diese Argumente darf die Funktion nicht aufgerufen werden. In diesem Abschnitt kann der Definitionsbereich von Funktionen eingeschränkt werden. So wird im obigen Beispiel vom Definitionsbereich für die Funktionen pop und top gefordert, daß sie nur für solche Stapel benutzt werden, für die die Funktion empty nicht gilt.
Der Abschnitt AXIOMS
Dieser Abschnitt stellt den wichtigsten Teil des ADT's dar. Zusammen mit den Vorbedingungen definiert er die Semantik der Funktionen und damit die Aufgaben der Routinen der späteren Implementierung. Er bildet somit die Basis für die Überprüfungen. Jede Eigenschaft, die den ADT ausmacht, wird hier als logische Aussage, z. B. in der Prädikatenlogik, formuliert.
Im Beispiel sind vier Aussagen genannt. Die erste beschreibt die Eigenschaft, daß jeder neu erzeugte Stapel anfänglich leer ist. Die zweite Aussage ergänzt, daß jeder Stapel, auf den durch push ein Wert gelegt wurde, nicht mehr leer sein kann. Die letzten beiden Aussagen beschreiben die last-in-first-out Eigenschaft, die einen Stack charakterisiert. Wenn auf einen Stapel ein Element x gelegt wurde und direkt danach top aufgerufen wird, so liefert top genau das Element x zurück. Das Element x befindet sich also an der Spitze des Stacks. Wird direkt nach dem Legen die Funktion pop aufgerufen, so befindet sich der Stapel wieder im Zustand, den er zuvor besaß.
Durch diese Beschreibung ist der ADT vollständig beschrieben. Jedes Objekt, welches durch die obigen Funktionen mit den spezifizierten Eigenschaften beschrieben werden kann, stellt einen Stapel dar. Beliebige weitere Eigenschaften dürfen vorhanden sein. Sie spielen in diesem Zusammenhang keine Rolle.
Man beachte, daß in keinster Weise vorgeschrieben wurde, wie die Funktionen realisiert werden können. Nicht einmal die Realisierung des ADT's im Ganzen wurde erwähnt. Es bleibt völlig offen, ob als Implementierungsidee z. B. ein Array oder eine verkettete Liste benutzt wird und ob diese Idee durch Hashfunktionen oder doppelte Verkettungen optimiert wird.
Wenn später der ADT durch mehrere Klassen implementiert wird, so kann zwischen diesen Klassen eine Abbildung angegeben werden, durch die jede Aussage über der einen Klasse in die andere Klasse übertragen wird. Mit den Begriffen des vorigen Abschnittes sind diese Klassen verschiedene Signaturen des abstrakten Datentyps Stack und die Abbildung ist der Isomorphismus zwischen ihnen.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Im vorangegangenen Abschnitt wurde immer nur vom Prüfen gesprochen. Was aber passiert, wenn eine Zusicherung verletzt ist? Die Antwort lautet: Es wird eine Ausnahme ausgelöst.
Eine solche Ausnahme kann dann abgefangen und entsprechend behandelt werden. In JaWA existiert ein besonderer Ausnahmemechanismus, der sich wesentlich von denen anderer Sprachen wie C++, Java oder Ada unterscheidet. In den letzteren kann eine Ausnahme wie eine `Goto'-Anweisung benutzt werden, um eine Methode an beliebiger Stelle zu verlassen und zum Aufrufer zurückzukehren. Diese Möglichkeit sind potentiell gefährlich, da mit ihnen das Abfangen von Fehlern umgangen werden kann.
Man stelle sich eine Klasse 'Limited Stack' vor, welche einen Stack von begrenzter Kapazität repräsentiert und als Array implementiert sei. Sie besitze eine Methode 'push', deren Implementierung sich auf die einer weiteren Methode 'setArrayField' abstützt. Wenn das Array voll ist und sich ein interner Zähler aus den Arraygrenzen herausbewegt, so löst 'setArrayField' eine Ausnahme aus, die von 'push' aufgefangen wird.
Der Entwickler von 'Limited Stack' möchte ein robustes und leicht zu benutzendes Modul. Daher ist es nicht abwegig, wenn er nach Auffangen der Ausnahme den Aufruf von 'push' beendet und in die Spezifikation mit hinein nimmt, daß 'push' nicht bei vollem Keller aufgerufen werden darf. Vielleicht sieht er die Rückgabe eines Fehlercodes vor. Ein solcher könnte vom Aufrufer geprüft werden, muß aber nicht.
Für die Benutzer entsteht hier eine gefährliche Fehlerquelle. Es können Elemente zur Laufzeit komplett verloren gehen, wenn bei der Überprüfung der Fehlercodes nachlässig gearbeitet wurde. Dies ist in der Praxis oftmals der Fall, da diese Prüfung nicht erzwungen wird. Gerade auch bei Teamarbeit entsteht hier eine weitere Gefahr. Wenn die Klasse schon in Benutzung ist, wird durch die veränderte Spezifikation, die nicht zum Handeln zwingt, möglicherweise ein Fehler in eine bereits bestehende Klassen durch die Hintertür hineingelassen.
Ein solches Verhalten ist nicht im Sinne des Programmierens mit Vertag. Für eine Methode sollte es genau zwei Möglichkeiten geben sich zu beenden:
Erfolg:
Scheitern:
Damit nun nicht jeder Fehler zum Beenden des gesamten Systems führt und um die im zweiten Punkt angesprochene Integrität der Klasse gewährleisten zu können, besitzt JaWA zwei weitere Sprachkonstrukte: Den rescue-Block und die retry-Anweisung.
Der rescue-Block kann am Ende des Methodenrumpfs angegeben werden. Tritt bei einer Ausführung der Methode eine Ausnahme auf, wird der Rumpf abrupt beendet und zum rescue-Block gesprungen. Hier kann der Entwickler Anweisungen vorsehen, damit die Integrität der Klasse gewahrt bleibt, z. B. könnte in einer Datenbank mit Transaktionskonzept die Konsistenz der Datenbank gesichert werden, indem bereits ausgeführte Schritte der Operation rückgängig gemacht werden. Die Ausnahme wird jedoch nicht gelöscht. Sie meldet das Scheitern dem Aufrufer.
Für weitere Flexibilität sorgt die retry-Anweisung. Mit ihr kann aus dem rescue-Block heraus die Ausführung des Methodenrumpfs erneut angestoßen werden. Wenn dieser Durchlauf alle für den Erfolg geforderten Bedingungen erfüllt, so konnte der Vertrag dennoch eingehalten werden. Für den Aufrufer ist das Wiederversuchen vollkommen unsichtbar, wenn man von der etwas längeren Ausführungszeit einmal absieht.
Somit tritt der Fall des Scheiterns des Methodenaufruf genau dann ein, wenn die Methode durch Beendigung des rescue-Blocks verlassen wird. Und der Fall des Erfolges tritt genau dann ein, wenn die Methode, möglicherweise nach einem Neubeginn mittels retry, durch Beendigung ihres Rumpfs verlassen wird.
Mit rescue und retry besitzt JaWA einen Ausnahmemechanismus, der die Fehler dort behandelt, wo sie Auftreten: in der Methode selbst. Sie können sich nicht fortpflanzen und an anderer Stelle Schaden anrichten. Es werden Fehler der oben beschriebenen Art vermieden, da die geänderte Spezifikation automatisch in die Überprüfung zur Laufzeit eingebunden ist.
Zum Seitenanfang
Zum Inhaltsverzeichnis
In diesem Kapitel werden die in JaWA möglichen Zusicherungen beschrieben. Die Beschreibung der Syntax erfolgt in Form von Grammatikregeln und jeweils an einem kurzen Beispiel aus einer Klasse 'Stack' für Stapel beliebiger Elemente. Die Semantik wird in Prosa erläutert.
Die Grammatikregeln sind in EBNF angegeben, wobei Terminalsymbole in 'Courier', Nichtterminale in 'Times' dargestellt sind. Alternativen sind durch '|' getrennt und nach Möglichkeit in eine eigene Zeile gesetzt. Optionale Angaben werden von eckigen Klammern '[ ]' umschlossen. Die Regeln für Zusicherungen werden der Einfachheit halber durchgängig als Dokumentationskommentare in '/**' und '**/' geschrieben. An ihrer Stelle können aber auch '/*' und '*/' verwendet werden. Es werden jedoch nur Dokumentationskommentare von dem Werkzeug 'JavaDoc' extrhiert.
Das Kapitel ist in die folgenden Abschnitte unterteilt:
Zum Seitenanfang
Zum Inhaltsverzeichnis
Zu jeder Methode einer Klasse in Java kann durch die JaWA-Erweiterungen, analog zu den Möglichkeiten in Eiffel, eine Vor- und eine Nachbedingung angegeben werden. Die Vorbedingung wird zu Beginn des Methodenrumpfs direkt hinter die öffnende geschweifte Klammer geschrieben, die Nachbedingung am Ende vor die schließende. Beide werden in Form von Dokumentationskommentaren angegeben.
Die Vorbedingung besteht aus dem Schlüsselwort 'require' und einer oder mehreren durch Semikolon getrennten, Zusicherungen. Die Zusicherungen sind, wie bereits in 1.4 Was sind Zusicherungen? erwähnt, boolesche Ausdrücke, wie sie auch im Methodenrumpf benutzt werden könnten. Es dürfen also alle Attribute der Klasse, Felder wie Methoden, und die aktuellen Parameter zum Erzeugen komplexer Ausdrücke verwendet werden.
Es können beliebig viele, durch Semikolon getrennte, Zusicherungen angegeben werden. Das Semikolon verbindet die Zusicherungen wie ein logisches 'and', so daß die gesamte Vorbedingung letztlich einen einzigen booleschen Ausdruck darstellt. Das Semikolon kann somit verwendet werden, um den Ausdruck in kleinere, übersichtlichere Teile zu zerlegen und, wenn gewünscht, jeden Teil mit einem eigenen Label zu versehen. Das Label wird dem Ausdruck vorangestellt, und ist von ihm durch einen Doppelpunkt getrennt.
Nachbedingungen werden nach denselben Regeln wie Vorbedingungen gebildet, nur daß sie mit dem Schlüsselwort 'ensure' beginnen. Sie bieten jedoch drei weitergehende Möglichkeiten: Zum ersten darf jedem Feld der Klasse das Präfix 'old_' vorangestellt werden. Es repräsentiert den Wert der Variablen vor dem Methodenaufruf. Z. B. kann durch eine Zusicherung wie 'i = old i' gefordert werden, daß sich der Wert von 'i' durch den Aufruf nicht ändern darf.
Die zweite Erweiterung ist das reservierte Wort 'nochange'. Es stellt einen booleschen Ausdruck dar, der genau dann wahr ist, wenn durch den Methodenaufruf kein Feld der Klasse verändert wurde. Es stellt damit eine Abkürzung bereit, die statt der expliziten Angabe der 'old'-Variante für jedes Feld der Klasse verwendet werden kann.
Die dritte Erweiterung betrifft den Rückgabewert von Funktionen. Er kann durch die Variable 'result' angesprochen werden, sofern die Methode nicht als 'void deklariert worden ist. Sie darf im Methodenrumpf und in der Nachbedingung benutzt werden.
Die folgenden Grammatikregeln beschreiben ihre syntaktische Form. Sie basieren auf der LALR1-Grammatik der offiziellen Java-Sprachspezifikation ([GJS97]). Ein großer Teil der hier angegebenen Regeln wird auch in den weiteren Abschnitten von den dort eingeführten Spracherweiterungen benutzt.
MethodBodyBlock:
{ [RequireClause] [BlockStatementList] [EnsureRescueClause] }
RequireClause:
/** require [BooleanAssertionList] **/
EnsureRescueClause:
/** EnsureClause RescueClause **/ /** **/
| /** EnsureClause **/
| /** RescueClause **/
EnsureClause:
ensure [NoChangeAssertionList]
NoChangeAssertionList:
NoChangeAssertion
| BooleanAssertion
| NoChangeAssertionList ; NoChangeAssertion
| NoChangeAssertionList ; BooleanAssertion
NoChangeAssertion:
nochange
BooleanAssertionList:
BooleanAssertion
| BooleanAssertionList ; BooleanAssertion
BooleanAssertion:
[AssertionLabel] BooleanExpression [{ MethodInvocation }]
BooleanExpression:
Expression
AssertionLabel:
Identifier :
Die Grammatikregeln beschreiben den Methodenrumpf, der nun neben einer Folge
von Anweisungen, die 'StatementList', auch eine Vor- und eine Nachbedingung
aufnehmen kann. Diese sind Dokumentationskommentare und enthalten eine Folge
von booleschen Zusicherungen. In der Nachbedingung ist auch das Schlüsselwort
'nochange' erlaubt. Label bestehen aus einem Bezeichner, der, durch
Doppelpunkt getrennt, einer booleschen Zusicherung vorangestellt wird. Die
etwas merkwürdige Behandlung der Nachbedingung wird zur Vermeidung von
Konflikten in der Grammatik benötigt. Die 'RescueClause' wird in
2.5 Der Rescue-Block: 'rescue' erläutert.
Das folgende Beispiel, und auch die weiteren, zeigen jeweils einen Ausschnitt
aus der Klasse 'Stack'. Vor- und Nachbedingungen werden an den
Methoden 'empty' und 'pop' beschrieben.
Um das Beispiel übersichtlich zu halten wurden Auslassungen gemacht und
durch '...' gekennzeichnet. Mit '
public class Stack {
private Linkable root;
private int nb_elements;
...
public boolean empty()
throws RuntimeCheck.AssertionException {
if (nb_elements==0)
return true;
else
return false;
/** ensure result==(nb_elements==0); nochange **/
}
public Value pop()
throws RuntimeCheck.AssertionException {
/** require !empty() **/
<Beginn des Methodenrumpfs>
return x;
/** ensure nb_elements == old_nb_elements-1 **/
}
...
}
Die in der Methode 'pop' angegebene Vorbedingung 'not empty'
drückt aus, daß diese Methode nur aufgerufen werden darf, wenn der Stapel
nicht leer ist. Dabei ist durch die Nachbedingung von 'empty'
sichergestellt, daß ihr Aufruf keine Veränderungen hervorruft.
Die Nachbedingung von 'pop' ihrerseits stellt sicher, daß sich durch
jeden Aufruf die Anzahl der Elemente um 1 verringert.
Wenn die Überprüfung zur Laufzeit eingeschaltet ist, so werden die Vor- und Nachbedingung bei jedem Aufruf der Methode 'pop' jeweils zu Beginn und Ende geprüft. Dies ist auch dann der Fall, wenn 'pop' innerhalb einer Zusicherung benutzt würde. Bei eingeschalteter Überprüfung kann sich der Entwickler also auf die Gültigkeit der Bedingung verlassen.
Ist eine der Zusicherungen verletzt, so wird je nach Übersetzungsmodus eine Ausnahme ausgelößt. In Java existieren zwei Arten von Ausnahmen, geprüfte und ungeprüfte. Erstere werden im Modus 'CheckedContract' benutzt. In Java muß eine solche geprüfte Ausnahmen in jedem Fall aufgefangen werden. Dies wird vom Java-Compiler bei der Übersetzung kontrolliert. Wenn in einer Methode eine geprüfte Ausnahme ausgelöst werden kann, so muß diese Anweisung von einem 'try-catch'-Block eingeschlossen sein oder durch eine 'throws'-Klausel im Methodenkopf an den Aufrufer weitergeleitet werden. Im obige Beispiel wurde dies getan. Das Beispiel kann daher in jedem der vier Übersetzungsmodi vom Compiler verarbeitet werden.
JaWA ist, wie Java, eine objektorientierte Sprache und unterstützt Vererbung und Polymorphismus. Es können Methoden dynamisch überschrieben werden. Man kann sich also nicht sicher sein, daß der Aufruf einer Methode auch wirklich diese ausführt. Ebenso könnte die Version einer erbenden Klasse ausgeführt werden. Der Vertrag, den man durch den Methodenaufruf abgeschlossen hat, muß aber in jedem Fall bestehen bleiben. Im Sinne der Korrektheitsformeln darf daher in der überschreibenden Methode die Vorbedingung nur abgeschwächt und die Nachbedingung nur verstärkt werden. Ist dies der Fall, so gilt der Vertrag auch dann, wenn dynamisch die neue Version ausgeführt wird.
Ob es sich bei Zusicherungen tatsächlich um eine Abgeschwächung oder Verstärkung handelt, kann allgemein nicht nachgewiesen werden. Für endliche Wertebereiche, wie sie für Variablen in Computer benutzt werden, ist eine Prüfung möglich, aber sehr aufwendig. In JaWA wird lediglich geprüft, ob Zusicherungen vorhanden sind: Wenn zu einer Methode keine Vor- bzw. Nachbedingung angegeben wurde, so wird vom JaWA-Präcompiler geprüft, ob in der Vererbungshierachie dieser Klasse ein Vorfahre existiert, der eine Methode mit gleicher Signatur besitzt. Wurde in dieser Methode eine Vor- bzw. Nachbedingung angegeben, so wird eine Fehlermeldung erzeugt und der Übersetzungvorgang abgebrochen..
Zum Seitenanfang
Zum Inhaltsverzeichnis
In jeder Klasse darf eine Klasseninvariante angegeben werden. Diese Invariante enthält Zusicherungen, die, bis auf Namen von Parametern, wie in den Vorbedingungen von Methoden definiert sein können. Die Klasseninvariante beginnt mit dem Schlüsselwort 'invariant' und wird wie eine Methode am Ende der Klasse angegeben.
In die Klasseninvariante sollten alle Zusicherungen aufgenommen werden, die Bedingungen enthalten, die für die gesamte Klasse und nicht nur für einzelne Methoden gelten. Z. B. kann mit ihrer Hilfe der durch die Felder definierte mögliche Zustandsraum eingeschränkt werden. Im Beispiel wird dies für das Feld 'nb\_elements' getan.
Man könnte die Invariante auch zu jeder Vor- und Nachbedingung explizit hinzuschreiben. Die Semantik wäre dieselbe, aber ihre Intention als invariante Bedingung über die gesamte Klasse wäre nur schlecht sichtbar. Außerdem werden Klasseninvarianten, im Gegensatz zu Vor- und Nachbedingungen, nicht vererbt.
Die Klasseninvariante wird am Schluß der Klasse wie eine Methode deklariert und an den Stellen in den übrigen Methoden aufgerufen, an denen sie geprüft werden soll. Auch sie enthält eine Folge von booleschen Zusicherungen, in der die Felder und Methoden der Klasse benutzt werden können. Lokale Variablen und Parameter können nicht verwendet werden. Die folgenden Grammatikregel beschreiben ihren syntaktischen Aufbau:
ClassBody:
{ [ClassBodyDecList] ClassInvariantClause }
ClassInvariantClause:
[InvariantClause]
InvariantClause:
/** invariant [BooleanAssertionList] **/
Wie aus den Regeln ersichtlich ist, kann in jeder Klasse höchstens
eine Klasseninvariante angegeben werden. Die Regel zur 'BooleanAssertionList'
wurde bereits in 2.1 Vor- und Nachbedingungen:
'require' und 'ensure' beschrieben.
Das folgende Beispiel zeigt die Invariante der Klasse Stack, welche eine einzelne Zusicherung enthält. Diese besagt, daß die Anzahl der Elemente, repräsentiert durch den Wert von 'nb_elements', nicht negativ werden kann. Die Methode 'pop' wird benutzt, um die Verwendung der Klasseninvarianten zu zeigen.
public class Stack {
private int nb_elements;
private Linkable root;
...
public Value pop()
throws RuntimeCheck.AssertionException {
/** require !empty() **/
<Beginn des Methodenrumpfs>
return x;
/** ensure nb_elements == old_nb_elements-1 **/
}
/** invariant nb_elements>=0 **/
}
Wenn die Überprüfung der Zusicherungen zur Laufzeit eingeschaltet ist, wird die Klasseninvariante durch logisches 'and' zur Vor- und Nachbedingung hinzugefügt und geprüft. Genauer: Bei jedem Methodenaufruf von außen, wird zu Beginn zusätzlich zur Vorbedingung auch die Klasseninvariante und am Schluß zusätzlich zur Nachbedingung ebenso die Klasseninvariante geprüft.
Der Begriff von außen steht hierbei für einen Aufruf, bei dem ein Kontrollfluß eine Instanz gewissermaßen betritt. Ein Beispiel soll dies verdeutlichen: Gegeben seien zwei Instanzen A und B von einer beliebigen, möglicherweise auch derselben, Klasse. Es wird eine Methode a1 der Instanz A aufgerufen, die ihrerseits eine Methode b der Instanz B aufruft. Und aus b wird wiederum eine Methode a2 der Instanz A aufgerufen. Die Aufrufe von a1 und b stellen jeweils einen Aufruf von außen dar, nicht aber a2, da der Kontrollfluß von A aus über B wieder zurück zu A verläuft. Somit wird die Klasseninvariante der Klasse zur Instanz A nur beim a1 und die Klasseninvariante der Klasse zur Instanz B bei b geprüft.
Bei Verwendung von Methoden innerhalb der Zusicherungen ist darauf zu achten, daß diese keine Kreisaufrufe entstehen lassen. Dies hätte einen Absturz des Systems zur Folge, da sie aus der unendlich tiefen Aufrufstruktur nicht zurückkehren würden. Man beachte, daß Kreise bei Tests auf jeden Fall gefunden werden, wenn jede Methode jeder Klasse mindestens einmal aufgerufen wird. Das sollte ein systematischer Test auf jeden Fall erfüllen. Es werden weder zum Zeitpunkt des Compilierens, noch zur Laufzeit Überprüfungen gemacht, ob die Zusicherungen sinnvoll sind.
Zum Seitenanfang
Zum Inhaltsverzeichnis
In Java existieren drei Arten von Schleifen. Sie wurden in JaWA analog durch Zusicherungen erweitert: Die Schleifen sind:
Da Schleifen nur innerhalb von Methoden benutzt werden können, sind sie ihre Zusicherungen nicht direkt Bestandteil der Dokumentation, sondern beschreiben die Implementierung. Sie leisten also sie keinen direkten Beitrag zum Vertrag zwischen Entwickler und Benutzer und sollten wie normale Kommentare formuliert.Dennoch besitzen sie eine wichtige Funktion. Sie können Eigenschaften der Implementierung zeigen, die nicht auf den ersten Blick aus dem Code ersichtlich sind, insbesondere kann die Terminierung für Schleifen gezeigt werden. Somit tragen sie zum Verständnis bei und helfen dem Entwickler, eine präzise Vor- und Nachbedingung oder auch Klasseninvariante zu formulieren.
Die bisher betrachteten Formen, Zusicherungen in den Programmcode einzubauen, gingen implizit davon aus, daß der Methodenaufruf terminiert, als irgendwann zum Aufrufer zurückkehrt. Diese Sichtweise ist korrekt, wenn von Schleifen abgesehen wird. Bei Schleifen muß die Terminierung explizit gezeigt werden, da sonst niemals die Nachbedingung geprüft würde und somit keine Garantien im Sinne eines Vertrages oder sogar in Form einer Korrektheitsformel gegeben werden könnte (siehe 1.2 Programmieren mit Vertrag).
In JaWA kann in einer Schleife eine Invariante und eine Variante angegeben werden. Wenn im folgenden eine Verwechslung mit der Klasseninvarianten nicht durch den Kontext ausgeschlossen ist, so wird von einer Schleifeninvarianten gesprochen. Die Invariante gibt eine Zusicherung an, die durch die Ausführung der Schleife nicht beeinflußt werden dar, während die Variante einen Integer-Ausdruck benennt, der dies ausdrücklich muß. Es sind zwei Bedingungen an die Variante geknüpft; Ersten muß der Wert ihres Ausdruck immer positiv sind und zweiten muß dieser Wert mit jedem Schleifendurchlauf abnehmen. Der JaWA-Präcompiler prüft diese Bedingungen und da beide Bedingungen nicht unendlich lang aufrecht zu erhalten sind, muß die Schleife terminieren.
Die Syntax der Invarianten ist dieselbe wie bei Klasseninvarianten. Nach dem Schlüsselwort 'invariant' können eine Menge von Zusicherungen, durch Semikolon getrennt, angegeben werden. Die Variante besteht aus dem Schlüsselwort 'variant' und einem Ausdruck, der einen Wert von Typ Integer liefert.
Es folgen nun die Grammatikregeln für die while-Schleife und für die angesprochenen Zusicherungen. Die Regeln der beiden Zusicherungen werden ebenfalls von den weiteren Schleifenarten benutzt.
WhileStatement:
while ( Expression ) AssertionClause
WhileStatementNoShortIf:
while ( Expression ) AssertionClauseNoShortIf
AssertionClause:
[InvariantClause] [VariantClause] Statement
AssertionClauseNoShortIf:
[InvariantClause] [VariantClause] StatementNoShortIf
InvariantClause:
/** invariant [BooleanAssertionList] **/
VariantClause:
/** variant IntegerExpression **/
Es werden in der Java-Grammatik der Sprachspezifikation zwei
Regeln für die while-Schleife benötigt, um das Dangling-Else-Problem
der if-then-else-Anweisung zu lösen (siehe
[GJS97] Seite 259).
In der Methode 'push' der Klasse 'Stack' wird eine while-Schleife benutzt, um die Liste der Stapelelemente zu durchlaufen:
public void push(Value x)
throws RuntimeCheck.AssertionException {
...
Linkable aktual=root;
int i=1;
while (i<nb_elements)
/* invariant nb_elements = old_nb_elements */
/* variant nb_elements-i */
{
<Beginn des Schleifenrumpfs>
i++;
};
...
}
Als Invariante wird die Anzahl der Elemente des Stapels benutzt. Sie darf
durch die Schleife nicht geändert werden. Die lokale Variable 'i'
zählt mit, so daß sich als Variante 'nb_elements-i' verwenden
läßt. Da durch die Klasseninvariante sichergestellt ist, daß
'nb_elements' nicht negativ ist und von der Schleife nicht verändert
wird, gilt mit der Initialisierung von 'i', daß der Wert der Variante
positiv ist. Im Schleifenrumpf wird 'i' immer um 1 erhöht, bleibt
aber dennoch kleiner 'nb_elements', da sonst die Abbruchbedingung
erfüllt wäre. Somit fällt der Wert der Variante mit jedem Schleifendurchlauf,
wird jedoch nie negativ, da vorher die Ausführung der Schleife beendet
wird. Die Terminierung ist damit gezeigt.
Die do-Schleife in Java ist der while-Schleife sehr ähnlich. Auch hier wird eine Abbruchbedingung angegeben. Jedoch wird diese Bedingung an das Ende der Schleife geschrieben. Die Schleife wird also in jedem Fall einmal durchlaufen. Die Grammatikregel für die do-Schleife lautet wie folgt:
DoStatement:
do AssertionClause while ( Expression ) ;
In der Beispielklasse 'Stack' wird keine do-Schleife verwendet. Deshalb soll
hier die while-Schleife der Methode 'push' in eine do-Schleife mit
ähnlicher Bedeutung dargestellt werden. Da die do-Schleife in jedem Fall
mindestens einmal Durchlaufen wird, wurde ihr eine bedingte Anweisung
vorangestellt. Die Invariante und die Variante bleiben unverändert. Die
Bedeutung ist nicht identisch, da im Falle einer nicht erfüllten Bedingung der
If-Anweisung die Invariante nicht geprüft wird. Für die an dieser Stelle
gemachten Aussagen ist dies jedoch nicht weiter von Bedeutung.
public void push(Value x)
throws RuntimeCheck.AssertionException {
...
Linkable aktual=root;
int i=1;
if !(i<nb_elements) {
do
/* invariant nb_elements = old_nb_elements */
/* variant nb_elements-i */
{
<Schleifenrumpf>
} while (i<nb_elements);
};
...
}
Die for-Schleife in Java wurde aus C++ übernommen. Sie besitzt drei durch Semikolon getrennte Ausdrücke im Schleifenkopf: die Initialisierung, die Abbruchbedingung und den Aktualisierer. Zunächst wird die Initialisierung ausgeführt. Dann beginnt die Ausführung der Schleife mit der Auswertung der Abbruchbedingung. Liefert sie 'true', so wird der Rumpf der Schleife und dann der Aktualisierer ausgeführt. Danach wird die Abbruchbedingung erneut geprüft. Liefert sie 'false', wird die Ausführung der Schleife beendet. Auch diese Schleife kann mit einer Invariante und einer Variante versehen werden:
ForStatement:
for ( ForInit ; Expression ; ForUpdate ) AssertionClause
ForStatement:
for ( ForInit ; Expression ; ForUpdate ) AssertionClauseNoShortIf ;
Auch für die for-Schleife werden zwei Regeln aufgrund des
Dangling-Else-Problems der if-then-else-Anweisung benötigt (siehe
\cite{GJS97} Seite 259).
Auch das Beispiel der for-Schleife stellt eine Umformung der while-Schleife aus der Methode 'push' dar. Die Anweisung zur Erhöhung der Variablen 'i' wurde aus dem ansonsten unveränderten Schleifenrumpf herausgenommen und als Aktualisierer in den Schleifenkopf eingefügt.
public void push(Value x) {
...
for (Linkable aktual=root,int i=1; i<nb_elements; i++)
/* invariant nb_elements = old_nb_elements */
/* variant nb_elements-i */
{
<Schleifenrumpf ohne die Anweisung 'i++;'>
};
...
}
Zum Seitenanfang
Zum Inhaltsverzeichnis
Die check-Anweisung wird benutzt, um an einer beliebigen Stelle im Programmcode des Methodenrumpfs eine Zusicherung anzugeben. Sie zeigt, daß an dieser Stelle die Gültigkeit der Bedingung erwartet wird, obwohl der Grund hierfür nicht direkt aus dem Programmcode ersichtlich ist.
Zum Beispiel möge an einer Stelle im Programmcode die Zuweisung 'x=y/z' vorkommen. Der Programmierer ist sich sicher, daß an dieser Stelle z immer einen Wert ungleich 0 hat. Daher möchte er es bewußt nicht prüfen. Eine solche Prüfung wäre überflüssig. Der Grund für einen Wert ungleich 0 liegt an einer anderen, entfernten Stelle im Code, möglicherweise sogar in einer anderen Methode.
Jemand anderes, der den Code durch schaut und den Grund nicht sofort erkennen kann, wird natürlich einen Fehler oder wenigstens Nachlässigkeit vermuten. Und auch der Programmierer selbst kann nicht immer alle Einzelheiten des gesamten Systems im Kopf haben und möchte an diese wichtige Eigenschaft erinnert werden. Mit der check-Anweisung wird sie explizit formuliert: 'check z!=0;'. Die check-Anweisung kann natürlich ebenfalls zur Laufzeit geprüft werden.
Man könnte statt der check-Anweisung auch einen Kommentar oder eine Anweisung, die zum Debuggen eingeschaltet werden kann, einfügen. Das Ergebnis wäre im letzteren Fall dasselbe. Die check-Anweisung sollte daher als eine kommentierende Debuganweisung aufgefaßt werden, bei der sich die Syntax an den bisherigen Anweisungen für die Vertragsmetapher anpaßt. Sie wird nach diesen Regeln gebildet:
Statement:
StatementWithoutTrailingSubstatement
| LabeledStatement
| IfThenStatement
| IfThenElseStatement
| WhileStatement
| ForStatement
| CheckStatement
| RetryStatement
CheckStatement:
/** check [BooleanAssertionList] **/
Als Beispiel soll hier eine Klasse dienen, in der u. a. eine Division
durchgeführt werden kann. Dazu besitzt die Klasse eine private Methode
'Div', welche von übrigen Methoden der Klasse aufgerufen wird und die
Division auf den Feldern x, y und z ausführt.
class Alpha {
int x,y,z
...
private void Div()
throws RuntimeCheck.AssertionException {
/* check z!=0 */
x=y/z;
}
...
}
Aus dem Zusammenhang, in dem 'Div' benutzt wird, sei klar, daß
hierbei der Divisor z immer ungleich 0 ist. Für jemanden, der die
Implementierung der Klasse nicht gut kennt, ist diese Information vielleicht
nur sehr schwer nachzuvollziehen, da sie über mehrere Methoden verteilt
ist. Deshalb wurde sie explizit durch die check-Anweisung formuliert.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Durch die Angabe eines rescue-Blocks kann im Fall einer verletzten Ausnahme die Integrität der jeweiligen Instanz gesichert werden. Eine ausführliche Beschreibung der Ziele ihres Einsatzes wird in 1.6 Vertragsverletzungen: Erfolg oder Scheitern gegeben. Sie wird von der Regel 'EnsureRescueClause' aus Abschnitt 2.1 Vor- und Nachbedingungen: 'require' und 'ensure' benutzt, also am Ende der Methode, hinter der Nachbedingung und vor der schließenden geschweiften Klammer. Sie besteht aus einer Folge von catch-Klauseln, welche jeweils einen Block mit Anweisungen besitzen.
RescueClause:
rescue [CatchList]
CatchList:
Catch
| CatchList ; Catch
Catch:
catch ( Expression ) Block ;
Die 'Expression' bezeichnet z. B. einen Ausdruck 'MyException
e', mit dem alle Ausnahmen vom Klassentyp 'MyException'
oder einer seiner Nachkommen aufgefangen werden kann. Die Anweisungen
im 'Block' werden daraufhin ausgeführt.
Als Beispiel soll wieder die in der Beschreibung der check-Anweisung benutzte Methode 'Div' dienen. Sie wurde um einen rescue-Block erweitert, die im Falle einer Ausnahme durch eine Verletzung der check-Anweisung das Feld x auf 0 setzt. Dies soll im Beispiel die die Integrität der jeweiligen Instanz der Klasse Alpha erhalten.
class Alpha {
int x,y,z
...
private void Div()
throws RuntimeCheck.AssertionException {
/* check z!=0 */
x=y/z;
/** rescue catch (RuntimeCheck.AssertionException e)
{x=0} **/
}
...
}
In Java muß jede Anweisung, die eine geprüfte
Ausnahme auslösen kann, von einem try-catch-finally-Block umschlossen
sein. Im try-Block wird sie ausgelöst und in
den catch-Klauseln wieder aufgefangen. Die catch-Klauseln werden vom
Programmierer im rescue-Block angegeben, der try-Block wird bei
entsprechendem Übersetzugsmodus vom
JaWA-Präcompiler erzeugt.
Jede catch-Klausel besitzt einen Parameter, unter dem die aufgefangenen Ausnahmeklassen in ihrem Block referenziert werden kann. Der Block der ersten zur Ausnahme passenden catch-Klausel wird ausgeführt. Der Java-Compiler stellt sicher, daß eine solche für jede Ausnahme, die im try-Block ausgelöst werden kann, existiert.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Mit den bisherigen Erweiterungen führt jede Verletzung einer Zusicherung zum Auslösen einer Ausnahme, die Methode für Methode, entsprechend der Aufrufreihenfolge, nach oben übergeben wird und letztlich zur Beendigung des Systems führt. Es soll aber auch ein Wiederaufsetzen ermöglicht werden, mit dem auf Fehler reagiert werden kann, indem durch einen erneuten Versuch versucht wird, das ursprüngliche Ziel des Methodenaufrufes zu erreicht.
In Abschnitt 1.6 Vertragsverletzungen: Erfolg oder Scheitern wurde die retry-Anweisung bereits besprochen, mit der dieses Wiederaufsetzen ermöglicht wird. Sie kann in JaWA nach folgender Regel wie eine normale Anweisung, allerdings nur innerhalb der Blöcke der catch-Klauseln, eingesetzt werden.
Statement:
StatementWithoutTrailingSubstatement
| LabeledStatement
| IfThenStatement
| IfThenElseStatement
| WhileStatement
| ForStatement
| CheckStatement
| RetryStatement
RetryStatement:
retry
Um die Anwendung der retry-Anweisung zu erläutern, wird das Beispiel der
Methode 'Div' ein weiteres Mal benutzt. Im Gegensatz zum Beispiel in
dem rescue-Block, wird hier der Wert des Divisors geändert und die Methode
erneut ausgeführt.
class Alpha {
int x,y,z
...
private void Div()
throws RuntimeCheck.AssertionException {
/* check z!=0 */
x=y/z;
/* rescue catch (RuntimeCheck.AssertionException e) {
z!=1; retry
}
*/
}
...
}
Der Methodenrumpf wird im Falle einer Verletzung der Zusicherung der
check-Anweisung durch die retry-Anweisung erneut unter geänderten Bedingungen
gestartet. Da lokale Variablen in Java innerhalb des Blockes selbst deklariert
werden, können geänderte Bedingungen zwischen zwei Durchläufen nur in Feldern
der Klasse gespeichert werden.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Jede Zusicherung, mit Ausnahme der Schleifenvariante, stellt einen booleschen Ausdruck darstellt, dessen Gültigkeit in einer bedingten Anweisung mit vorangestelltem Negationsoperator geprüft werden kann. Durch die Negation wird dann eine Ausnahme ausgelöst, wenn die zugesicherte Bedingung nicht gültig ist.
Die Vor- bzw. Nachbedingung wird jeweils zu Beginn bzw. am Ende eines jeden Methodenaufrufs geprüft. Wenn in der Nachbedingung eine Variable mit 'old' verwendet wird, so wird im Anschluß an die Vorbedingung eine lokale Variable erzeugt, welche den Wert zwischenspeichert. Bei Verwendung von 'nochange' geschieht dies für alle Attribute der Klasse, unabhängig davon, ob sie als 'privat', 'protected', 'public' oder ohne Modifizierer definiert sind.
Die Klasseninvariante wird zu einer neuen Methode übersetzt, die genau dann aus den Vor- und Nachbedingungen aufgerufen wird, wenn ein Aufruf von außen erfolgt (siehe Abschnitt 2.2 Die Klasseninvariante: 'invariant').
Dazu wird ein Aufrufzähler eingeführt, der innerhalb der Vorbedingung um 1 erhöht und innerhalb der Nachbedingung wieder um 1 verringert wird. Besitzt der Vorfahre einer Klasse eine Klasseninvariante, so wird diese ebenfalls aufgerufen.
Bei Schleifen wird die Invariante zu Beginn eines jeden Durchlaufs und direkt hinter ihr durch eine bedingte Anweisung geprüft. Für die Variante wird eine lokale Variable erzeugt, welche den Wert zu Beginn eines Durchlaufs zwischenspeichert, so daß am Ende geprüft werden kann, ob ihr Wert gefallen und immer noch positiv ist. Die check-Anweisung wird lokal wie ein Makro expandiert. Aus ihr wird direkt eine bedingte Anweisung zur Prüfung ihrer Zusicherung erzeugt.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Durch die Spracherweiterungen ergeben sich ein paar Einschränkungen für die Entwicklung der eigenen Programme. Diese gliedern sich in:
Zum Seitenanfang
Zum Inhaltsverzeichnis
Durch die Spracherweiterungen sind die Schlüsselwörter 'require', 'ensure', 'invariant', 'variant', 'check' und 'nochange' zur Grammatik hinzugefügt worden. Obwohl an dieser Stelle keine Probleme erwartet werden, sollten sie nicht als Bezeichner benutzt werden. Als erstes Wort am Anfang von Dokumentationskommentaren und normalen Kommentaren dürfen sie aber auf keinen Fall auftauchen, da sie sonst als Zusicherungen interpretiert und geparst würden.
In den Methoden werden je nach Zusicherungen folgende lokale Variablen benutzt:
Auf die vom Präcompiler hinzugefügten Felder und lokalen Variablen sollte nur durch die von ihm erzeugten Anweisungen zugegriffen werden. Ihre Benutzung im eigentlichen Programm ist nicht vorgesehen, kann jedoch nicht verhindert werden. Eine solche Benutzung kann die Bedeutung der Zusicherungen außer Kraft setzen. So würde durch eine nicht vorgesehene Veränderung des Feldes 'depthOfCall' die Prüfung der Klasseninvarianten zu völlig falschen Zeitpunkten durchgeführt. Sie würde damit ihre Aussagekraft verlieren und sinnlose Ausnahmen erzeugen.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Im Gegensatz zu Eiffel, wird in dem für Java entwickelten Ansatz nur bei Methodenaufrufen die Klasseninvariante geprüft, und nicht auch beim Zugriff auf öffentliche Variablen. Ein solcher Zugriff erfolgt ebenfalls von außen und müßte zur Prüfung der Klasseninvarianten führen. Eine solche Umsetzung durch einen Präcompiler wäre allerdings sehr aufwendig, da jeder einfache Variablenzugriff durch einen Methodenaufruf ersetzt werden müßte.
Deshalb soll hier ein Weg vorgeschlagen werden, der als Kompromiß beide Aspekte berücksichtigt. Attribute, bei denen durch eine Wertzuweisung eine Verletzung der Invarianten auftreten kann, werden als kritisch betrachtet und sollten als nichtöffentlich deklariert werden. Sie würden das Prinzip der Datenkapselung verletzen. Ihr Zugriff sollte immer über eine Methode gekapselt werden. Die unkritischen Attribute können zur Steigerung der Effizienz öffentlich bleiben. Dies gilt auch für Felder, die als Klassenattribute deklariert wurden, da sie nur einmal für alle Instanzen einer Klasse angelegt werden. Auch hier könnte eine Instanz die Invariante einer weiteren verletzen.
Das Feld 'depthOfCall' als Zähler für die Aufruftiefe ist vom Typ Integer deklariert. Die maximale Aufruftiefe ist somit durch den Wertebereich 'Integer' beschränkt. Dies gilt auch für die Anzahl der Schleifen innerhalb eines Methodenrumpfs, da die lokale Variable 'variant' zur Unterscheidung durchnumeriert wird.
Der rescue-Block und die Retry-Anweisung können benutzt werden, um durch einen erneuten Versuch die Erfüllung der Nachbedingung inklusive der Klasseninvarianten zu erreichen. Sie können aber auch mißbraucht werden, indem sie die Werte von Feldern oder den Rückgabewert in einer solchen Weise ändern, die nicht den erwarteten Ergebnissen entspricht. In Abschnitt 2.6 Die Retry-Anweisung wurde dies für die Methode 'Div' getan. Dadurch wurde aber die eigentliche Berechnung umgangen. Die Methode konnte zwar erfolgreich beendet werden, liefert nun aber einen Wert, der nichts mit dem eigentlichen Ergebnis der Berechnung zu tun hat. Es muß vom Entwickler selbst darauf geachtet werden, daß er nicht den Sinn der Spracherweiterungen umgeht.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Zur Beschreibung der Installation existiert eine eigene Datei names 'Install.txt' im übergeordnetem Verzeichnis.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Als Einstieg in die systematische Entwicklung von Klassen unter Verwendung der Vertragsmethaper soll eine Fallstudie zur Entwicklung einer Klasse für verkettete Listen dienen. In diesem Zusammenhang werden auch Details von Java und die Benutzung des JaWA-Präcompilers beschrieben. Der Vorgang ist in drei Schritte gegliedert:
Der erste Schritt bildet die Basis. Hier wird versucht, eine möglichst reine und von der Implementierungsidee unabhängige Beschreibung der Klasse zu erreichen. Diese Beschreibung sollte über die momentanen Bedürfnisse hinausgehen und eine allgemeine und wiederverwendbare Lösung des Problems darstellen. Für unser Beispiel der verketteten Liste bedeutet dies, daß beliebige Elemente in die Liste aufgenommen werden können und allgemeine Dienste wie 'Einfügen' und 'Löschen' vorhanden sind. Da Listen sehr allgemein sind, können hier nur wenige Vorbedingungen und Axiome formuliert werden. Der ADT wird 'List' genannt. Die Datenobjekte werden durch die Menge 'Value' dargestellt.
ADT List
TYPES
List, Value, BooleanFUNCTIONS
new : ---> List empty : List ---> Boolean insert : Value x List ---> List delete : List -/-> ListPRECONDITIONS
Für alle l:List gilt: delete : pre delete(l) = not empty(l)AXIOMS
Für alle v: Value und l:List gilt: empty(new()) not empty(insert(v,l))
Der zweite Schritt versucht diesen ADT durch eine Klasse zu beschreiben. Diese Klasse wird ebenfalls mit 'List' bezeichnet (Für ADT's und deren Funktionen wird eine 'kursive' Schrift verwendet, für Klassen und ihre Feldern und Methoden eine 'nicht proportionale'). Es kommen hier die Aspekte der 'Darstellung' und der 'aktiven Maschine' hinzu. Für die Darstellung soll eine weitere Klasse 'Linkable' benutzt werden. Sie stellt Listenelemente zur Verfügung, die jeweils ein Datenobjekt und eine Referenz auf das nachfolgende Listenelement aufnehmen können. Eine Liste stellt also eine Verkettung von Listenelemente dar, deren Wurzel in der Instanz von 'List' gespeichert wird. Zur Darstellung der Datenobjekte wird der ADT 'Value' als Schnittstelle 'Value' definiert. Beide Klassen und die Schnittstelle werden in das Paket 'DataContainer' eingefügt.
Der Aspekt der aktiven Maschine wird durch einen Cursor realisiert. Die Instanzen merken sich in ihm die aktuelle Arbeitsposition. An dieser Position werden dann Elemente eingefügt oder gelöscht. Ein Cursor ermöglicht Methoden mit wenigen Parametern und eine sehr effiziente Implementierung. Wenn z.B. in der Mitte der Liste mehrere Elemente hintereinander gelöscht werden, so muß nicht für jedes Element die Liste erneut bis zur entsprechenden Position durchlaufen werden. Auch lassen sich Suchoperationen wie 'FindFirst' und 'FindNext' implementieren, die ohne internen Zustand überhaupt nicht möglich wären.
Es sollte sich schon an dieser Stelle für einen Ubersetzugsmodus entschieden werden, da im Modus 'Contract' in den Köpfen der Methoden alle Ausnahmen angegeben werden müssen, die in ihren Rümpfen ausgelöst werden können.
Das nun folgende Listing zeigt einen Ausschnitt aus der Klasse 'List', welche im Verzeichniss 'DataContiner' in der Datei 'List.JaWA' gespeichert ist. Sie wird vom Präcompiler in die Datei 'List.java' übersetzt, die dann nur noch Java-Anweisungen enthält. Der Java-Compiler erzeugt hieraus die Datei 'List.class'.
Die meisten Methoden und Zusicherungen wurden erst durch die Darstellung in die Klasse aufgenommen und sind nicht Bestandteil des ADT. Die im ADT zur Funktion 'delete' angegeben Vorbedingung wird in der Methode 'Delete' verwendet. Das erste Axiom des ADT's wird implizit im Konstruktor verwendet, das zweite in der Nachbedingung der Methode 'Insert'.
package DataContainer;
public class List {
private Linkable root;
private Linkable cursor;
private int pos;
private int nb_elements;
public boolean IsEmpty()
throws RuntimeCheck.AssertionException {
return (nb_elements == 0);
/** ensure result == (nb_elements==0); nochange **/
}
public void GoToFirstElement()
throws RuntimeCheck.AssertionException {
/** require !IsEmpty() **/
...
/** ensure nb_elements==old_nb_elements **/
}
public void GoToNextElement()
throws RuntimeCheck.AssertionException {
/** require !IsEmpty() **/
...
/** ensure nb_elements==old_nb_elements **/
}
public void GoToLastElement()
throws RuntimeCheck.AssertionException {
/** require !IsEmpty() **/
...
/** ensure nb_elements==old_nb_elements;
cursor.GetNext()==root
**/
}
public void GoToPrevElement()
throws RuntimeCheck.AssertionException {
/** require !IsEmpty() **/
...
/** ensure nb_elements==old_nb_elements **/
}
public void Insert( Value value )
throws RuntimeCheck.AssertionException {
/** require value!=null **/
...
/** ensure !IsEmpty() **/
}
public void Delete()
throws RuntimeCheck.AssertionException {
/** require !IsEmpty() **/
...
/** nb_elements==old_nb_elements -1 **/
}
/** invariant 0<=pos; pos<=nb_elements;
pos==GetPosition(cursor);
cursor==null | pos!=0 ;
**/
}
Nachdem die Klasse beschrieben und alle Methoden implementiert wurden, folgt
im dritten Schritt die Übersetzung. Wie bereits erwähnt, soll der
Übersetzungsmodus 'Contract' benutzt werden. Deshalb
müssen Aufrufe von Methoden der Klasse 'List' von einer
try-catch-Anweisung umschlossen sein.
Um die Klasse 'List' zu benutzen, wurde das folgende kleine Beispiel
definiert, welches ein ausführbares Javaprogramm darstellt. Die Klasse
'X' implementiert die Schnittstelle 'Value'.
package DataContainer;
class X implements Value {}
public class TestList {
static List l;
public static void main(String[] argv) {
try {
l = new List();
x= new X();
l.InsertAfter(x);
} catch (RuntimeCheck.AssertionException e)
{System.out.print("ERROR");}
}
}
Ist der Präcompiler installiert, so kann die Übersetzung der Klasse 'List' durch den Befehl:
JaWA DataContainer/List.JaWAgestartet werden. Danach wird das Testprogramm durch den Befehl:
JaWA DataContainer/TestList.JaWAübersetzt. Da es keine Zusicherungen enthält, hätte an dieser Stelle auch der normale Java-Compiler benutzt werden können. Der Befehl:
java DataContainer.TestListstartet die Java-Virtual-Maschine, die die Klassen lädt und das Programm ausführt.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Die Überprüfung der Zusicherungen zur Laufzeit ermöglicht das Finden und Lokalisieren von Fehlern in der eigenen Software. Dafür wird aber, je nachdem wie intensiv mit Zusicherungen gearbeitet wurde, einige Zeit und auch etwas Speicherplatz benötigt. Wenn die Effizienz im Vordergrund steht, ist das ärgerlich und nicht akzeptabel. Aber zum Zweck der Effizienz auf die Vorteile des Programmierens mit Vertrag, wie Debugging und rescue-Blöcke etc., zu verzichten, ist ebenso ärgerlich.
So wie der Eiffel-Compiler versucht, praktisch einsetzbare Softwaresysteme zu generieren, gilt dies auch für den JaWA-Präcompiler. Deshalb wurden die im Eiffel-Compiler verwendbaren Optionen zur Auswahl der zu überprüfenden Zusicherungen auf den JaWA-Präcompiler übertragen. Es sind drei Modi auswählbar:
Zum Seitenanfang
Zum Inhaltsverzeichnis
Im Modus All findet die Überprüfung für alle im Programm angegebenen Zusicherungen statt. Bei ihrer Verletzung werden Ausnahmen erzeugt und die Kontrolle springt zum Rescue-Block, oder, falls ein solcher nicht vorhanden ist, zum Aufrufer. Eine geprüfte Ausnahme muß, eine ungeprüfte kann aufgefangen werden.
Zu Beginn der Entwicklung sollte der Modus All verwendet werden, um Fehler, sowohl konzeptioneller, als auch implementationstechnischer Art, so früh wie möglich zu entdecken. Wenn man sich nach einer gründlichen Testphase sicher ist, daß keine oder nur noch wenige Fehler vorhanden sind, kann man den Umfang der Überprüfungen durch einen der übrigen Modi einschränken und eine effizientere Ausführung erreichen.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Im Modus Preconditions werden nur die Vorbedingungen der Methodenaufrufe geprüft und lösen Ausnahmen aus. Wenn geringe Einbußen (ca. 20%) bei der Laufzeit hingenommen werden können, so sollte die Option Preconditions verwendet werden. Sie stellt einen Kompromiß zwischen Effizienz und Sicherheit dar, bei dem nur die Vorbedingungen der Methoden, jeweils ohne den Teil der Invarianten, geprüft werden. Wenn man sich sicher ist, daß die eigene Klasse korrekt arbeitet, aber prüfen möchte, ob der spätere Benutzer auch die Vorbedingung einhält, so kann diese Option das bei einem nur geringfügigem Mehr an Laufzeit und Speicherplatz leisten.
Zum Seitenanfang
Zum Inhaltsverzeichnis
In Modus Nothing ist die Überprüfung der Zusicherungen zur Laufzeit komplett ausgeschaltet. Somit können die Zusicherungen nicht mehr als Garantien betrachtet werden. Falls es zu einer Verletzung der Zusicherungen käme, würde diese nicht entdeckt und könnte weitreichende Folgen haben, so wie sie ohne Zusicherungen möglich sind. Sowohl der Verlust der Integrität des Systems als auch ein Absturz wären möglich.
Das Beispiel zur check-Anweisung in Abschnitt 2.4 Die Check-Anweisung verdeutlicht die möglichen Folgen. Die Zusicherung garantiert für z einen Wert ungleich 0. Findet diese Prüfung nicht statt, so kann die Benutzung von z in der folgenden Division einen Laufzeitfehler produzieren, der in einem Absturz des Systems enden kann. Für leere Referenzen gilt dasselbe.
Man sollte also wirklich sicher sein, daß das System seine Aufgabe fehlerfrei erfüllt, wenn man die Option Nothing wählt.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Der Umstieg auf das neue Konzept erfordert einige Änderungen für die Sichtweise der Entwicklung von Softwaresystemen. Er sollte daher langsam und schrittweise möglich sein. Zu diesem Zweck wurden vier verschiedene Übersetzungsmodi eingebaut, mit denen der Entwickler den Grad und Umfang der Benutzung des Konzeptes abstufen kann. Dies ist auch dort interessant, wo das Konzept nachträglich in bereits bestehende Systeme aufgenommen werden soll. Die Übersetzungsmodi dienen nicht der Effizienzsteigerung, wie die Überprüfungsmodi, sondern dem schrittweisen Einstieg in den Umgang mit Zusicherungen und dem Präcompiler. Die Modi im Überblick:
Zum Seitenanfang
Zum Inhaltsverzeichnis
Der Übersetzungsmodus Nothing stellt den ersten Modus dar. Er ermöglicht das Hinzufügen von Zusicherungen als Kommentare und hat keinen Einfluß auf das Verhalten des Systems. Mit diesem Modus sollen die ersten beiden Ziele des Programmierens mit Vertrag ermöglicht werden, eine formale Spezifikation und ihr automatisches Einfließen in die Dokumentation.
Obwohl dieser Modus keinerlei Änderungen an einem System hervorruft und daher auch problemlos in bereits entwickelte und eingesetzte Systemen nachträglich eingefügt werden kann, stellt er doch den größten Schritt auf dem Weg zum neuen Konzept dar, nämlich den methodischen Wechsel. Mit diesem Modus soll das Sammeln von Erfahrungen mit der formalen Beschreibung von Objekten durch ADT's ermöglicht werden, ohne das ein verändertes Verhalten bezüglich der Implementierung vom Benutzer gefordert wird. Die Umstellung wird somit hoffentlich nicht zu groß.
Gleichzeitig stellt dieser Modus eine Sicherheit dar. Wenn Programme grundsätzlich nicht fehlerfrei sind, so ist es auch der JaWA-Präcompiler nicht. Damit es an dieser Stelle nicht zu Problemen kommen kann, ist es mit diesem Modus auf einfache und schnelle Weise möglich, den Präcompiler auszuschalten, ohne aufwendig Makefiles verändern und die Namen der Quelldateien von Hand in 'name.java' umbenennen zu müssen.
Dieser Modus sollte nicht benutzt werden, wenn Effizienz bei der Ausführung gefordert ist, da bei diesem Modus die Übersetzung ausgeschaltet ist. Somit würden auch eventuell vorhandene rescue-Blöcke nicht übersetzt. Diese können aber auch für Ausnahmen benutzt werden, die nicht durch Zusicherungen ausgelöst wurden. Für eine höhere Effizienz sollen die Überpruefungsmodi 'Nothing' oder 'Precondition' benutzt werden. Dies sollte natürlich erst am Ende einer gründlichen Testphase geschehen, wenn der Entwickler sicher ist, daß das System seine Aufgaben erfüllt.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Mit dem Modus Warning wird es möglich, die gemachten Zusicherungen zur Laufzeit überprüfen zu lassen. Dieser Modus erweitert den ersten also um die Debugging-Funktionalitäten. Der Kontrollfluß des Programms wird nicht verändert, sondern eine Instanz der in der Konfigurationsdatei unter 'WarningClass' angegebenen Klasse erzeugt und ihre Methode 'Message' aufgerufen. Diese Klasse stellt keine Ausnahme dar. Dieser Modus soll helfen, die im ersten Schritt geleistete Arbeit der formalen Spezifikation prüfbar zu machen.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Die nächste Stufe stellt der Modus UncheckedContrakt dar. Mit diesem Modus erfolgt die Übersetzung der Zusicherungen, so daß bei ihrer Verletzung Ausnahmen ausgelöst werden. Es wird jedoch eine ungeprüfte Ausnahme verwendet. Eine solche Ausnahme kann aufgefangen werden, muß aber nicht. Da eine nicht aufgefangene Ausnahme zur Beendung des Systems führt, muß der Entwickler sehr genau darauf achten, daß an dieser Stelle in seinem System keine Probleme auftreten können.
Es erfolgt in diesem Modus die Anbindung an den Ausnahmemechanismus und es wird Software-Fehlertoleranz ermöglicht. Bis zu diesem Modus ist ein Wechsel zwischen den Modi ohne größeren Aufwand möglich und kann somit problemlos auch in bereits bestehende Projekte nachträglich aufgenommen werden.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Der Modus Contrakt arbeitet wie der vorhergehende, nur mit geprüften Ausnahmen. Damit stellt er den Vertrag zwischen Benutzer und Entwickler her. Jede Anweisung, die eine geprüfte Ausnahme auswerfen kann, muß von einem try-Block umschlossen sein. Jede Methode die eine geprüfte Ausnahme weiterleitet, muß diese in ihrem Kopf deklarieren. Da der Präcompiler die Schnittstelle einer Klasse nicht verändern soll, muß dies vom Entwickler selbst eingefügt werden. Ein Wechsel zu diesem Modus ist daher mit Änderungen in den Klassendeklarationen und auch in den Programmen, die ihre Methoden aufrufen, verbunden. Dennoch sollte dieser Modus das Ziel bei der Benutzung von Zusicherungen sein, da erst hier vom Programmieren mit Vertrag gesprochen werden kann.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Aus dem JaWA-Präcompiler heraus wird der eigentliche Java-Compiler aufgerufen, um die semantische Korrektheit der Zwischenform 'Check' zu prüfen und die JaWA-Spracherweiterungen zu übersetzen. Beide Werkzeuge müssen konfigurierbar sein. Daher werden alle Parameter, die beim Aufruf des JaWA-Präcompilers angegeben wurden, an den Java-Compiler weitergereicht. Somit läßt sich dieser weiterhin einstellen.
Einstellungen am JaWA-Präcompiler werden in einer Konfigurationsdatei namens 'JaWA.rc' angegeben. Der JaWA-Präcompiler sucht zunächst im aktuellen Verzeichnis nach dieser Datei. Ist hier keine vorhanden, sucht er im Homeverzeichnis des Benutzers. Liegt auch hier keine, so werden die Default-Einstellungen für die Optionen benutzt.
In der folgenden Aufstellung sind alle Optionen mit den jeweils möglichen Werten genannt. Diese Werte sind durch Komma getrennt und die Default-Einstellung ist 'kursiv' gedruckt. Wenn eine beliebige Zeichenfolge angegeben werden darf, so wurde '...' geschrieben:
VerboseMode = on , off
Logfile = ./JaWA.log , ...
CheckMode = Nothing , Preconditions , All
TranslationMode = Nothing , Warning,
UncheckedContrakt, Contract
ExceptionClass = RuntimeCheck.AssertionException , ...
RuntimeExceptionClass = RuntimeCheck.AssertionRuntimeException , ...
WarningClass = RuntimeCheck.Warning , ...
Ist der VerboseMode eingeschaltet, so werden Kontrollausgaben
erzeugt, mit denen die Ausführung des JaWA-Präcompilers nachvollzogen
werden kann. Dieser Modus ist nicht für das Debuggen des Präcompilers
gedacht, sondern dient der Kontrolle, ob und welche Konfigurationsdatei benutzt
wurde und an welcher Stelle sich der Übersetzungsvorgang befindet.
Wird ein Logfile angegeben, so werden Debug- und Verboseausgaben in die entsprechende Datei geleitet, sonst zur Standardausgabe. Der Normalfall ist die Erzeugung der Datei 'JaWA.log' im aktuellen Verzeichnis.
Welche Zusicherungen überprüft werden sollen, wird durch den Überpruefungsmodus CheckMode definiert.
Der Übersetzungsmodus TranslationMode definiert die Art, in der die Zusicherungen behandelt werden.
In ExceptionClass kann die im Übersetzungsmodus 'Contract' zu benutzende Klasse für geprüfte Ausnahmen angegeben werden. Dies kann somit auch eine eigene, erweiterte Klasse sein, welche z.B. in einer graphischen Umgebung die Fehlermeldung in einem eigenen Fenster erscheinen läßt oder sie in einer Datenbank speichert. Die hier angegebene Klasse muß dazu von der Klasse 'AssertionException' aus dem Paket 'RuntimeCheck' erben.
In RuntimeExceptionClass kann die im Übersetzungsmodus 'Contract' zu benutzende Klasse für ungeprüfte Ausnahmen angegeben werden. Sie muß ein Nachkomme von der Klasse 'AssertionRuntimeException' aus dem Paket 'RuntimeCheck' sein.
In WaringClass kann die im Übersetzungsmodus 'Warning' zu benutzende Klasse für die Ausgabe von Informationen zu verletzten Zusicherungen angegeben werden. Sie muß von der Klasse 'Warning' aus dem Paket 'RuntimeCheck' erben.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Die folgende Aufstellung zeigt die vom JaWA-Präcompiler generierten Fehlermeldungen, unterteilt in Fehler während der Übersetzung und währen der Ausführung des JaWA-Programms:
Zum Seitenanfang
Zum Inhaltsverzeichnis
Die folgende Aufstellung zeit alle Fehlermeldungen des Präcompilers. Wenn in den Meldungen Alternativen möglich sind, so wurden diese durch Komma getrennt in Klammern gesetzt.
Zum Seitenanfang
Zum Inhaltsverzeichnis
Die folgende Aufstellung zeit alle Laufzeit-Fehlermeldungen. Sie werden durch die in der Konfigurationsdatei angegebenen Klassen bestimmt. Werden die Default-Einstellungen benutzt, so wird, analog zu Fehlermeldungen des Java-Compilers, folgende zweizeilige Meldung ausgegeben:
" 'filename':'line': 'message' in class 'c' method 'm'
'filename':'line': 'label' 'assertion' "
wobei 'filename' den Namen der Quelldatei, 'line' die Zeilennummer, 'c' den Namen der Klasse, 'm' den Namen der Methode, 'label' das optionale Label der Zusicherung, 'assertion' die Zusicherung selbst und 'message' für eine der folgenden Meldungen steht:
Zum Seitenanfang
Zum Inhaltsverzeichnis
An dieser Stelle werden einige Hinweise zu weiterführenden Informationsquellen gegeben.
LINKS:
Literatur: