OCLByExampleLectureforcomputerscience.pdf

ocl

1. Department of Computer Science, Institute for Software and Multimedia Technology
OCL
(Object Constraint Language) (Object Constraint Language)
by Example
Dr Birgit Demuth Dr
.
Birgit Demuth

2. In theory, there is no difference
between theory and practice.
But, in practice, there is.
Jan L. A. van de Snepscheut/Yogi Bera
Dr. Birgit Demuth MINE Summer School, Nida, 2009 2

3. Main Goals of the Lecture • Bridge the gap between practically used software
specifications (UML) and formal languages
Introduce
into
OCL (
history

outline

literature
)
•
Introduce
into
OCL (
history
,

outline
,

literature
)
• Learn how to specify semantics using OCL
•
Learn
what
are
interesting
OCL
use
cases
Learn
what
are
interesting
OCL
use
cases
• Inform what OCL tools can already be used Dr. Birgit Demuth MINE Summer School, Nida, 2009 3

4. Foundation: Assertions
•An assertionis a predicate (i.e., a true–false statement)
placed in a program to indicate that the developer thinks
th t th di t i l t t th t l [Wiki di ] th
a
t th
e

pre
di
ca
t
e
i
s

a
l
ways
t
rue

a
t th
a
t
p
l
ace
[Wiki
pe
di
a
]
.
•Usa
g
e in
g
– Hoare logic [Hoare 1969]
– Design by contract [Meyer 1986, Eiffel]
For run
time checking (Java (
t
) JML
JASS SQL
–
For run
-
time checking (Java (
asser
t
)
,
JML
,

JASS
,
SQL
,

…)
– During the development cycle (debugging) – Static assertions at compile time
Dr. Birgit Demuth MINE Summer School, Nida, 2009 4

5. Object Constraint • Model-based assertion
[dl]df fll
•
[
Warmer an
d
K
l
eppe
]

d
e
f
ine a constraint as
f
o
ll
ows:
“A constraint is a restriction on one or more values
A constraint is a restriction on one or more values of (part of) an object-oriented model or system.“
• OCL as specification language for object constraints Dr. Birgit Demuth MINE Summer School, Nida, 2009 5

6. History of OCL • Developed at IBM in 1995 originally as a business
engineering language
Adopted as a formal specification language within
UML
•
Adopted as a formal specification language within
UML
• Part of the official OMG standard for UML (from
version 1.1 on)
• Used for precisely defining the well-formedness rules
(WFRs) for UML and further OMG-related metamodels
•
Current version is OCL 2 0
•
Current version is OCL 2
.
0
Dr. Birgit Demuth MINE Summer School, Nida, 2009 6

7. OC
L
(Object Constraint Language)
• Extends the Unified Modeling Language (UML)
•
Formal language for the definition of constraints and Formal language for the definition of constraints and queries on UML models
• Declarative
Sd ff f
•
S
i
d
e e
ff
ect
f
ree
• Add precise semantics to visual (UML-) models
•
Generalized for all MOF based metamodels
•
Generalized for all MOF based metamodels
• Meanwhile generally accepted • Many extensions such as for temporal constraints • „Core Language“ of other OMG languages (QVT, PRR) Dr. Birgit Demuth MINE Summer School, Nida, 2009 7

8. Literature
[
1
]
Warmer
,
J.
,
Kle
pp
e
,
A.: The Ob
j
ect Constraint Lan
g
ua
g
e.
[
],,pp, j gg
Precise 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 catalo www.omg.org/technology/documents/modeling
_
spec
_
catalo
g.htm#UML
[4] OMG UML 2.0 OCL,
www omg org/technology/documents/formal/ocl htm www
.
omg
.
org/technology/documents/formal/ocl
.
htm
[5] Heinrich Hußmann: Formal Specification of Software
Systems. Course, 2000, Technische Universität Dresden
Dr. Birgit Demuth MINE Summer School, Nida, 2009 8

9. Dr. Birgit Demuth MINE Summer School, Nida, 2009 9

10. Constraint
Definition
–„A constraintis a restriction on one or more
values of (part of) an object-oriented model or
system
“

system
.

• A constraint is formulated on the level of classes, but
its semantics is applied on the level of objects.
• originally formulated in the syntactic context of a UML
UML
model (i e a set of UML diagrams)
UML
model (i
.
e
.
a set of UML diagrams)
Dr. Birgit Demuth MINE Summer School, Nida, 2009 10

11. Invariant Invariant
Definition
–An invariantis a constraint that should be true for an
object during its complete lifetime.
• Invariants often represent rules that should hold for the
real-life objects after which the software objects are
modeled.
Syntax Syntax
context <classifier> i
nv[<constraint name>]: <Boolean OCL ex
p
ression>
Dr. Birgit Demuth MINE Summer School, Nida, 2009 11
p

12. OCL/UML By Example
Dr. Birgit Demuth MINE Summer School, Nida, 2009 12

13. Invariant
-
Examples
Invariant
-
Examples
c
ontext Meetin
g

i
nv
:
self.end >
s
elf.start
g
Equivalent Formulations
context
Meeting
inv
: end >
start
context
Meeting

inv
:

end

>

start
--"self" always refers to the object identifier from which the
constraint is evaluated.
context Meeting inv startEndConstraint: s
elf.end >
s
elf.start
--
Names can be given to the constraint
Dr. Birgit Demuth MINE Summer School, Nida, 2009 13

14. P econdition /Postcondition P
r
econdition /Postcondition
•
Constraint that specify the applicability and effect of an
•
Constraint that specify the applicability and effect of an operation without stating an algorithm or implementation
• Are attached to an operation in a class diagram
Allow a more complete specification of a system
•
Allow a more complete specification of a system Dr. Birgit Demuth MINE Summer School, Nida, 2009 14

15. Precondition Definition Definition
– Constraint that must be true just prior to the execution
of an operation
Syntax
context <classifier>::<operation> (<parameters>) context

<classifier>::<operation>

(<parameters>)
pre[<constraint name>]: <
Boolean OCL ex
p
ression>
p
Dr. Birgit Demuth MINE Summer School, Nida, 2009 15

16. Precondition - Examples context Meeting::shift(d:Integer)
pre: self.isConfirmed = false
context Meeting::shift(d:Integer) pre: d>0 pre:

d>0
context Meeting::shift(d:Integer) pre: self.isConfirmed = false and d>0 Dr. Birgit Demuth MINE Summer School, Nida, 2009 16

17. Postcondition Postcondition Definition
C t i t th t t b t j t ft t th ti
–
C
ons
t
ra
i
n
t th
a
t
mus
t b
e
t
rue
j
us
t
a
ft
er
t
o
th
e

execu
ti
on

of an operation
• Postconditions are the way how the actual effect of an
operation is described in OCL.
Syntax
context <classifier>::<operation> (<parameters>) context

<classifier>::<operation>

(<parameters>)
post[<constraint name>]:
<Boolean OCL expression>
Dr. Birgit Demuth MINE Summer School, Nida, 2009 17

18. Postcondition - Examples context Meeting::duration():Integer
post: result= self.end – self.start
keyword
result
refers to the result of the
operation
--
keyword
result
refers to the result of the
operation
context Meeting::confirm() post: self.isConfirmed = true
Dr. Birgit Demuth MINE Summer School, Nida, 2009 18

19. Postcondition – Examples (cont.) c
ontext Meeting::shift(d:Integer)
post: start = start@pre+d and end = end@pre+ d
--
start@pre
indicates a part of an expression
start@pre
indicates a part of an expression
-- which is to be evaluated in the original state
-- before execution of the operation
--
start refers to the value upon completion of the operation
--
@pre is only allowed in postconditions @pre is only allowed in postconditions
Dr. Birgit Demuth MINE Summer School, Nida, 2009 19

20. Postcondition – Examples (cont.) •messaging only in postconditions
•
is specifying that communication has
taken place
is specifying that communication has
taken place
•hasSent (“^“) operator c
ontext Subject::hasChanged()
post: observer^update(2,4)
/
* standard observer
p
attern:
/
p
results in true if an update message with arguments 2 and 4
was sent to the observer object during execution of the
operation
hasChanged()
operation
hasChanged()
*/
Dr. Birgit Demuth MINE Summer School, Nida, 2009 20

21. Buildin
g
OCL Ex
p
ressions <OCL ex
p
ression>
(
1
)
gp p ()
• Boolean expressions •Standard library of
primitive types and associated operations
–Basic types (Boolean, Integer, Real, String)
Collection types:
–
Collection types:
• Collection
•Set
• Ordered Set (only OCL2) •Bag •
Sequence
Dr. Birgit Demuth MINE Summer School, Nida, 2009 21
•
Sequence

22. Building OCL Expressions <OCL expression> (2) User defined types (OCLType)
Cl t (Mdl t)
•
Cl
ass
t
ype
(M
o
d
e
l t
ype
)
:
– Classifier in a class diagram (implicitly defined)
– Generalisation among classiefiers leads to Supertypes
– A class has the following Features:
• Attributes (start)
•
Operations
(duration())
•
Operations
(duration())
• Class attributes (Date::today)
• Class operations
• Association ends („navigation expressions“)
•Enumeration t
yp
e
(
Gender
,
Gender::male
)
Dr. Birgit Demuth MINE Summer School, Nida, 2009 22
yp
(, )

23. OCL Type Hierarchy
T
T
T
T
T
Dr. Birgit Demuth MINE Summer School, Nida, 2009 23

24. OCL T
yp
e Conformance Rules
yp
OCL is a strongly typed language . The parser has to check the conformance:
T1 f T2 if i f T1 b
•
T
ype
1
con
f
orms

to
T
ype
2 if
an
i
nstance

o
f T
ype
1
can
b
e

substituted at each place where an instance of Type2 is
expected. General rules:
Eh T f t h f it t
•
E
ac
h T
ype

con
f
orms
t
o

eac
h
o
f it
s

super
t
ypes.
• Type conformance is transitive.
•
A paramerized type T(X) conforms to T(Y) if X conforms to Y
Dr. Birgit Demuth MINE Summer School, Nida, 2009 24
•
A paramerized type T(X) conforms to T(Y) if X conforms to Y
.

25. OCL Constraints and Inheritance • Constraints are inherited. •
Liskov
’
s Substitution Principle
•
Liskov s Substitution Principle
– Wherever an instance of a class is expected, one can
always substitute an instance of any of its subclasses.
•An invariantfor a superclass is inherited by its subclass.
A subclass may strengthen the invariant but cannot weaken
it. •A preconditionmay be weakened but not strengthened in
a redefinition of an operation in a subclass.
•A postconditionmay be strengthened but not weakened in
a redefinition of an operation in a subclass.
Dr. Birgit Demuth MINE Summer School, Nida, 2009 25

26. Navigation Expressions
•
Association ends (role names) are be used to navigate
“

•
Association ends (role names) are be used to
„
navigate
from one object in the model to another object.
• Navigations are treated as attributes (dot-Notation).
The type of a navigation expression is either a
•
The type of a navigation expression is either a
–User defined type
(association end with multiplicity at most 1)
–Collection
(association end with multiplicity > 1) Dr. Birgit Demuth MINE Summer School, Nida, 2009 26

27. Ni i E i
El
N
av
i
gat
i
on
E
xpress
i
ons

-
E
xamp
l
es
User defined type
– Navigation from
M
eetingto
m
oderator
results in type Teammember
context Meeting context

Meeting

inv: self.moderator.gender = Gender::female
Dr. Birgit Demuth MINE Summer School, Nida, 2009 27

28. Navi
g
ation Ex
p
ressions - Exam
p
les
gp
p
Collection
– Navigation von Meeting to participants
results in type
Set(Teammember)
results in type
Set(Teammember)
context Meeting inv: self->collect(participants)->size()>=2 or with
shorthand
notation:
or with
shorthand
notation:
context Meeting inv: self.participants->size()>=2
Dr. Birgit Demuth MINE Summer School, Nida, 2009 28

29. Collection Operations (1) • 22 operations with variant meaning depending on the
collection type such as
–equals(=) and not equals operation (<>)
– Transformations (
a
sBag
(
),
a
sSet
(
),
a
sOrderedSet
(
),
asSequence())
–including(object)andexcluding(object) –
flatten
()
for
example
flatten
()
for
example
Set{Bag{1,2,2},Bag{2}} ÆSet{1,2}
–Typicalsetoperations
(
union intersection minus symmetricDifference
)
(
union
,
intersection
,
minus
,
symmetricDifference
)
– Operations on ordered collections only (OrderedSet,
Sequence) (such asfirst(), last(), indexOf())
Dr. Birgit Demuth MINE Summer School, Nida, 2009 29

30. Collection O
p
erations
(
2
)
p()
Loop operations (Iterators)on all collection types
any(expr) any(expr) collect(expr)
exists(expr)
forAll(expr) isUnique(expr) one(expr) select(expr) reject(expr) reject(expr) sortedBy(expr)
Dr. Birgit Demuth MINE Summer School, Nida, 2009 30

31. Loo
p
O
p
eration
i
terate
()
pp
()
Collection->iterate( element : Type1;
result
:
Type2 = <
expression
>
result
:
Type2

=

<
expression
>
| <expression with element and result> }
• All other loop operations can be described as a special
case of iterate()such as in the following simple
example:
Set {1,2,3}->sum() Set{1,2,3}->
iterate{i: Integer, sum: Integer=0 | sum + i }
Dr. Birgit Demuth MINE Summer School, Nida, 2009 31

32. Further Examples for Collection Operations (1) •
A teammeeting has to be organized for a whole team A teammeeting has to be organized for a whole team ( forAll()):
i
c
ontext Teammeet
i
ng
inv: participants->forAll(team=self.for)
context Meetinginv: oclIsTypeOf(Teammeeting)
implies participants->forAll(team=self.for)
Dr. Birgit Demuth MINE Summer School, Nida, 2009 32

33. Further Examples for collection operations (2) • Postconditions
(
s
elect
()
)
:
(
()
)
context Teammember::numMeeting():Integer post: result=meetings->size() context Teammember::numConfMeeting():Integer context

Teammember::numConfMeeting():Integer
post: r
esult=meetin
g
s
-
>
s
elect
(
isConfirmed
)
-
>
size
()
g
()
()
Dr. Birgit Demuth MINE Summer School, Nida, 2009 33

34. Flattening of Collections Automatic flattening rule for all nested collections Automatic flattening rule for all nested collections
self.participants.meetings
in the context „Meeting“
What happens? What happens? • self.participants delivers a Set(Person) •
s
elf.
p
artici
p
ants.meetin
g
sdelivers a
pp g
Bag(Set(Person)
• Results in a Bag(Person) Dr. Birgit Demuth MINE Summer School, Nida, 2009 34

35. Derivation Rule (derive, OCL2) Derivation Rule (derive, OCL2)
•
Derived attribute
(size)
Derived attribute
(size)
context Team::size:Integer derive:
members
-
>size()
derive:
members
-
>size()
•Derived association (conflict)
– defines a set of meetings that are in conflict with each other context Meeting::
conflict:Set(Meeting)
context

Meeting::
conflict:Set(Meeting)
derive: select(m|m<>self and self.inConflict(m))
Dr. Birgit Demuth MINE Summer School, Nida, 2009 35

36. Initial Value (init, OCL2) ElE
xamp
l
es
c
ontext Meetin
g
::isConfirmed : Boolean
g
init:false context Teammember:meetings : Set(Meetings) context

Teammember:meetings

:

Set(Meetings)
init:Set{}
• Note that an initial value must be valid only at the object
creation time!
Dr. Birgit Demuth MINE Summer School, Nida, 2009 36

37. Query Operation (body, OCL2) • Operations that do not change the state of the system • Can be used as a query language
Power
of
SQL
•
Power
of
SQL
Example
context T
eammember
:
:
g
etMeetin
g
Titles
()
:
B
a
g
(
Strin
g)

gg
()
g
(g)
body:meetings->collect(title)
Dr. Birgit Demuth MINE Summer School, Nida, 2009 37

38. Let Ex
p
ression
(
let
)
p()
• Interesting for complex expressions
•D
e
fin
e

a
l
oca
l v
a
ri
ab
l
e

(
noCo
nfli
ct
)
t
h
at

ca
n
be

used

eeaocaaabe
(
oCo ct
)
tatca beused
instead of a sub-expression
c
ontext Meeting
i
nv
:
letnoConflict: Boolean =
participants meetings
-
>
forAll
(
m|m
<>
self
and
participants
.
meetings
>

forAll
(
m|m
<>
self
and
m.isConfirmed implies not self.inConflict(m))
in isConfirmed impliesnoConflict
Dr. Birgit Demuth MINE Summer School, Nida, 2009 38

39. Definin
g
New Attributes and O
p
erations
(
def, OCL2
)
gp
()
• Adding attributes and query operations to the model •
Syntax is similar to the let expression
•
Syntax is similar to the let expression
• Helpful for the reuse of OCL expressions in several
constraints
context Meeting context

Meeting

def: noConflict : Boolean =
participants.meetings->forAll(m|m<>self and
m.isConfirmed implies not self.inConflict(m))
Dr. Birgit Demuth MINE Summer School, Nida, 2009 39

40. Packa
g
in
g
OCL Ex
p
ressions
gg p
packageMeetingExample context Meeting::isConfirmed : Boolean init: false init:

false

context Teammember:meetings : Set(Meetings)
i
nit: Set{}
.... endpackage Dr. Birgit Demuth MINE Summer School, Nida, 2009 40

41. Limitations of OCL Limitations of OCL •
No support for
inconsistency detection
for OCL
No support for
inconsistency detection
for OCL
•„Frame Problem“
– Operations are specified by what they change (in post-
d)hhl h h
con
d
itions
)
, wit
h
t
h
e imp
l
icit assumption t
h
at everyt
h
ing
else (the frame) remains unchanged
•
Limited recursion Limited recursion
•allInstances() Problem:
– Person.allInstances()allowed
– not allowed for infinitetypes such as
Integer.allInstances()
Dr. Birgit Demuth MINE Summer School, Nida, 2009 41

42. Building complete models with OC
L
• Statechart diagram •
Interaction diagram
•
Interaction diagram
• Activity diagram
•Com
p
onent dia
g
ram
pg
• Use case diagram Dr. Birgit Demuth MINE Summer School, Nida, 2009 42

43. OCL in Statecharts – Example (oclInState())
operation on all objects (Typ OclAny)
lIStt( OlStt) B l
oc
lI
n
St
a
t
e
(
s:
O
c
lSt
a
t
e
)
:
B
oo
l
ean
c
ontext Vector::removeElement(d:Data)
pre: oclInState(notEmpty)
p
ost: size@
p
re = 1 im
p
lies
o
clInState(em
p
t
y
)
Dr. Birgit Demuth MINE Summer School, Nida, 2009 43
ppp
py

44. Undefined Values in OCL Undefined Values in OCL • An OCL expression can evaluate to „undefined“ (OclVoid)
For example: Access to an attribute value or navigation
–
For example: Access to an attribute value or navigation where no value is existent in the respective object
•Strictness Principle
– Whenever a subexpression of an OCL expression
evaluates to undefined, then the whole term evaluates to evaluates to undefined, then the whole term evaluates to undefined
–Exceptions
T dfid T
•
T
rue

or

un
d
e
fi
ne
d
=
T
rue
• False and undefined = False
•False im
p
lies undefined = True
Dr. Birgit Demuth MINE Summer School, Nida, 2009 44
p

45. T
he OclVoid Type
•
Undefined value is the only instance Undefined value is the only instance
• Operation for testing if the value of an expression is
undefined
oclIsUndefined(): Boolean
--
true if the object is undefined true if the object is undefined
-- otherwise false
Dr. Birgit Demuth MINE Summer School, Nida, 2009 45

46. Some Tips for Writing OCL Expressions Constraints should be easy to read and write:
• Avoid complex navigation expressions
h
•C
h
oose appropriate context
• Avoid allInstances()
•
Split and
“
constraints by writing multiple constraints
•
Split
„
and constraints by writing multiple constraints
• Use the „collect“ shorthand • Use association end names (role names) instead of
association names in modeling
Dr. Birgit Demuth MINE Summer School, Nida, 2009 46

47. Typical Use Cases for OCL
Model Layer Examples
Metamodels: {MOF-, Ecore-based} X {UML, CWM, ODM, SBVR, PRR, DSLs}
M2
(Metamodel)
•Specification ofWFRsin OMG standards
•Definition ofModeling Guidelinesfor DSLs
•Specification o
f
Model Transformations
M1 (Model)•Model Verification (ÆCASE-Tool)
•
Evaluation
of
modeling
guidelines
Evaluation
of
modeling
guidelines
•Execution of model transformations
•Specification ofBusiness Rules/Constraints
•Specification o
f
Test Cases
M0
(
Ob
j
ects
)
•Evaluation of Business Rules/Constraints
•
Testing
Dr. Birgit Demuth MINE Summer School, Nida, 2009 47
(j )
Testing

48. Examples for OCL on Metamodel
• WFR in UML metamodel
context Classifier inv: n
ot self.allParents
-
>
includes
(
self
)
()
--Generalization cycles are not allowed
•
UML modeling guideline for Java developers
•
UML modeling guideline for Java developers
context Classifier inv SingleInheritance: self.generalization->size()<= 1 -- Multiple inheritance is not allowed
Dr. Birgit Demuth MINE Summer School, Nida, 2009 48

49. Some UML/OCL Tools • 12 OCL tools/libraries (see OCL Portal) •
Integrations
into
UML
environments
•
Integrations
into
UML
environments
–MagicDraw Enterprise Edition v16.5
– Borland Together2008 (OCL/QVT)
–Eclipse MDT/OCL fo
r
EMF Based Models
–ArgoUML
–
Fujaba4Eclipse Fujaba4Eclipse
Dr. Birgit Demuth MINE Summer School, Nida, 2009 49

50. Decennial Anniversary of Dresden OCL in 2009 Dr. Birgit Demuth MINE Summer School, Nida, 2009 50

51. Dresden OCL2 for Eclipse
Dr. Birgit Demuth MINE Summer School, Nida, 2009 51

52. Dresden OCL2 for Eclipse
Dr. Birgit Demuth MINE Summer School, Nida, 2009 52

53. XMI Import intoDresden OCL2 for Eclipse •TopCased (EMF UML2 XMI)
• MagicDraw (EMF UML2 XMI)
ld( )
•Visua
l
Para
d
igm
(
EMF UML2 XMI
)
• Eclipse UML2 / UML2 Tools (EMF UML2 XMI) Dr. Birgit Demuth MINE Summer School, Nida, 2009 53

54. OCL Support in MagicDraw Enterprise Edition “OCL validation rules” (based on Dresden OCL2 Toolkit)
1. Specification on UML metamodel (M2) /
Verification on UML models (M1)
2. Specification of Stereotypes (M2) /
Verification of UML models (M1)
3. Specification on UML models (M1) /
Verification of UML instances (objects)
Dr. Birgit Demuth MINE Summer School, Nida, 2009 54

55. Dr. Birgit Demuth MINE Summer School, Nida, 2009 55

56. Dr. Birgit Demuth MINE Summer School, Nida, 2009 56

57. Dr. Birgit Demuth MINE Summer School, Nida, 2009 57

58. Dr. Birgit Demuth MINE Summer School, Nida, 2009 58

59. Acronyms OCL
OMG
MOF
Object Constraint Language Object Management Group Mt
Obj t F ilit
MOF PRR QVT
M
e
t
a-
Obj
ec
t F
ac
ilit
y
Production Rule Representation
Query Views Transformation
QVT UML WFR
Query Views Transformation Unified Modeling Language Well-Formedness Rule
Dr. Birgit Demuth MINE Summer School, Nida, 2009 59

60. Thank you
f tt ti ! f
or

your

a
tt
en
ti
on
!
Dr. Birgit Demuth MINE Summer School, Nida, 2009 60