<< zurück

MBSE Home

weiter >>

3.4 Funktionen in OCL

Bisher wurden nur OCL-Invarianten definiert, die eine Eigenschaft über einen Systemzustand bestehend aus einer Sammlung von Objekten charakterisierten. Dabei wurden vordefinierte Methoden der OCL zur Bearbeitung von Container-Datenstrukturen verwendet. Während OCL einerseits außerhalb des let-Konstrukts keine eigenen Funktionen beziehungsweise Methoden definieren kann, ist OCL andererseits doch hervorragend geeignet, mithilfe von Paaren aus Vor- und Nachbedingung die Effekte von Methoden des zugrunde liegenden Modells zu spezifizieren. Umgekehrt kann auch das Modell Methoden für die Spezifikation von OCL-Bedingungen zur Verfügung stellen.²⁰

Die Spezifikation von Methoden durch Vor-/Nachbedingungspaare entspricht der von [Mey97] propagierten Spezifikation von Verhalten mit Contracts. Diese Vorgehensweise wird in [PH97] auf Basis einer eigenständigen Kernsprache namens „Aicken“ verfeinert und eine auch Seiteneffekte einbeziehende Theorie dafür gebildet. [MMPH99, MPH00] transferiert Teile dieser Ergebnisse auf Java. Die dort verwendeten „Observer“-Funktionen entsprechen den nachfolgend eingeführten Queries, erlauben aber nicht die Erzeugung neuer Objekte.

3.4.1 Queries

In den bisher formulierten Bedingungen wurden meist von der OCL selbst angebotene Funktionen verwendet. An vielen Stellen ist es jedoch hilfreich, auf die von der Implementierung zur Verfügung gestellten Methoden zuzugreifen, um eine Bedingung kompakt zu formulieren. Eine solche Methode wird Query genannt und wird durch den Stereotyp ≪query≫ gekennzeichnet. Als Erweiterung des Klassendiagramms in Abbildung 3.8 wird eine detaillierte Beschreibung der Message-Struktur in Abbildung 3.20 beschrieben. Sie enthält unter anderem zwei Query-Methoden.

Diese Queries erlauben die Selektion der einer spezifischen Auktion zugeordneten Menge von Nachrichten. Diese kann dann mit den in einer Auktion enthaltenen Nachrichten verglichen und so sichergestellt werden, dass die zu einer Auktion entstandenen Nachrichten in korrekter Form und Reihenfolge an die Teilnehmer einer Auktion weitergeleitet werden.

Aufgrund der gewählten zweiwertigen Logik ist es allerdings möglich, dies kürzer zu formulieren, wenn davon ausgegangen wird, dass der Aufruf getAuction() einen undefinierten Wert oder null liefert, falls die Nachricht nicht auktionsspezifisch ist:

Wie die Beschreibung des Stereotyps ≪query≫ in Tabelle 3.21 erläutert, ist es eine wesentliche Eigenschaft von Queries, die zugrunde liegende Objektstruktur nicht zu modifizieren. Das heißt, es werden in keinem existierenden Objekt Attribute modifiziert oder Assoziationen verändert. Nur dadurch kann sichergestellt werden, dass eine Evaluierung einer Bedingung zur Laufzeit nicht das System selbst verändert. Die Vergabe des Stereotyps ≪query≫ an eine Methode bedeutet also eine Obligation des Programmierers, bei der Umsetzung keinerlei Modifikation an Objektzuständen vorzunehmen. Der Stereotyp ≪query≫ vererbt sich auf die Methoden der Unterklassen. Queries können überschrieben werden, müssen jedoch in Unterklassen ebenfalls als Queries implementiert werden. Es gehört heute zum guten und durch Codierungsstandards unterstützten Programmierstil, Query-Methoden mit den Präfixen get, is, has oder give beginnen zu lassen.

Eine Query darf jedoch neue Objekte erzeugen und diese an den Aufrufer zurückgeben, solange neue Objekte von der vorherigen Datenstruktur aus nicht erreichbar sind. Diese „temporären“ Objekte werden vom Java-Laufzeitsystem in einer Implementierung selbständig wieder entfernt. Diese neuen Objekte können auch miteinander verbunden sein und Links in die ursprüngliche Objekstruktur aufweisen (siehe Illustration in Abbildung 3.22).

Leider ist die Erzeugung von Objekten nicht vollständig seiteneffektfrei, denn die Menge aller Objekte einer Klasse (die Extension) verändert sich. Erzeugt eine Query neue Objekte, so wird sie auch unrein genannt. Wird eine unreine Query in einer Spezifikation eingesetzt, so werden die erzeugten Objekte nicht in die Extension aufgenommen.²¹

Würde eine Query diese Objekte nach ihrer Erzeugung nicht modifizieren dürfen, so wären Queries durch statische Programmanalyse erkennbar. Die Java-Implementierung einer Query dürfte nur lokale Variablen belegen, Berechnungen durchführen und andere Queries aufrufen. Dennoch ist auch hier eine auf Daten- und Kontrollflussanalyse beruhende Technik denkbar, die Methodenrümpfe statisch darauf prüfen kann, ob sie Queries sind. Ein solcher Algorithmus kann zwar nicht alle Fälle als korrekt erkennen, aber es ist bereits ausreichend, wenn er in konservativer Weise alle Implementierungen ablehnt, die zweifelhaft sind, ohne damit zu viele Query-Implementierungen auszuschließen.

Eine Query ist eine normale Methode einer Klasse des UML Klassendiagramms. Wie andere Methoden auch, ist eine Query normalerweise für die Verwendung in der Implementierung gedacht. Beispielsweise kann das Ergebnis einer Query von einer aufrufenden Methode in die existente Objektstruktur eingebunden werden.

3.4.2 ≪OCL≫-Methoden

Für die Modellierung komplexerer Eigenschaften ist es oft sinnvoll oder sogar notwendig, zusätzliche Queries zu definieren. Derartige Queries sind jedoch normalerweise nicht für die Implementierung, sondern ausschließlich für die Spezifikation gedacht. Sie stehen deshalb in einer Produktionsinstallation nicht zur Verfügung. Um reine Spezifikationsqueries zu kennzeichnen wird der Stereotyp ≪OCL≫ in Tabelle 3.23 eingeführt. Er unterscheidet sich in seiner Bedeutung von ≪query≫ nur darin, dass eine Implementierung im Produktionssystem nicht vorgesehen ist.²² Abbildung 3.24 zeigt zwei solche Methoden, die der Klasse Person hinzugefügt wurden.

Die Eigenschaften solcher Funktionen können genau wie die Eigenschaften von Queries oder normalen Methoden durch eine Methodenspezifikation oder durch eine direkte Implementierung in Java angegeben werden. Allerdings kann eine direkte Implementierung in Java nur vorgenommen werden, wenn die Signatur keine OCL-Datentypen beinhaltet.

3.4.3 Methodenspezifikation

Das Ziel eines Softwaresystems ist vor allem die Adäquatheit des für den Anwender sichtbaren Verhaltens. Dieses Verhalten wird meist durch komplexe Interaktion von Methoden realisiert. Die Datenstruktur, auf der diese Methoden arbeiten, ist daher eigentlich nur Mittel zum Zweck. Entsprechend ist es nicht nur interessant, mit der OCL Invarianten zu charakterisieren, sondern insbesondere das Verhalten von Methoden zu spezifizieren. Für eine Methodenspezifikation wird der dafür besonders geeignete Vor-/Nachbedingungsstil eingesetzt. Der Kontext einer Methodenspezifikation wird durch eine Methode, die normalerweise mit der beinhaltenden Klasse qualifiziert ist, sowie den zugehörigen Parametern festgelegt. Zwei Bedingungen, die Vorbedingung und die Nachbedingung, die beide mit Namen versehen werden können, charakterisieren den Effekt der Methode. Die Methode isAuctionSpecific aus Abbildung 3.24 kann in der Unterklasse BidMessage wie folgt spezifiziert werden:

Die Vorbedingung mit dem Namen IAS1 besagt, dass die Methode jederzeit aufgerufen werden kann. Die Nachbedingung IAS2 charakterisiert in der Variable result das Ergebnis des Methodenaufrufs. Sie besagt, dass jede Nachricht des Typs BidMessage auktionsspezifisch ist. Wie die nächste Bedingung zeigt, kann von Nachrichten dieser Sorte die betroffene Auktion abgefragt werden:

Die Nachbedingung beschreibt, dass an der als Ergebnis gelieferten Auktion (result) eine Person p teilnimmt, die diese Nachricht erhalten hat.

Die Einschränkung in der Vorbedingung einer Methode besagt nur, dass falls die Vorbedingung erfüllt ist, die Nachbedingung zugesichert wird. Insbesondere wird dabei zugesichert, dass die Methode nicht mit einer Exception terminiert. Dieser Kontrakt im Sinne von [Mey97] macht jedoch keine Aussage darüber, was passieren kann, wenn die Vorbedingung nicht erfüllt ist. Für eine robuste Implementierung sollte auch in diesem Fall mit einer definierten Reaktion geantwortet werden. [HHB02] beschreibt insgesamt vier verschiedene Interpretationen für Methodenspezifikationen, von denen die hier verwendete totale Korrektheit bei Erfüllung der Vorbedingung auch die Terminierung fordert.

In obiger Bedingung wird das Schlüsselwort this verwendet, um damit den Bezug auf das Objekt herzustellen, auf das die Methode angewandt wird. Dieses Schlüsselwort steht nur zur Verfügung, wenn die spezifizierte Methode auf ein Objekt anzuwenden ist, also nicht das Merkmal static besitzt. Die statischen Methoden zur Erzeugung von Message-Objekten (vergleiche Abbildung 3.20) können damit wie folgt beschrieben werden:

Ist die Klasse MessageFactory, zu der diese statische Methode gehört, von untergeordneter Bedeutung oder ist dies noch nicht festgelegt, so kann die Klasse auch ausgelassen werden. Dies ist vor allem für die im letzten Abschnitt eingeführten Spezifikationsqueries von Interesse, da diese normalerweise nicht implementiert und damit keiner Klasse zugewiesen werden.

Obige und die folgende Spezifikation zeigen, dass in Vor- und Nachbedingungen neben der Ergebnisvariable result auch Parameter der Methode eingesetzt werden können:

Die verwendete Listenkomprehension selektiert alle Nachrichten, die einer Auktion a zugeordnet sind. Dieses Beispiel zeigt auch, dass mit der gezeigten Spezifikationstechnik auch die mit dem Stereotyp ≪OCL≫ attributierten Spezifikationsqueries charakterisiert werden, ohne dass eine Implementierung anzugeben ist.

Abbildung 3.25 enthält eine Methode addMessage, die dazu dient, bei einer Person eine weitere Nachricht hinzuzufügen. Die Nachbedingung der Methodenspezifikation enthält einen expliziten Bezug auf den Zustand vor dem Methodenaufruf durch Verwendung des Postfix @pre:

Wie auch in Java ist es möglich Methoden mit variabler Stelligkeit zu definieren, wie das folgende Beispiel zeigt. Methode addMessages kann mit variablen vielen Nachrichten aufgerufen werden. Ihr Parameter ml ist wie in Java vom Typ [Message]:

@pre in Nachbedingungen

Der Operator @pre darf nur auf einzelne Attribute oder Navigationselemente angewandt werden. Ein Ausdruck der Form (a.b)@pre ist bereits syntaktisch verboten. Dennoch ist die Bedeutung des @pre in seinen Nuancen präzise festzulegen. Deshalb soll anhand des aus [RG02, Ric02] übernommenen und in Abbildung 3.26 illustrierten Beispiels gezeigt werden, wie der Operator @pre bei sich dynamisch ändernden Objektstrukturen wirkt.

Abbildung 3.26(a) enthält einen Ausschnitt des Auktionsmodells, der zeigt, dass Personen die Firma wechseln können. Das Objektdiagramm²³ 3.26(b) zeigt, dass john gemeinsam mit drei Kollegen seiner Firma im Auktionssystem angelegt ist. Im Beispiel wird angenommen, dass er von einer neuen Firma abgeworben wird, die bisher noch nicht im Auktionssystem erfasst war. Dann ergibt ein Wechsel die in Abbildung 3.26(c) dargestellte Situation mit dem neuen Objekt c2.

Der Operator @pre kann bei einem Ausdruck der Form john.company.employees in der Nachbedingung auf verschiedene Arten verwendet werden:

john.company.employees == 1,

da dieser Ausdruck vollständig im Zustand nach dem Methodenaufruf ausgeführt wird. Die Navigation mittels company führt auf das Objekt c2 mit dem entsprechenden Attributinhalt.

john@pre.company.employees == 1,

denn die Referenz auf das Objekt john hat sich während des Methodenaufrufs nicht geändert. Es gilt john==john@pre. Erst durch Betrachtung der Attribute werden die Veränderungen in Objekt john sichtbar.

john.company@pre.employees == 3,

weil mit company@pre auf den ursprünglichen Zustand des Objekts john zurückgegriffen wird und dieser Teilausdruck zu Objekt c1 evaluiert. Dann wird aber mittels dem Zugriff über employees der aktuelle Zustand von c1 erreicht.

john.company@pre.employees@pre == 4,

da hier auf das ursprüngliche Objekt c1 in dessen ursprünglichem Zustand zugegriffen wird.

john.company.employees@pre

ist undefiniert, da john.company zu c2 evaluiert und dieses Objekt im ursprünglichen Zustand noch nicht existiert hat.

Ein alternativer, aber gleichwertiger Zugang zum Verständnis von Nachbedingungen ist möglich, indem Ausdrücke der Form company@pre als zusätzlich vereinbarte Attribute verstanden werden, in denen der alte Wert des Attributs company abgelegt ist.

Charakterisierung von Objekterzeugung

Unter der Annahme, dass eine Person zu einer neuen Firma wechselt, kann die in Abbildung 3.26 eingeführte Methode changeCompany wie folgt charakterisiert werden:

Dabei wurde der Operator isnew(.) verwendet, um anzuzeigen, dass company ein neues Objekt ist. Dieser Operator ist eine Kurzform für einen Vergleich der vor und nach einem Methodenaufruf existenten Objektmengen. Der Operator isnew() kann also wie folgt charakterisiert werden:

Der isnew(.)-Operator wirkt in der OCL also nur beschreibend, während mit dem aus Java bekannten new-Konstrukt neue Objekte erzeugt werden. Es ist deshalb zu beachten, dass der isnew-Operator innerhalb von OCL-Nachbedingungen prüft, ob ein Objekt neu angelegt wurde, aber kein neues Objekt erzeugt. Deshalb ist auch zum Beispiel ein let X x = new X() nicht möglich. Das let-Konstrukt ist also nicht geeignet neue Objekte zu beschreiben, sondern Zwischenergebnisse abzulegen. Der isnew-Operator hat die Signatur

und kann nur auf Objekte, nicht aber auf Grunddatentypen oder Container angewandt werden.

Spezifikation eines Konstruktors

Ein Speziallfall einer Methode ist ein Konstruktor. Diese Form der Methode zeichnet sich dadurch aus, dass sie das eigene Objekt erzeugt. Entsprechend sind bei der Spezifikation eines Konstruktors einige Besonderheiten zu beachten. Das Schlüsselwort this und Attribute des Objekts dürfen nur in der Nachbedingung verwendet werden. Die Vorbedingung kann also nur über die Argumente des Konstruktors Aussagen treffen. In der Nachbedingung ist es außerdem verboten mit @pre auf die Attribute des erzeugten Objekts zuzugreifen, da diese im Vorzustand noch nicht existiert haben. Nachfolgende Spezifikation zeigt einen Ausschnitt der Charakterisierung für neue Auktions-Objekte:

Bei Konstruktoren gilt grundsätzlich result==this. Deshalb kann auf die Attribute des Ergebnisses, sowohl mit result.status, mit this.status oder nur mit status zugegriffen werden.

Integration mehrerer Bedingungen

Die Methode changeCompany wurde in der mit CC1pre/CC1post bezeichneten Bedingung unter der Annahme charakterisiert, dass die neue Firma noch nicht existiert. Abbildung 3.27 illustriert aber nun einen Fall, in dem die Firma bereits existiert hat und die Vorbedingung CC1pre nicht zutrifft. In diesem Fall muss auch die Nachbedingung CC1post nicht erfüllt werden. Die obige Spezifikation ist also unvollständig. Sie kann deshalb wie folgt ergänzt werden:

Diese Bedingung beschreibt einen weiteren Teil des Verhaltens der Methode changeCompany, indem sie davon ausgeht, dass das Unternehmen bereits eingetragen ist, aber die Person dem Unternehmen derzeit nicht angehört. Ein derartiger Fall, dass zwei Methodenspezifikationen für dieselbe Methode existieren, kann aus mehreren Gründen auftreten. Beispielsweise können verschiedene Entwickler parallel Anforderungen an eine Methode stellen. Möglich ist auch, dass Anforderungen an dieselbe Methode aus zwei unterschiedlichen Interfaces oder Oberklassen geerbt werden. In beiden Fällen ist eine Integration der Bedingungen notwendig. Die beiden Methodenspezifikationen können als Implikation der Form

verstanden werden.²⁴ Wenn beide Paare gültig sein sollen, so kombiniert sich das zu einer neuen Aussage der Form:

Das heißt, wenn beide Vorbedingungen erfüllt sind, dann müssen auch beide Nachbedingungen erfüllt werden. Dies führt zu Inkonsistenzen, wenn sich die beiden Nachbedingungen widersprechen. Oft werden deshalb Nachbedingungen orthogonal zueinander definiert, indem sie sich mit verschiedenen Aspekten einer Methode beschäftigen oder, wie in obigem Fall, die Vorbedingungen disjunkt sind. Die Kombinierbarkeit von Methodenspezifikationen mit überlappenden Vorbedingungen lässt sich zum Beispiel dazu nutzen, unterschiedliche Aspekte des Verhaltens einer Methode separat zu modellieren.

In manchen Fällen ist es sinnvoll, Methodenspezifikationen nicht nur nebeneinander zu stellen und durch Tests oder Inspektion festzustellen, ob diese konsistent sind, sondern eine explizite Integration in eine einzelne Charakterisierung zu überführen. Dies kann etwa nach folgendem auch in [HHB02] vorgestellten Schema erfolgen:

Wurden dabei allerdings unterschiedliche Namen für die Methodenparameter verwendet, so sind gegebenenfalls Umbenennungen notwendig. Eine so kombinierte Bedingung kann oft vereinfacht werden. Im Beispiel entsteht so:

Vererbung von Methodenspezifikationen

Die Spezifikation des Verhaltens einer Methode wird normalerweise an Unterklassen vererbt. Das heißt, dass jede Unterklasse von Person die Methode changeCompanyüberschreiben und dabei ihr Verhalten im Rahmen der vorgegebenen Methodenspezifikation ändern darf. Auch dürfen weitere Methodenspezifikationen für Unterklassen angegeben werden. Dabei wird das beschriebene Verfahren zur Integration von Methodenspezifikationen verwendet, um die vererbte und hinzugefügte Methodenspezifikation zu kombinieren.

In Frameworks ist es üblich, für zu überschreibende Methoden Default-Implementierungen anzugeben. Eine solche Default-Implementierung kann wesentlich detaillierter durch eine Methodenspezifikation erfasst werden, wenn diese nur für die Methode dieser Klasse gilt. Es ist daher in gewissen Situationen wünschenswert, eine Methodenimplementierung nicht zu vererben. Dafür kann der Stereotyp ≪not-inherited≫ verwendet werden, der die als Default eingestellte Vererbung verhindert.²⁵

Abbildung 3.28 demonstriert die Gültigkeit von vererbten und nicht vererbten Methodenspezifikationen. Die jeweils explizit angegebenen Spezifikationen ergänzen sich und können durch das bereits beschriebene Verfahren integriert werden.

Der Stereotyp ≪not-inherited≫ wird in Tabelle 3.29 eingeführt.

Im Gegensatz zu Methodenspezifikationen stellt sich die Frage nach der Vererbung von Invarianten nicht, da dort der Kontext aus mehreren Objekten bestehen kann und die Extension eines im Kontext angegebenen Typs die Objekte der Unterklassen beinhaltet.

Unvollständige Charakterisierungen

Die gerade entwickelte Bedingung bietet auf den ersten Blick genau wie CC2post eine interessante Implementierungsalternative. Denn statt den Link der wechselnden Person auf die neue Firma zu ändern, könnte auch der Name des alten Firmen-Objekts geändert werden.

Im Allgemeinen bietet eine Methodenspezifikation keine vollständige Beschreibung des gewünschten Verhaltens. So kann eine Implementierung der Methode eine Reihe von weiteren Modifikationen an Systemteilen vornehmen, die in der Bedingung gar nicht explizit erwähnt sind. Dazu gibt es verschiedene, unter dem Begriff Frame-Konzept zusammengefasste Ansätze, mögliche Veränderungen explizit zu kontrollieren [GHG⁺93, BMR95]. Der direkte Ansatz ist es, explizit eine Liste von unveränderlichen Objekten beziehungsweise Attributen anzugeben. In [MMPH99] wird dafür zum Beispiel das Schlüsselwort unchanged verwendet. Diese Negativliste kann jedoch sehr groß werden und erfordert zudem einen Überblick über das Gesamtsystem, ist also nicht modular. Eine Variante ist es, deshalb die Positivliste aller veränderbaren Objekte beziehungsweise ihrer Attribute sowie der möglicherweise neu angelegten Objekte anzugeben. Eine dritte Variante bezieht diese Positivliste implizit aus der Menge der in der Spezifikation erwähnten Objekte und Attribute.

Der letzte Ansatz hat allerdings das Problem, dass normalerweise bei vererbten Methoden explizit erwünscht ist, Veränderungen an neuen Attributen vorzunehmen, die in der Spezifikation der Methode der Oberklasse nicht antizipiert werden konnten.

Für Verifikationszwecke ist es unabdingbar, alle potentiellen negativen Veränderungen in der Spezifikation auszuschließen. Bei einer Verifikation geht man (implizit) von einem bösen Entwicklerteam aus und versucht zu zeigen, dass für alle potentiellen Implementierungen die gewünschten Eigenschaften gelten, die Entwickler also gezwungen sind, ein gutartiges System zu implementieren.

In der Praxis ist diese Annahme nicht sinnvoll, da Entwickler normalerweise wohlwollende Menschen sind und jedem in jeder Phase der Softwareentwicklung zugestanden werden kann, selbständig Entscheidungen zu treffen, die weitere Entwurfs- oder Implementierungsdetails festlegen. Die Metapher des wohlwollenden Entwicklers erlaubt es in der Modellierung, viele Details offen zu lassen. Insbesondere kann davon ausgegangen werden, dass in der Implementierung einer Methode nur eine minimale Anzahl von Modifikationen am Systemzustand vorgenommen werden, um die Vor-/Nachbedingungen korrekt zu realisieren.

Natürlich entsteht hier ein Spannungsfeld zwischen der Notwendigkeit, in der Spezifikation Eigenschaften festzulegen und dem Vertrauen in den Entwickler, unvollständige Spezifikationen richtig mit Details auszufüllen. Dieses Spannungsfeld kann aber unter anderem dadurch reduziert werden, dass Spezifikateure und Entwickler dieselbe Personengruppe sind oder eng verzahnt zusammenarbeiten.

Als Beispiel hierfür kann der letzte Fall company.name==name für die Methode changeCompany dienen. In diesem Fall gehört die Person bereits zum Unternehmen. Der Fall wird zunächst ebenfalls separat spezifiziert und bei Bedarf in die Gesamtspezifikation integriert:

Dabei ist auffallend, dass die Erfüllung der Nachbedingung keine echten Aktivitäten erfordert, sondern nur sicherstellt, dass die in den anderen Fällen stattfindenden Aktivitäten unterbleiben. Dabei wird explizit festgelegt, dass die in den anderen Fällen veränderten Attribute hier unverändert bleiben sollen. Über weitere Attribute wird nicht gesprochen, da von einem wohlwollenden Entwickler ausgegangen wird, dem aber eventuelle Flüchtigkeitsfehler unterlaufen und deshalb der hier modellierte dritte Fall bei der Entwicklung des Codes und der Tests helfen kann.

Rekursive Funktionsdefinition

Wird eine Methode durch Vor- und Nachbedingung beschrieben, so kann diese Methode bereits während der Definition rekursiv verwendet werden. Der OCL-Standard [OMG10b] erlaubt rekursive Definitionen, ohne jedoch deren Bedeutung präzise zu klären. Die Spezifikation

nutzt foo rekursiv. Aufgrund der speziellen Struktur, mit result auf der linken Seite der Gleichung kann diese Spezifikation als Funktionsimplementierung gelesen werden und erhält so eine eindeutige Bedeutung. Die präzise Bedeutung hinter rekursiven Funktionsdefinitionen ist relativ komplex und soll hier nicht ausgeführt werden. Wesentlicher Kernpunkt dabei ist, dass bei einer rekursiven Gleichung oft viele Implementierungen möglich sind, aber bei speziellen Formen der Spezifikation durch Fixpunktinduktion eine eindeutige Bedeutung festgelegt wird, die genau dem Verhalten der Implementierung entspricht.

Wir geben hier einige Beispiele an, die im Sinne einer Spezifikation korrekt sind, für bestimmte Anwendungsfälle sogar sinnvoll sein können, aber durch die rekursive Verwendung der definierten Funktion auch sehr gefährlich wirken:

würde als Implementierung nicht unbedingt terminieren. Als Spezifikation ist für den Fall a <= 0 etwas ausgesagt während für a > 0 einfach nur keine Aussage getroffen und damit jede Implementierung möglich ist. Auf die Spitze getrieben ist dies durch eine völlig fehlende Aussage:

Demgegenüber hat

durchaus eine Aussage und diverse Implementierungen, sogar die recht einfache foo(a,b)=0. Aber keine der Implementierungen ist bevorzugt. Mehrere Implementierungsalternativen bietet auch:

Da nur Queries in Bedingungen genutzt werden dürfen, sind rekursive Methodendefinitionen nur für Queries möglich. Da Attributmanipulationen so wegfallen und bei geeigneter Definitionsstruktur in einer Funktionsrumpf-artigen Form kann unter Nutzung induktiver Datenstrukturen wie die natürlichen Zahlen sogar eine einzige und damit eindeutige Impementierung beschrieben werden. In Abschnitt 3.5.1 benutzen wir dies, um die transitive Hülle einer Relation zu beschreiben. Da wir die OCL grundsätzlich als Spezifikationssprache einsetzen, sind Definitionen mit rekursiv verwendeten Funktionen erlaubt, bleiben aber eigenschaftsorientierte Spezifikationen.

Hilfsvariablen und das let-Konstrukt

In komplexeren Methodenspezifikationen kommt es vor, dass in der Vorbedingung ein bestimmtes Objekt gesucht wird, an dem in der Nachbedingung eine Änderung vorgenommen werden soll. Um für Vor- und Nachbedingung gemeinsame Variablen einführen zu können, wurde das let-Konstrukt erweitert. Es erlaubt nun Variablen zu definieren, die dann in beiden Bedingungen gleich belegt sind. Dadurch kann die Methodenspezifikation CC2pre/CC2post umgebaut werden zu:

Diese Erweiterung des let-Konstrukts kann als doppelte Anwendung des let-Konstrukts verstanden werden:

Die Einführung von Zwischenvariablen und Hilfsfunktionen durch das let-Konstrukt kann aber auch umgekehrt als Definition von Attributen beziehungsweise Methoden einer anonymen Klasse verstanden werden, die implizit in den Kontext aufgenommen wird. Abbildung 3.30 illustriert dies anhand der beiden Beispiele Time2 und Time3 aus Abschnitt 3.1.2. Für die Beschreibung der neuen Attribute und der neuen Operation wurde ebenfalls OCL verwendet. Wie bereits in [CK01] diskutiert wurde, ist diese Form der Illustration jedoch nicht äquivalent zur Definition mit dem let-Konstrukt selbst. Die mit let definierten Elemente stehen nur lokal zur Verfügung und können außerhalb des Definitionsbereichs nicht verwendet werden. Außerdem besteht ein wesentlicher Unterschied in der Behandlung von undefinierten Ergebnissen, denn das let-Konstrukt erlaubt undefinierte Zwischenergebnisse und kann doch in definierter Weise ein Gesamtergebnis erbringen.

Wie bereits in Abschnitt 3.1.2 bemerkt, erhöht die Möglichkeit rekursiver Definitionen innerhalb des let-Konstrukts die Komplexität der Typisierung (vgl. [CK01], Gofer [Jon96] und SML [MTHM97]) und wird, wie viele in der Literatur zu findende falsche rekursive Definitionen der transitiven Hülle einer Assoziation zeigen, weniger verständlich. Da OCL eine Spezifikationssprache ist, sind rekursive Definitionen als Gleichungen und nicht als operationelle Definitionen zu verstehen. Gleichungen sind aber, wie in Abschnitt 3.5.1 noch genauer diskutiert wird, mehrdeutig. Da rekursive Definitionen auch durch das zugrunde liegende Objektsystem möglich sind, wird auf die Möglichkeit einer rekursiven Definition verzichtet.

3.4.4 Bibliothek von Queries

OCL ist als Bedingungssprache konzipiert, die es mit Ausnahme lokaler Definitionen in let-Konstrukten nicht erlaubt, eigene Datentypen, Methoden oder Variablen zu definieren. Stattdessen werden Datentypen und Methoden des zugrunde liegenden Modells und die Stereotypen ≪query≫ und ≪OCL≫ eingesetzt. Das zugrunde liegende Modell kann deshalb vorgefertigte Bibliotheken von Queries anbieten, die eine kompakte Definition von OCL-Bedingungen erlauben. In diesem Abschnitt werden beispielhaft einige dieser Funktionen diskutiert und damit gezeigt, wie derartige Bibliotheken erstellt werden können.

Formal werden die hier definierten Spezifikationsqueries von einer Klasse angeboten, die der Einfachheit halber OCLlib genannt wird. Es wird angenommen, dass diese Klasse immer implizit im Kontext einer Bedingung vorhanden ist, so dass ihre statischen Queries statt mit OCLlib.sum auch mit sum verwendet werden können. Abbildung 3.31 enthält die Signatur eines Ausschnitts dieser kleinen Bibliothek. Die darin enthaltenen Queries sind durch die Unterstreichung als statisch deklariert, damit sie ohne Bezug auf ein Objekt verwendet werden können.

Für Container mit ganzen Zahlen stehen mathematische Operationen wie Summe und Maximum zur Verfügung:

Zur aufsteigenden Sortierung von Listen ganzer Zahlen kann der Operator sort verwendet werden.

Eine Vielzahl weiterer vordefinierter und domänen- oder projektspezifischer Operationen ist denkbar und sollte für OCL in ähnlicher Form zur Verfügung stehen, wie das für Programmiersprachen bereits der Fall ist.

Bernhard Rumpe. Agile Modellierung mit UML. Springer 2012

<< zurück

MBSE Home

weiter >>