Fakultt Informatik, Institut SMT, Lehrstuhl Softwaretechnologie
Einfhrung in OCL (Object Constraint Language)
Dr Birgit DemuthDr. Birgit Demuth
Rules and models destroy genius and art.
William HazlittEnglish writer, 1778 - 1830 English writer, 1778 1830
Dr. Birgit Demuth SWT II, SS 2009 2
Was wollen wir lernen?
Einfhrung in die Thematik (Vertragsmodell, Zusicherungen, berblick OCL, Literaturquellen)Sprachkonzepte und OCL by Example Sprachkonzepte und OCL by Example
Anwendungsflle fr OCL Aktuelle OCL ToolsAktuelle OCL Tools
Dr. Birgit Demuth SWT II, SS 2009 3
Theoretische GrundlagenTheoretische Grundlagen
Hoare-Tripel { P } S { Q } [Hoare, 1969], z.B.{x=y} y:=y-x+1 {y=1}
Design by Contract (Vertragsmodell) [Meyer, 1997], bertragung auf Klassen und Methoden
Dr. Birgit Demuth SWT II, SS 2009 4
Softwarepionier C.A.R. Hoare
Software-Pioniere, sd&m-Konferenz 2001 in Bonn
"What a wonderful set of resources! Congratulations on assembling this marvelous collection. Grady Booch
www.sdm.de/de/publikationen/konferenzen/softwarepioniere2001/
Dr. Birgit Demuth SWT II, SS 2009 5
Zusicherungen (defensive Programmierung)
Vorbedingung: muss die Kundenklasse einhalten
Nachbedingung:garantiert die Anbieterklasse garantiert die Anbieterklasse
Klasseninvariante: muss von allen Methoden der Anbieterklasse
eingehalten werden (vor und nach jeder Methodenausfhrung)g
gilt whrend der gesamten Lebensdauer der Objekte der Klasse
Dr. Birgit Demuth SWT II, SS 2009 6
Formulierung von Zusicherungen
Modellbasiert: OCL
In Programmiersprachen: EIFFEL
JASS (Ja a ith ASSe tions) JASS (Java with ASSertions) JML (Java Modeling Language) Java (assert)
Dr. Birgit Demuth SWT II, SS 2009 7
OCL (Object Constraint Language)
ergnzt die Unified Modeling Language (UML) formale Sprache fr die Definition von Constraints formale Sprache fr die Definition von Constraints
(Zusicherungen) und Anfragen auf UML-Modellen standardisiert (OMG)
d kl deklarativ seiteneffektfrei fgt graphischen (UML-)Modellen przisierte Semantik fgt graphischen (UML )Modellen przisierte Semantik
hinzu verallgemeinert fr alle MOF-basierten Metamodelle inzwischen allgemein akzeptiert, viele Erweiterungen Core Language von Modelltransformationssprachen
(QVT) Regelsprachen (PRR)
Dr. Birgit Demuth SWT II, SS 2009 8
(QVT), Regelsprachen (PRR) ...
Literatur
[1] Warmer, J., Kleppe, A.: The Object Constraint Language. [ ] , , pp , j g gPrecise Modeling with UML. Addison-Wesley, 1999
[2] Warmer, J., Kleppe, A.: The Object Constraint Language Second Edition.Second Edition.Getting Your Models Ready For MDA. Addison-Wesley, 2003
[3] OMG UML specification, www.omg.org/technology/documents/modeling spec catalowww.omg.org/technology/documents/modeling_spec_catalog.htm#UML
[4] OMG UML 2.0 OCL, www omg org/technology/documents/formal/ocl htmwww.omg.org/technology/documents/formal/ocl.htm
[5] Brgge, B., Dutoit, A.H.: Objektorientierte Softwaretechnik mit UML, Entwurfsmustern und Java. PEARSON Studium, 2004 (kurze Zusammenfassung)
Dr. Birgit Demuth SWT II, SS 2009 9
2004 (kurze Zusammenfassung)
Dr. Birgit Demuth SWT II, SS 2009 10
Constraint
Definition nach [1] A constraint is a restriction on one or more values of (part of)
an object-oriented model or system.
Definition nach [5] Eine Einschrnkung ist ein Prdikat, dessen Wert wahr oder
f l h i t falsch ist. Boolesche Ausdrcke sind Einschrnkungen. OCL erlaubt die formale Spezifikation von Einschrnkungen fr
einzelne Modellelemente (z B Attribute Operationen Klassen) einzelne Modellelemente (z.B. Attribute, Operationen, Klassen) sowie fr Gruppen von Modellelementen (z.B. Assoziationen)
Wir benutzen im folgenden weiter den Begriff des Constraints.
Dr. Birgit Demuth SWT II, SS 2009 11
Invariante
Definition Eine Invariante ist ein Constraint, das fr ein Objekt
whrend seiner ganzen Lebenszeit wahr sein sollte whrend seiner ganzen Lebenszeit wahr sein sollte.
Syntaxcontext inv []:
Dr. Birgit Demuth SWT II, SS 2009 12
OCL/UML By Example
Dr. Birgit Demuth SWT II, SS 2009 13
Invariante - Beispiel
context Meeting inv: self.end > self.start
quivalente Formulierungenquivalente Formulierungencontext Meeting inv: end > start
-- self bezieht sich immer auf das Objekt, fr das das C t i t b h t i dConstraint berechnet wird
context Meeting inv startEndConstraint: self.end > self.start
-- Vergabe eines Namens fr das Constraint
Sichtbarkeiten von Attributen u.. werden durch OCL standardmig ignoriert.
Dr. Birgit Demuth SWT II, SS 2009 14
Precondition (Vorbedingung)
Pre- und Postconditions sind Constraints, die die Anwendbarkeit und die Auswirkung von Operationen spezifizieren, ohne dass dafr ein Algorithmus oder eine Implementation angegeben dafr ein Algorithmus oder eine Implementation angegeben wird.
DefinitionDefinition
Eine Precondition ist ein Boolescher Ausdruck, der zum Zeitpunkt des Beginns der Ausfhrung der zugehrigen Operation wahr sein mussOperation wahr sein muss.
Syntax
context :: ()pre []:
Dr. Birgit Demuth SWT II, SS 2009 15
Precondition - Beispiele
context Meeting::shift(d:Integer) pre: self.isConfirmed = false
context Meeting::shift(d:Integer) pre: d>0pre: d>0
context Meeting::shift(d:Integer) pre: self.isConfirmed = false and d>0
Dr. Birgit Demuth SWT II, SS 2009 16
Postcondition (Nachbedingung)
Definition
Eine Postcondition ist ein Boolescher Ausdruck, der unmittelbar nach der Ausfhrung der zugehrigen unmittelbar nach der Ausfhrung der zugehrigen Operation wahr sein muss.
Syntaxcontext :: ()post []: post []:
Dr. Birgit Demuth SWT II, SS 2009 17
Postcondition - Beispiele
context Meeting::duration():Integerpost: result = self.end self.start
-- result bezieht sich auf den Rckkehrwert der Operation
context Meeting::confirm()context Meeting::confirm()post: self.isConfirmed = true
context Meeting::shift(d:Integer)post: start = start@pre +d and end = end@pre + d
-- start@pre bezieht sich auf den Wert vor Ausfhrung derstart@pre bezieht sich auf den Wert vor Ausfhrung der-- Operation -- start bezieht sich auf den Wert nach Ausfhrung der Operation-- @pre ist nur in Postconditions erlaubt
Dr. Birgit Demuth SWT II, SS 2009 18
OCL-Ausdrcke (1)
Boolesche Ausdrcke Standardbibliothek
Basistypen: Boolean Integer Integer Real Stringll k Kollektionstypen:
Collection Set Set Ordered Set (nur OCL2) Bag
SDr. Birgit Demuth SWT II, SS 2009 19
Sequence
OCL-Ausdrcke (2)
Nutzerdefinierte Typen (OCLType) Klassentyp (Modelltyp):
Kl i i Kl di Klasse in einem Klassendiagram Generalisierung zwischen den Klassen fhrt zu
Supertypen. Eine Klasse besitzt die folgenden Features:
Attribute (z.B. start)
Operationen (nur query operations) (z.B. Operationen (nur query operations) (z.B. duration())
Klassenattribute (z.B. Date::today)
Klassenoperationen Klassenoperationen Assoziationsenden (Navigationsausdrcke)
Aufzhlungstyp (enumeration typ)
Dr. Birgit Demuth SWT II, SS 2009 20
OCL-Typhierarchie mit Standardtypen (Ausschnitt)
T
T T T T
Dr. Birgit Demuth SWT II, SS 2009 21
OCL-Typ-Konformittsregeln yp g
OCL ist eine typsichere Sprache. Der Parser prft OCL-Ausdrcke auf Konformitt: Typ 1 ist konform zu Typ 2, wenn eine Instanz von Typ 1
an jeder Stelle ersetzt werden kann wo eine Instanz vom an jeder Stelle ersetzt werden kann, wo eine Instanz vom Typ 2 erwartet wird.
Allgemeine Regeln Typ 1 ist konform zu Typ 2, wenn Sie identisch sind.
J d T i t k f j d i S t Jeder Typ ist konform zu jedem seiner Supertypen. Typkonformitt ist transitiv.
Dr. Birgit Demuth SWT II, SS 2009 22
OCL Constraints und VererbungConstraints allgemein Constraints einer Superklasse werden von den Subklassen geerbt.
Dabei gilt das Liskovsche Substitutionsprinzip.g p p
Invarianten Eine Subklasse kann die Invariante verstrken, sie aber nicht Eine Subklasse kann die Invariante verstrken, sie aber nicht
abschwchen.
Preconditions Eine Vorbedingung kann bei einem berschreiben einer Operation
einer Subklasse aufgeweicht, aber nicht verstrkt werden.
Postconditions Eine Nachbedingung kann bei einem berschreiben einer Operation
einer Subklasse verstrkt, aber nicht aufgeweicht werden.
Dr. Birgit Demuth SWT II, SS 2009 23
Navigationsausdrcke
Assoziationsenden (Rollennamen) knnen verwendet werden, um von einem Object im Modell/System zu einem anderen zu navigieren (Navigation)g ( g )
Navigationen werden in OCL als Attribute behandelt (dot-Notation).
Der Typ einer Navigation ist entweder Der Typ einer Navigation ist entweder Nutzerdefinierter Typ (Assoziationsende mit Multiplizitt
maximal 1)
Kollektion von nutzerdefinierten Typen (Assoziationsende Kollektion von nutzerdefinierten Typen (Assoziationsende mit Multiplizitt > 1)
Dr. Birgit Demuth SWT II, SS 2009 24
Navigationsausdrcke - Beispiele
Nutzerdefinierter Typz.B. moderatorNavigation von Meeting ist vom Typ Teammemberg g yp
context Meeting i lf d t d G d f linv: self.moderator.gender = Gender::female
Dr. Birgit Demuth
Top Related