exam in discrete math

A1Homework_01

FrmlMeth.SoftwareEXLSGroupCASpringSemester2018CO-4262018-738AM.zip

Home >Mathematics homework help >Calculus homework help >exam in discrete math

Overview5.html

This unit (which will go over 3 weeks) will introduce you to Object Constraint Language (OCL)

Learning Objectives: Related course level objectives: 2 & 5 (Note LO4 measures Course Outcome 5)

The student will be able to explain what OCL is and what it is used for.
The student will be able to identify the 6 types of OCL expressions and how they are used.
The student will be able to define the 4 types of constraints in OCL.
The student will be able to apply OCL to a small system model expressed in UML

To achieve the learning objectives of this module, you must do the following:

Go to the OCL Center and explore the site. On the homepage, look at the “More on OCL on this site” section and follow all the links under that heading.
Read chapters 1-3 in The Object Constraint Language Second Edition.
Read all the notes in this module.
Read the OMG OCL 2.4 Specification.
Do the the OCL assignment.
Participate and lead (start threads and reply to threads) the discussion on OCL in the Discussion Tool.
post your presentation.
grade other students presentations.
Prepare for Exam 2 by reviewing the material we have covered since the Midterm Exam.

InterpretingOCL.pdf

Interpreting the Object Constraint Language

Ali Hamie, John Howse and Stuart Kent Division of Computing,

University of Brighton, Lewes Rd., Brighton, UK. e-mail: [email protected]

Abstract

The Object Constraint Language (OCL), which forms part of the UML 1.1. set of modelling notations is a precise, textual language for expressing constraints that cannot be shown in the standard diagrammatic notation used in UML. A semantics for OCL lays the foundation for building CASE tools that support integrity checking of whole UML models, not just the component expressed using OCL. This paper provides a semantics for OCL, at the same time providing a semantics for classes, associations, attributes and states.

1: Introduction

The Object Constraint Language [1][2] is a precise textual language to complement graphical languages in modelling object-oriented systems. It allows constraints on the model to be expressed, that can not be expressed using standard diagrammatic notations. Specifically, OCL supports the expression of invariants and pre/post conditions, allowing the modeller to specify precise and detailed constraints on the behaviour of a model, without getting embroiled in implementation detail.

OCL is the culmination of recent work in OO model- ling [3][4] which has selected ideas from formal methods to combine with diagrammatic, object-oriented modelling resulting in a more precise, robust and expressive notation. Syntropy [3] extended OMT [5] with a Z-like textual lan- guage for adding invariants to class diagrams and annotat- ing transitions on state diagrams with pre/post conditions. OCL adopts a simple non-symbolic syntax and restricts itself to a small set of core of concepts.

One of the most important aspects of OCL is that it is part of the Unified Modelling Language [6], which has recently become the global standard modelling language,

under the auspices of the Object Management Group. As a result it is likely to get much greater exposure and use than previously proposed formal specification languages such as VDM [7] and Z [8], and work invested in ensuring that it is correct and appropriate for its purpose is therefore more likely to reap a dividend than work on the aforemen- tioned languages.

The purpose of this paper is to provide a semantics to check that OCL is unambiguous and to improve OCL [9]. As OCL does not exist in a vacuum, but instead depends on some parts of a model to be defined already in dia- grams, this necessitates a semantics for a kernel of the UML diagrammatic notation, specifically: class diagrams. Thus OCL provides a focus for integrating the semantics of the diagrammatic notations. We present one such inte- grated semantics, which we hope lays the foundation for building CASE tools that support integrity checking of whole UML models, not just the component expressed using OCL.

Semantics work [10][11] for OO modelling notations in widespread use, such as OMT or UML, is generally restricted to capturing the meaning of those notations, so accompanying precise textual languages have yet to be considered, as languages such as OCL have only very recently been incorporated. Exceptions to this are the work of Bicarregui et al. [12][13] which uses the Object Calcu- lus [14] to develop a semantics for Syntropy [3], and our own work [15][16][17][18][19].

We have chosen to use Larch [20]. This choice is motivated in part by the desire not to be engaged in the design of logics and reasoning systems, but instead to focus on elaborating the meaning of the modelling nota- tions themselves. Larch is a stable language with a well- developed supporting toolset. It uses first-order predicate logic, rather than temporal logic, so is accessible to a wider audience, which includes, hopefully, some commercial tool developers. It is also close to technologies most likely to leverage the sophisticated CASE tools that should result

from increasing the precision and expressiveness of mod- elling notations. This is illustrated by the inclusion of an automated proof assistant in its accompanying toolset. We have also been using our Larch-based semantics as a start- ing and subsequent reference point for developing check- ing and animation tools in Prolog.

The paper is organised as follows. Section 2 is an informal introduction of using OCL, in combination with a kernel of the UML diagrammatic notation (class dia- grams), in writing navigation expressions in object-ori- ented modelling. Section 3 establishes the semantic framework by giving a semantics to class diagrams. Sec- tion 4 defines the semantics of OCL expressions. A key aspect of this is a semantics for navigation expressions, including navigation over collections other than sets, such as sequences and bags, and the semantics of filters. Section 5 deals with system states. Section 6 summarises the semantics of invariants and pre/post conditions (expressed in OCL). Section 7 summarises the general mapping of the UML/OCL elements considered. Section 8 concludes with an overview of future work in semantics and elsewhere.

2: Navigation in OO Modelling

Navigation in OO modelling means following links from one object to locate another object or a collection of objects. It is possible to navigate across many links, and hence to navigate from a collection to a collection. Naviga- tion is at the core of OCL. OCL expressions allow us to write constraints on the behaviour of objects identified by navigating from the object or objects which are the focus of the constraint. At the specification level, the expressions appear in invariants, preconditions and postconditions.

2.1: Example model

Figure 1 presents a small, contrived example of a class dia- gram in UML for a simple system that supports scheduling of offerings of seminars to a collection of attendees by pre- senters who must be qualified for the seminars they present. A full description of the notation can be found in [6][21].

2.2: Navigating from single objects

Navigation expressions start with an object, which can be explicitly declared or given by a context. For example, a declaration s : Seminar means that s is a variable that can refer to an object taken from the set of objects conforming to type Seminar. Here, the type name is used to represent the set of objects in the model that conform to the type.

A navigation expression is written using an attribute or role name, and an optional parameter list. Given the ear- lier declaration, the OCL expression s.title represents the value of the attribute title for the object represented by s. An OCL expression can also use the name self to refer to a contextual instance. In the following example, self refers to an instance of seminar:

Seminar self.title

Navigating from an object via an association role can result in a single object or a collection, depending on the cardinality annotations of the association role. For exam- ple, given the declaration p : Presenter, the expression p.qualifiedFor results in a set of seminars p is qualified to present.

The association between Seminar and Offering has the annotation {ordered} on the offering role. As a result, the expression s.offering, where s is a seminar, results in a sequence. Notice that this means that the operator “.” is overloaded, because it can map an object to a set, to a bag, or to a sequence.

2.3: Navigating from collections

Assume we have the following declaration p:Presenter. The navigation expression p.qualifiedFor.title (also writ- ten p.qualifiedFor->collect(title) in OCL) involves navi- gating first from a single object and then from a collection, namely the set of seminars for which presenter p is quali- fied. This is because the expression parses as (p.qualifiedFor).title. The result of this expression is a bag obtained by applying title to each member of the set p.qualifiedFor. The OCL operation asSet can be used to convert this bag to a set. Similarly, navigating from a bag

Figure 1. Class diagram for a seminar scheduling system

S e m i n a r S c h e d u l i n g S y s t e m

title: String S e m i n a r

n a m e : S t r i n g P r e s e n t e r

n a m e : S t r i n g A t t e n d e e

g o i n g A h e a d : B o o l e a n d a t e : D a t e

Offering

� �

�

qualifiedFor

qualified ��

�

� �

{ o r d e r e d }

yields a bag and navigating from a sequence yields a sequence.

2.4: Invariants

Navigation expressions can be part of an invariant on a type which must be true for all instances of that type at any time. For example, an invariant for the seminar scheduling system would be:

Presenter

self.qualifiedFor->includesAll(self.offering.seminar)

which says that a presenter must be qualified for all semi- nars he/she is assigned to present.

2.5: Preconditions and postconditions

An OCL expression can also be used as a precondition or postcondition, which are used to specify the behaviour of an operation or method. The name self can also be used in the expression referring to the object on which the opera- tion was called. Expressions occurring in a postcondition can refer to two sets of values for each property of an object:

• the value of a property at the start of the operation or method

• the value of a property upon completion of the opera- tion or method

In OCL the value of a property at the start of the oper- ation is denoted by postfixing the property name with the commercial sign @, followed by the keyword pre.

Figure 2 gives the specification of an operation markAsAbsent in terms of pre/post conditions. This oper- ation marks a presenter as absent by cancelling his/her pre- sentations within specific dates.

3: Semantics: Class Diagrams

We shall use the Larch Shared Language (LSL) [20] to provide the semantics of OCL expressions. This is achieved by first providing the semantics of object types,

attributes, and associations. LSL uses specification mod- ules, called traits, to describe abstract data types and theo- ries.

3.1: Object types

An object type is a description of a set of objects in terms of properties and behaviour they all share. In our formali- sation, an object type is associated with an LSL basic sort consisting of elements that uniquely represent objects (instances) of the type, which can be thought of as object identifiers. The attributes of an object type are formalised as functions on the sort representing this type.

The object type Presenter in Figure 1 is interpreted as a basic sort denoted by , namely a sort of presenter identifiers. The attribute name is interpreted as a function with signature

, which is added to the specification for object type Presenter. The type String is interpreted as the sort of strings which is avail- able in the Larch HandBook of specification modules [20]. In a very similar way we interpret the other object types for the seminar scheduling system.

3.2: Associations

We now extend the interpretation of object types and attributes given in the previous section to include binary associations. Associations are basically relationships between objects. Each association in a class diagram has two role names which can be used to navigate the associa- tion from a specific object to refer to other objects and their properties. For instance, the association between Pre- senter and Seminar (Figure 1) has two role names quali- fied and qualifiedFor.

We formalise associations between object types as two related functions that map an object of one type to the set of associated objects of another (or the same) type. These mappings are specified in a way that is independent of the structure of types they associate. Thus we have a generic Larch theory for associations that can be renamed to specify each particular association in the model. For example, the association between Presenter and Seminar would be represented as two functions and

with the signatures:

where and are the

power sorts of and respectively. By choosing power sorts for the domains and ranges of

SeminarSchedulingSystem

markAsAbsent(p : Presenter, from, to : Date)

pre: true

post: p.offering@pre->forAll( o |

o.date >= from and o.date <= to implies

o.presenter = Set{})

Figure 2.Specification of operation markAsAbsent

Presenter

name

name : Presenter String→

String

qualified

qualifiedFor

qualified : Set Seminar[ ] Set Presenter[ ]→

q u a l i f i e d F or : S e t P r e s e n t e r[ ] S e t S e m i n a r[ ]→

Set Seminar[ ] Set Presenter[ ] Seminar Presenter

these mappings, we have a uniform treatment of associa- tions which simplifies the formalisation and provides generic theory for associations. In the case of an optional association (0..1 cardinality), this is especially useful to check whether there is an object or not when navigating the association, namely whether the resulting set is empty or not. The case where navigation is from a single object is subsumed with the general case where the set is a singleton containing that object. The corresponding functions that map single objects can be defined in terms of those that map sets of objects (see later).

The two functions and satisfy the axioms:

The operation is the union operation on sets. Note that these axioms imply that these functions are completely determined by their values at singleton sets.

In order to represent the association, these functions are related by the following axiom:

Intuitively, this axiom asserts that if instructor p is quali- fied to present seminar s, then p must be included in the set of presenters qualified to present s.

The corresponding functions that operate on single objects may be constructed from those whose domains are power sorts as follows:

Semantically, navigating from a single object is equivalent to navigating from a singleton set containing that object.

For further details and for the generic traits of object types and associations the reader is referred to [15][17].

4: Collections and their operations

Collection as defined in OCL is an abstract type, with con- crete collection types as its subtypes; Set, Sequence, and Bag. This type is not strictly necessary since it is defined as an abstract supertype.

The Collection type can be specified in LSL by a sort and including the signatures of the com-

mon operations shared between its subtypes and some of their axioms. Let be the sort of collec-

tions of type . For example, the size operation which

common to all collection types has the signature and is specified in

terms of the operation iterate. The collection types (Set, Bag, and Sequence) can be specified in LSL as abstract data types with the familiar operations. For example, LSL provides traits (available in the Larch HandBook) for spec- ifying these mathematical abstractions. The additional operations provided by OCL will be dealt with in the next subsection.

The Larch Shared Language does not support subsort- ing. So in order to assert that is a subtype of

we use the function

that maps a set into a collection representing it. The assertion that Bag[T] and Sequence[T] are subtypes of Collec- tion[T] can be handled in a similar way by overloading the function . For bags we have

. The

size operation has to be specified on by includ-

ing the signature together with the axiom:

similarly, we specify size for bags and sequences. There are many operations defined on collection

types in OCL. These operations transform existing collec- tions into new ones. Here we consider the more interesting ones, namely select, reject, collect, forAll, exists and iterate.

4.1: Select and reject operations

The select and reject operations provide a way of specify- ing a subset of a collection. A select is an operation on a collection and is specified using the ->-syntax:

collection -> select( v : T | b-expr-v)

where the variable v is called the iterator and b-expr-v is a boolean expression. This expression is evaluated by using v to iterate over collection and evaluating b-expr-v for each v. The v is a reference that refers to the objects from the collection.

The meaning of select expressions can be obtained by defining two function and with the signa-

tures

and respectively. The function is defined

as . That is each boolean expression induces a function. The select operation applied to a set always results in a set, and the same applies for bags and sequences. Hence, the meaning of the operation has to be specified for sets, bags and sequences.

qualified

qualifiedFor

qualified {}( ) {}=

qualifiedFor {}( ) {}=

qualified s s '∪( ) == qualified s ( ) qualified s '( )∪

qualifiedFor s s '∪( ) == qualifiedFor s ( ) qualifiedFor s '( )∪

∪

s qualifiedFor p { }( ) == p qualified s { }( )∈∈

qualified s ( ) == qualified s { }( )

qualifiedFor p ( ) == qualifiedFor p { }( )

Collection

Collection T [ ]

size :Collection T [ ] Integer→

Set T[ ] Collection T [ ] toCollection : Set T[ ] Collection T [ ]→

toCollection

toCollection : Bag T[ ] Collection T [ ]→ Set T[ ]

size : Set T[ ] Intege r→

size s( ) size toCollection s ( )( )=

select p

: Collection T[ ] Collection T[ ]→

p : T Bool→ p p v( ) == b-expr-v

For sets we define a function with the sig-

nature and satisfies the

axioms:

where is a boolean function defined as above. In addi- tion we have the axiom:

For example, p.offering->select(goingAhead) is inter- preted as , where

goingAhead is interpreted as a function with the signature .

For bags and sequences similar functions can be defined with similar axioms, the only difference is the sig- natures of these functions.

The reject operation is similar to the select opera- tion, but with reject we get the subset of all the elements for which the boolean expression evaluates to False. In fact reject can be interpreted in terms of select because the expression collection->reject(v:T | b-expr-v) is equivalent to collection->select(v : T | not(b-expr-v)).

4.2: Collect operation

The select and reject operations always yield a sub-col- lection of the original one. However, it is often required to specify a collection which is derived from some other col- lection, but which contains different objects from the origi- nal collection. The collect operation provides such construct in OCL. The syntax of collect is written as fol- lows:

collection -> collect(v : T | expr-v )

The value of the collect operation is the collection of the results of all the evaluations of expr-v.

The meaning of collect expressions can be obtained by defining two functions and f with the sig-

natures

respectively. The function f is defined as . In OCL the result of the collect operation on a set is a

bag rather than a set. So we define which satisfies the axi-

oms:

However, if it is required that collect on a set should result in a set rather than a bag, then we can make a set from the bag by using the function which satisfies the axioms:

For bags we define

which satisfies similar axioms as the one for sets. For sequences, we define

which also satisfies similar axioms as the one for sets, where the only difference is that the result is a sequence.

4.3: Navigation expressions

In OO modelling navigating from a collection of objects is very common. For this reason OCL provides a shorthand notation for the operation collect. Instead of writing self.qualifiedFor->collect(title) we can write self.quali- fiedFor.title. In OCL applying a property to a collection of objects is interpreted as a collect over the members of the collection with the specified property.

So, for any propertyname of objects in a collection, the following expressions are identical

collection.propertyname

collection->collect(propertyname)

In OCL, a collection of collections is automatically flat- tened. Such a view is easy to teach to modellers, but hard to define without falling into traps. In related work we have shown that flattening is not necessary. More informa- tion about this can be found in [9].

4.4: Quantifications

OCL provides two operations for quantifications forAll and exists operations. The forAll operation in OCL allows the specification of a boolean expression, which must hold for all objects in a collection. Its syntax is given by:

collection -> forAll( v : T | b-expr-v )

The value of a forAll expression is boolean. The result is true if the boolean expression b-expr-v is true for all ele- ments of collection. The result is false if b-expr-v evalu- ates to false for one or more v in collection.

select p

: Set T[ ] Set T[ ]→

Select p

{}( ) == {} select

p insert v s ,( )( ) == if p v( ) then

insert v select p

s( ),( ) else select p

s( )

toCollection select P

s( )( ) select

p toCollection s ( )( )

select goingAhe ad offering p ( )( )

goingAhead : Offering Bool→

collect f

: Collection T [ ] Collection S [ ] f : T S→

→

f v( ) = expr-v

collect f

: Set T[ ] Bag S[ ]→

collect f {}( ) == {} collect f insert v s ,( )( ) == insert f v( ) collect f s( ),( )

toCollection collect p

s( )( ) == collect

p toCollection s ( )( )( )

asSet : Bag T[ ] Set T[ ]→

asSet {}( ) == {} asSet insert v b ,( )( ) == insert v asSet b ( ),( )

collect f : Bag T[ ] Bag S[ ]→

collect f : Seq T[ ] Seq S[ ]→

The semantics of forAll can be given by using LSL universal quantification denoted by . So the forAll expres- sion is interpreted as:

The semantics of exists can be given in a similar way.

4.5: Iterate operation

OCL also has the iterate operation which is very generic in the sense that the operations select, reject, forall, exists, and collect can all be described in terms of iterate. The syntax of iterate is:

collection->iterate(v : T; acc:S = expr | expr-v-acc)

The iterate operation is evaluated by using v to iterate over the collection and the expr-v-acc is evaluated for each v. After each evaluation of expr-v-acc, its value is assigned to acc. In this way the value of acc is built up during the iteration of the collection.

The meaning of iterate expressions can be obtained by defining

and , where .

For sets the function satisfies the axioms:

where delete is the operation for removing an element from a set. These axioms are only valid for functions that satisfy the properties:

Without these axioms we can have two equal sets and

where is not equal to . This is clearly not consistent with the notion of substituting equals for equals. So if does not satisfy these properties, the operation iterate is not deterministic. For bags and sequences we can define similar functions which satisfy similar axioms.

5: System state

So far we have ignored system state, which is required in the presence of dynamic behaviour, as specified for exam- ple through preconditions and postconditions on opera- tions. Thus we enrich the semantic model with a sort of system state . Given this, we introduce, for each object

type T, a function which returns the set of existing objects of type T (i.e. those that have been created

and not destroyed) in a given state σ. This function is used to interpret the allInstances feature of an object type, which returns the set of all instances of the type. For exam- ple, T.allInstances is interpreted as the set .

Attributes of a given object type are interpreted as functions with additional argument for the system states. For example, the attribute title is now interpreted as a func- tion . And similarly for associations.

6: Invariants, preconditions and postconditions

We interpret invariants by interpreting each expression occurring in it and adding universal quantifications. For example, for the invariant given earlier, the self.qualified- For is interpreted as , and self.offering.seminar is interpreted as

. So the invariant is interpreted as the following assertion:

That is, the invariant must hold in every system state σ. We interpret pre/post conditions by interpreting each

expression occurring in them. For example, the postcondi- tion of the operation markAsAbsent is interpreted by interpreting p.seminar@pre as , and the predicate part of forAll as

. The whole postcondition is interpreted as:

where and are the states before and after the opera- tion is executed respectively.

7: Summary of mapping

In this section we summarise the mappings between OCL types and expressions and the sorts and expressions of LSL.

For each type A in a class diagram we associate with it a sort of all possible object identities that conform to the type, denoted by . We define a mapping

by . That is, τ(A) is the sort associated with the type A. For example, we have τ(Seminar) =def Seminar .

The basic value types in OCL are mapped directly to predefined sorts in LSL. The type Boolean is mapped to

∀

v : T∀( ) v collection b - r -vexp⇒∈( )

iterate f rexp, : Collection T [ ] S→

f : T,S S→ f v acc,( ) == r -v -accexp iterate f rexp,

iterate f rexp, {}( ) == r i

exp

terate f rexp, insert v s ,( )( ) == f v iterate f rexp, delete v s,( )( ),( )

f x y,( ) f y x,( ) f x f y z,( ),( ) f f x y,( ) z,( )

= =

s 1

s 2 iterate s 1( ) iterate s 2( )

Σ T : Σ Set T[ ]→

T σ( )

title : Seminar Σ, String→

qualifiedFor self σ,( )

seminar offering self σ,( ) σ,( )

p : Presenter , σ : Σ∀ seminar offering self σ,( ) σ,( )( )

qualifiedFor self σ,( ) ⊆

seminar p σ,( )

pred o σ,( ) == date o σ,( ) from≥ date o σ,( ) to≤∧

o : Offering , σ σ' : Σ,( )∀( ) o Offering σ( )∈ pred o σ,( )∧ presenter p σ',( ) {}=⇒

( )

σ σ'

τ : OclType lslSort→ τ A( ) =A

the sort Bool , i.e. τ(Boolean) =def Bool , which is speci- fied as a trait in the Larch HandBook of specifications. The type Integer is also mapped to a predefined sort in LSL namely Integer , i.e τ(Integer) =def Integer . Similarly we have τ(String) =def String . Enumerated types are also mapped directly to LSL enumerated sorts.

For collection types such as sets, bags and sequences, LSL provides basic traits that specify basic operations on these structures. However, these traits need to be extended to deal with new operations available in OCL. These traits can be constructed by including the traits that specify oper- ations like select, reject, iterate, etc.. For the moment we map the types Set(T), Bag(T), and Sequence(T) to the sorts Set[T] , Bag[T] , and Seq[T] respectively.

For each attribute att of type T of an object type A we associate with it a function symbol denoted by att . For this we define a mapping α� which maps an attribute sym- bol to a function symbol in LSL, by α�(att:T) =def

. Operations or queries on type A such as op(S):T of type T, are mapped as: α�(op(S):T) =def

For each association role r (at the right) of an associa- tion between two types A and B we associate a function symbol in LSL. For this we define a mapping ρ� by ρ�(r:set[B]) =def . Parameterised

(qualified) association roles are dealt with in a similar way. The table in Figure 3 summarizes the above mappings.

We now define a mapping µ with signature

that maps OCL expressions to LSL expressions based on the above mappings. The definition of µ is given in Figure 4. The interpretation of an OCL expression as given by µ is given at a moment in time corresponding to a sys- tem state . In this definition, variables in OCL are mapped into variables in LSL, i.e. µ(v) = v. Expressions of the form v.att are mapped to . Expressions of the form c->collect(v : T | expr-v), where c is a collection and expr-v is an expression involving v, are mapped to

, where is the interpretation of

c, and f(v) = µ(expr-v). The only exception is where the expression is a role name, in which case c->collect(r) is interpreted as .

Value expressions true and false are mapped to true and false respectively. Set expressions such as Set{}, Set{1,2} are mapped to {} and { 1,2 } , syntactic sugar for insert(1,insert(2,{})) , respectively. Other value expressions are mapped in a similar way.

8: Conclusions

A precise semantics for a subset of OCL expressions together with the semantics for a kernel of the UML dia- grammatic notation – class (type) diagrams, has been defined in terms of Larch. We have achieved nearly com- plete coverage of the OCL, although details have been omitted in some cases. Through this semantics, we have

OCL LSL

A (object type) A (sort of object identities)

T (value type) T (sort of values)

Boolean Bool

String String

Integer Integer

Collection(T) Collection[T]

Set(T) Set[T]

Bag(T) Bag[T]

Sequence(T) Seq[T]

att:T (attribute)

op(S) :T

r : set[B] (role)

r (S) : set[B] (role)

r : B (role)

r (S) : B (role)

Figure 3. Mappings of types, attributes and associations

att : A Σ, T→

op : A S Σ, T→,

att : A Σ, T→

op : A S Σ, T→,

r : Set A[ ] Σ, Set B[ ]→

r : Set A[ ] S Σ, Set B[ ]→,

r : Set A[ ] Σ, Set B[ ]→

r : Set A[ ] S Σ, Set B[ ]→,

r : set A[ ] Σ, set B[ ]→

OCL expressions LSL expressions

v (variable) v (variable)

v.att att(v, σ)

v.op(v’) op(v,v’, σ)

v.r (r role name) r(v, σ)

c->select(v | b-expr-v) select p(c, σ) , where p(v, σ)= µ( b-expr-v)

c->reject(v | b-expr-v) reject p(c, σ) ,where p(v, σ)= µ( b-exp-v)

c->collect(v | exp-v) collect f (c, σ) , where f(v, σ)= µ( exp-v)

c->iteate(v;acc=exp | expr-v-acc)

iterate f,exp (c, σ) , where f(v ,acc ,σ)= µ( expr-v-acc)

c.r (c collection, r role) r(c, σ) , (µ( c)= c )

Figure 4. Definition of the mapping µ

µ : OclExpression lslExpression→

att a σ,( )

collect f

c σ,( ) µ c( ) = c

r c σ,( )

established that there is no need for flattening collection of collections when navigating from collections. We have not considered meta level features in OCL, such as type casting and interrogation queries on objects. How- ever, it is relatively a simple matter to formalise these in Larch. Future semantics work includes:

• Semantics for constraint diagrams [18][19], a dia- grammatic notation that allows most, if not all, OCL expressions to be given a diagrammatic characterisa- tion.

• The use of this kernel to give the semantics of other aspects of UML. In particular state diagrams may be mapped to class diagrams with additional constraints expressed in OCL.

• Also being worked on is the semantics of extensions to UML suggested by Catalysis [4]. We are using the Larch trait inclusion mechanism to define the seman- tics of framework composition; and are working out the proof obligations for establishing conformance relationships between models, in particular between the specification and design in a refinement.

Apart from establishing precise, core concepts and check- ing the integrity and well-definedness of modelling nota- tions, the semantics effort is also aimed at establishing a foundation for building CASE tools. We are currently experimenting with checking and animation tools written in Prolog, where the mapping from model to Prolog has benefited considerably from the work in Larch.

Acknowledgements

Thanks for comments are due to colleagues on the BIRO project at Brighton, in particular Franco Civello and Rich- ard Mitchell. This research is funded by the UK EPSRC under grant number GR/K67304.

References

[1] Rational Software Corporation, Object Constraint Language Specification, Version 1.1, http://www.rational.com, 1997.

[2] A. Kleppe, J. Warmer, and S. Cook, “Informal Formality? The Object Constraint Language and its application in the meta- model”, Proc. of UML’98 International Workshop, P. Muller and J. Bezivin, ed., Mulhouse, France, June 3-4, 1998, pp. 127-136.

[3] S. Cook, and J. Daniels, Designing Object Systems: Object- Oriented Modelling with Syntropy, Prentice-Hall, Hemel Hemp- stead, UK, 1994, p. 389.

[4] D. D'Souza, and A. Wills, Objects, Components and Frame- works with UML: The Catalysis Approach, book submitted for publication by Addison-Wesley, UK, 1998, also available at http:/ /www.trireme.com/catalysis.

[5] J. Rumbaugh, M. Blaha, W. Premerali, F. Eddy, and W. Lorensen, Object-Oriented Modelling and Design, Prentice-Hall, Emglewood Cliffs, New Jersy, 1991, p. 500.

[6] Rational Software Corporation, The Unified Modeling Lan- guage, Version 1.1, http://www.rational.com, 1997.

[7] C. Jones, Systematic Software Development using VDM (2nd edition), Prentice-Hall, Hemel Hempstead, UK, 1990, p. 333.

[8] M. Spivey, The Z notation (2nd ed.), Prentice Hall, UK, 1992.

[9] A. Hamie, F. Civello, J. Howse, S. Kent, and R. Mitchell, “Reflections on the Object Constraint Language”, Proc. of UML’98 International Workshop, P. Muller and J. Bezivin, ed., Mulhouse, France, June 3-4, 1998, pp. 137-145.

[10] H. Bourdeau, and B. Cheng, “A Formal Semantics for Object Model Diagrams”, IEEE Transactions on Software Engi- neering, Vol. 21, No. 10, 1995, pp. 799-821.

[11] R. France, J. Bruel, M. Larrondo-Petrie, and M. Shroff, “Exploring The Semantics of UML Type Structures with Z”, Proc. Int’l Workshop on Formal Methods for Object-Based Dis- tributed Systems (FMOODS’97), Chapman and Hall, London, 1997, pp. 247-260.

[12] J. Bicarregui, K. Lano, and T. Maibaum, “Towards a Com- positional Interpretation of Object Diagrams”, Proc. IFIP TC2 Working conference on Algorithmic Languages and Calculi, Chapman and Hall, 1997.

[13] J. Bicarregui, K. Lano, and T.S.E Maibaum, “Objects, Asso- ciations and Subsystems: a hierarchical approach to encapsula- tion”, Proc. European Conf. of Object-Oriented Programming (ECOOP'97), LNCS 1241, Springer-Verlag, 1997, pp. 324-343.

[14] J. Fiadeiro, and T. Maibaum, “Temporal Theories and Mod- ularisation Units for Concurrent System Specification”, Formal Aspects of Computing, Springer-Verlag, Vol. 4, No. 3, 1992, pp. 239-272.

[15] A. Hamie, and J. Howse, “Interpreting Syntropy in Larch”, Tech. Report ITCM97/C1, Computing Division, University of Brighton, Brighton, UK, 1997.

[16] A. Hamie, J. Howse, and S. Kent, “Navigation Expressions in Object-Oriented Modelling”, Proc. of FASE in ETAPS98, LNCS, 1382, Springer-Verlag, 1998, pp. 123-137.

[17] A. Hamie, J. Howse, and S. Kent, “Modular Semantics of Object-Oriented Models”, to be published in the proceedings of the Third Northern Formal Methods WorkShop, UK, 1998.

[18] S. Kent, “Constraint Diagrams: Visualising Invariants in Object-Oriented Models”, Proc. of OOPSLA97, ACM Press, 1997.

[19] S. Kent, “ Visualising Contracts in Object-Oriented Mod- els”, Proc. VISUAL98 in ETAPS’98, Lisbon, Portugal, 1998.

[20] J. Guttag, and J. Horning, Larch: Languages and Tools for Formal Specifications, Springer-Verlag, 1993.

[21] M. Fowler, and K. Scott, UML Distilled, Addison-Wesley, 1997, p. 179.

OCLpaper.pdf

Enhancing the Object Constraint Language for More Expressive Specifications

Ali Hamie Division of Computing University of Brighton

Lewes Road, Brighton, UK +44 1273 642032

[email protected]

ABSTRACT The Object Constraint Language (OCL) is a precise language which could be used for describing constraints on object-oriented models and other modelling artifacts. The kind of constraints which can be described using OCL include invariants on classes, types and interfaces, preconditions and postconditions of operations and methods. This paper describes some enhancements to OCL that make specifications convey information more effectively. For example, adding redundant invariants, time- based constraints, postconditions, and examples could make the specification clearer to readers, and can be used in showing that the specification says what is intended. Another example of an enhancement is the use of case analysis sugar which splits up a specification into manageable parts. These enhancements have been already integrated in some specification languages such as Larch/ C++, a larch style behavioral interface specification language for C++.

Keywords UML, OCL, constraints, specification, modelling

1 INTRODUCTION The Object Constraint Language (OCL) [10][21][24][25] is a specification language for describing constraints on object-oriented models. It is an optional part of the Unified Modelling Language (UML) [22][5] which is the de facto standard for object-oriented analysis and design. OCL allows constraints on a UML model to be expressed, that can not be easily expressed using standard diagrammatic notations. Specifically, OCL supports the expression of invariants on classes and types, preconditions and postcon- ditions on operations, allowing the modeller to specify pre-

cise and detailed constraints on the behaviour of a model, without getting embroiled in implementation details. Kent [11] has developed a diagrammatic notation based on Venn diagrams for describing constraints which could be used in conjunction with UML/OCL.

OCL is the culmination of recent work in OO modelling [2][4] which has selected ideas from formal methods to combine with diagrammatic, object-oriented modelling resulting in a more precise, robust and expressive notation. Syntropy [2] extended OMT [23] with a Z-like textual lan- guage for adding invariants to class diagrams and annotat- ing transitions on state diagrams with preconditions and postconditions. However, OCL adopts a simple non-sym- bolic syntax and restricts itself to a small set of core of con- cepts.

This paper describes some enhancements to OCL which would make specification convey information effectively. One enhancement is to allow the specification of redundant information which could provide a basis for debugging specifications. That is by adding some information which should be implied by the specification would help readers and help check that the specification says what is intended. These enhancements apply generally to the precondition and postcondition approach to specification [13] and they have been integrated with other specification languages such as Larch/C++ [14][15] which is a Larch style behav- ioral interface specification language for C++, and JML (Java Modelling Language) a behavioral interface specifi- cation language for Java [12]. The main contribution of this paper is to incorporate these enhancements into OCL for specifying UML object-oriented models. We extend OCL with time-based constraints. We also extend the enhance- ment of adding redundant specifications with the ability to express equivalent forms of invariants and postconditions.

The paper is organised as follows. Section 2 is an introduc- tion of using OCL, in combination with a kernel of the UML diagrammatic notation (class diagrams), in writing

invariants, preconditions and postconditions. Section 3 introduces redundant specifications into UML/OCL mod- els. Section 4 discusses time-based constraints and the introduction of redundant constraints within OCL. Section 5 deals with case analysis. Section 6 provides a conclusion and further work.

2 THE OBJECT CONSTRAINT LANGUAGE The Object Constraint Language (OCL) [10][21][24][25] is a specification language for describing constraints on object-oriented models. It is developed at IBM and it is an optional part of the object-oriented de facto standard UML. It is based on textual rather than symbolic syntax which makes it more accessible for specifying constraints on object-oriented models than other specification languages such as Z [20] and VDM [9]. The design of OCL is heavily influenced by the work of Cook and Daniels [2] which bor- rows heavily from Z. The constraints which are expressible using OCL are as follows:

• Invariants on Classes or Types that must hold at all times.

• Preconditions which are constraints that must hold before the execution of an operation.

• Postconditions which are constraints that will hold after the execution of an operation under the appro- priate precondition.

• Guards which are constraints on the transitions of an object from one state to another.

The constraints are described in the context of an object- oriented model, that is they cannot be stand alone con- straints. The following example illustrates the use of OCL in describing some of these constraints.

2.1 Example Model

The example we shall use is a class diagram describing a model for a hotel management system. This example is based on the example in [25]. A hotel has a number of rooms that can be rented to guests. There are also a number of bathrooms, which are either associated with a specific room or used by multiple rooms on the same floor. The model is expressed in UML which consists of a set of nota- tions for describing object-oriented models. A full descrip- tion of UML can be found in [22] and a distilled description can be found in [5]. The class diagram introduces a lan- guage of classes, attributes and associations. This language automatically becomes part of OCL and can be used to form expressions. For example, the class names introduced by the class diagram Hotel, Room, etc. become types in OCL. The attribute names such as address, minFloor, maxFloor, etc. also become part of the vocabulary of OCL. Association roles such as hotel, guests, etc. also become part of OCL.

These as we shall see later can be used to form navigation expressions.

2.2 Invariants

The constraints which can be expressed using OCL are always connected to a UML object-oriented model. An invariant is a constraint which can be associated with a class, type or interface in a UML model. The invariant is expressed as a boolean expression which restricts or limits the value of an attribute or association role, or it can state a relationship between the values of attributes and association roles. The result of the expression must be true for all instances of the associated class at any point in time.

A simple invariant on the hotel model is that the number of rooms in a hotel is greater than or equal to one. Such an invariant can be shown in the class diagram as a text between curly brackets in a note box with a dotted line to the associated class as shown in Figure 1. The standard UML stereotype <<invariant>> can be used to indicate an invariant constraint. However, in some cases invariants tend to take up too much space resulting in a cluttered diagram. This is the case when there are a large number of invariants. This can be overcome by writing invariants separately in a

Figure 1. Class diagram for hotel model

H o t e l

address: Strin g n u m b e r O f R o o m s : I n t e g e r minFloor: Integer m a x F l o o r : I n e t g e r

totalRent(): Real

R o o m f l o o r N u m b e r : I n t eg e r r o o m N u m b e r : I n t e g e r n u m b e r O f B e d s : I n t e g e r rent: Real color : Color

p a i n t ( n e w C o l o r : C o l o r )

B a t h R o o m

f l o o r N u m b e r : I n t eg e r r o o m N u m b e r : I n t e g e r usage: Integer

u s e s ( g : G u e s t )

r o o m s

hotel

0..1

G u e s t

n a m e : S t r i n g age : Integer s e x : { m a l e , f e m a l e }

hotel

g u e s t s

r o o m

< < i n v a r i a n t > > { n u m b e r O f R o o m s > = 1 }

text document. For example, the invariant on the class Hotel can be expressed in OCL as follows:

context Hotel invariant:

self.numberOfRooms >= 1

The keyword context specifies the context of the invariant which is the class Hotel in this case. self is a keyword in OCL which represents a contextual object for which the con- straint applies. In this case self refers to an object of class Hotel.

In OCL, self can be omitted because the contextual object is the default. So the above invariant could also be expressed as:

context Hotel invariant:

numberOfRooms >= 1

2.3 Preconditions and Postconditions

The behavior of an operation of a class or type can be pre- cisely specified in terms of a precondition and postcondi- tion pair. The precondition and postcondition are expressed using OCL expressions. The name self can also be used in the precondition or postcondition referring to the object on which the operation was invoked. Expressions occurring in a postcondition can refer to two sets of values for each property of an object:

• the value of a property at the start of the operation or method.

• the value of a property upon completion of the operation or method.

In OCL the value of a property at the start of the operation is denoted by postfixing the property name with the com- mercial sign @, followed by the keyword pre.

As a simple example, consider the specification of the oper- ation increaseRent in terms of precondition and postcondi- tion pair which is given below. This operation increases the rent of a given room by an amount taken as a parameter to the operation.

context Room:: increaseRent(amount : integer)

pre : amount > 0

post : rent = rent@pre + amount

The keyword context indicates the context in which the operation can be applied which is the class Room in this case. The precondition states that the amount must be posi- tive. The postcondition states that the new rent of the room has been increased by amount.

3 REDUNDANT SPECIFICATIONS A redundant specification describes properties which should follow from the main specification. As such, a

redundant specification does not form a part of the main specification, rather it can be regarded as a formalised com- mentary on it. Adding redundant parts to a specification results in a more expressive specification language. That is expressive in the way it conveys information or constraints to the reader. This would allow modellers and specifiers to express properties the model should have, and which are important to readers without cluttering up the main specifi- cation. Another important reason for adding redundant specifications is the ability to check the main specification. For instance, a reader would be able to check his or her understanding of the specification against the redundant parts.

The approach of adding redundant parts of a specification has been incorporated in the Larch family of specification languages [8]. The emphasis was on the benefits of check- ing that a specification meets the specifier’s intuition and intention by comparing the redundant parts against the main parts; such checking is called “debugging” a specification [6]. For example, the Larch Shared Language (LSL) [8] has features which makes it possible to state redundant claims about theories.

In this section we incorporate features into OCL/UML that can be used to state redundant claims and properties about UML models. This would include adding redundant invari- ants, redundant preconditions and postconditions.

3.1 Redundant Invariants

A class or type may have several invariants constraining its objects. The combination of these invariants describes con- straints relating attributes and association roles. Some of the consequences of these relationships could be stated as redundant invariants. In OCL one way to introduce a redun- dant invariant is to have a keyword redundant indicating a redundant property of an object of a given class or type. The following illustrates this:

context Class redundant Invariant :

redundantInvariant

Where Class is a class which provides the context of the redundant invariant redundantInvariant. This states that redun- dantInvariant should follow from the combination of all the invariants on Class.

As an example consider the following simple invariant on the class Hotel:

context Hotel invariant:

self.numberOfRooms >= 1

Which states that the number of rooms in a hotel is greater or equal to one.

Another invariant on the Hotel class is the following which relates the attribute numberOfRooms to the association role rooms:

context Hotel invariant:

self.numberOfRooms = self.rooms->size

This invariant says that the number of objects in the room collection (rooms->size) is equal to the value of the attribute numberOfRooms.

Given these two invariants we could state the following derived or redundant invariant:

context Hotel redundant invariant:

self.rooms->size >= 1

This redundant invariant states that the number of objects in the room collection is greater than or equal to one. It is easy to see that this follows from the two previous invariants by substituting equals for equals.

In order to debug an invariant one is required to prove the following:

invariant implies redundantInvariant

Where invariant is the invariant and invariantRedundant is the redundant invariant. With tool support the specification of a class (collection of invariants) could be checked against redundant properties of the class.

Another form of redundant information is to add equivalent invariants. In OCL we could use the keyword equivalent to add equivalent invariants. For example an equivalent form of the above invariant is:

context Hotel invariant:

self.numberOfRooms = self.rooms->size

equivalent invariant :

self.rooms->size = self.numberOfRooms

This could be used to debug invariants by proving that the equivalent form is equivalent to the main invariants. This has not been incorporated in any specification language.

Object states on a state diagram must be related to the attributes and association roles on a class diagram. This can be expressed as an invariant in OCL. To distinguish invari- ants on states from invariants on attributes one could intro- duce a keyword state Invariant as follows:

context Class state invariant:

stateInvariant

Where stateInvariant is the predicate relating the a state to the attributes of Class. This may seem redundant because a state can be represented as an attribute on a class diagram, so that the keyword invariant may be sufficient. However, this might

be useful when reading invariants relating state attributes to other attributes.

3.2 Redundant Postconditions

A redundant postcondition can be introduced when specify- ing an operation in terms of a precondition and a postcondi- tion pair. As such a redundant postcondition is stated in the context of an operation specification. It describes properties that should follow from the main part of a specification. In the context of UML/OCL redundant postconditions can be introduced by using redundant postcondition keywords to state operation claims. The following illustrates this in gen- eral:

context Class:: op(p1: T1, ..., pn: Tn) : T

pre : precondition

post : postcondition

redundant post : redundantPost

where precondition is the precondition, postcondition is the postcondition and redundantPost is the redundant postcondi- tion.

In order to make use of redundant postconditions for debug- ging an operation specification, for each such claim, one would try to prove the following:

precondition and postcondition implies redundantPost

As an example consider the following specification of the operation paint on the hotel model:

context Room::paint(newColor: Color)

pre : guests->isEmpty

post : color = newColor and rent = rent@pre+1

The precondition says that a room can only be painted when it is empty, i.e. there are no guests in it. While the postcon- dition says that the room has a new color and that the rent is increased by ten pounds.

The specification of paint with a redundant postcondition could be given as follows:

context Room::paint(newColor: Color)

pre : guests->isEmpty

post : color = newColor and rent = rent@pre+10

redundant post : rent = rent@pre+10

This says that the postcondition should imply that the rent is increased by ten per cent, which is easy to see by the prop- erty of the boolean operator and.

Another useful form of redundancy is to state a postcondi- tion in an equivalent form. This could be achieved by a key- word equivalent post as the following example shows:

context Room::paint(newColor: Color)

pre : guests->isEmpty

post : color = newColor and rent = rent@pre+10

equivalent post : rent = rent@pre+10 and color= newColor

This example is simple but it illustrates the idea behind equivalent postconditions. To debug a specification with equivalent form one has to show the following:

postCondition implies equiPost and

equiPost implies postCondition

Where postCondition is the postcondition and equiPost is the equivalent form of the postcondition.

Again with tool support one would be able to debug an operation specification.

3.3 Examples

Another form of redundancy to specifications is obtained by adding examples which clearly illustrate what is to be done. In OCL, we could use the keyword example to incor- porate examples within specifications. the following exam- ple illustrates this:

context Room::paint(newColor: Color)

pre : guests->isEmpty

post : color = newColor and rent = rent@pre+10

example : newColor = red and guests = Set{} and

color=red and rent@pre = 40 and rent=50

The example shows clearly the relationship between the variables involved in the specification.

The specification language Larch/C++ [15] was the first language to incorporate examples as part of interface speci- fications. Examples can also help in debugging specifica- tions. The specification of the operation describes a relationship between the pre- and post-state. The example describes a pair of states which must be in the relation spec- ified by the operation specification. That is the following must be proved:

example implies (precondition implies postcondition)

Where example is the predicate describing the example, pre- condition is the precondition and postcondition is the postcon- dition. This is equivalent to proving the following:

(example and precondition) implies postcondition

It is more useful to give examples which are consistent with the precondition. Therefore, it might be useful to check that the predicate obtained from the example is consistent with the precondition.

It is also possible to add examples to invariants. This could be achieved as follows:

context Class invariant:

invariant

example : example

Where invariant is the invariant and example is the predicate describing the example. This could help debugging invari- ants by proving the following;

example implies invariant

Adding examples to an invariant could be used to show that the invariant is satisfiable. That is there is at least one object that makes the invariant true.

3.4 Redundant Preconditions

It is also possible to add redundant preconditions to an operation specification. This enables one to state properties that must follow from the precondition, which could be use- ful for exposing to the reader properties that follow from the semantics of the specification language. In OCL redun- dant preconditions could be introduced by introducing a keyword redundant pre as follows:

context Room::paint(newColor: Color)

pre : guests->isEmpty

redundant pre : guests->size = 0

post : color = newColor and rent = rent@pre+1

The redundant precondition states that the number of guests in the room is zero, which is easily derived from the fact that the guest collection is empty. In addition, if the type Color is specified as an enumerated type such as {red, green, blue, yellow}, then a derived precondition is given as follows:

redundant pre : newColor = red or newColor= green or

newColor = blue or newColor= yellow

This unpacks the semantics of enumerated types in OCL.

For debugging specifications with redundant preconditions one is required to prove the following:

precondition implies redundantPre

Where precondition is the precondition and redundantPre is the redundant precondition. It is not clear at this stage whether there is great need for incorporating redundant pre- conditions into OCL.

4 TIME-BASED CONSTRAINTS An invariant on a class or type in OCL must hold for any object of the class in all visible states. A visible state is one that can be observed by clients of that class. Such invariants express common properties that would otherwise be repeated in every operation’s precondition and postcondi- tion. However, invariants are not just mere notational abbreviations, because they apply to all operations, even when new ones are added to a class or type.

Time-based constraints are similar to invariants. However, a time-based constraint on a class or type must hold for any ordered pair of visible states in a computation, where the first state occurs before the second. The property expressed by a time-based constraint must express a reflexive and transitive relation on states in order to make sense. As for invariants, time-based constraints if not expressed sepa- rately, would otherwise have to be repeated in every opera- tion’s postcondition. However, time-based constraints are not just mere notational abbreviations, because they apply to all operations, even when new ones are added to a class or type. The idea of time-based constraints was first intro- duced in [16][17] under the name history constraints. Time- based constraints can be easily incorporated in OCL by introducing a keyword constraint as follows:

context Class constraint :

constraint

where constraint is a boolean expression representing the constraint. This expression relates two states (before state, after state) and will involve @pre.

A simple time-based constraint is that some attributes of an object never changes its value once it is initialized. For example, in the hotel model one constraint is that the floor- Number of a room never changes. In OCL this could be expressed as:

context Room constraint :

floorNumber = floorNumber@pre

This only applies to objects which are not newly created. That is the object must exist in at least two visible states.

Time-based constraints can also be used to express mono- tonic relationships between pre-states and post-states. For example, in the hotel model, a guest age increases with time. This can be expressed as follows:

context Guest constraint:

age >= age@pre

In order to debug a time-based constraint we could incorpo- rate redundant constraints using redundant constraint keywords:

context Class redundant constraint :

redundantConstraint

Where redundantConstraint is the redundant constraint. Debugging time-based constraints would involve proving the following

constraint implies redundantConstraint

Note that constraint could be a conjunction of time-based constraints.

As a simple example, suppose that the number of rooms in a hotel does not change. This can be expressed as a time- based constraint as follows:

context Hotel constraint :

self.numberOfRooms = self.nmberOfRooms@pre

We also have the following invariant:

context Hotel invariant:

self.numberOfRooms = self.rooms->size

A simple example of a redundant time-based constraint is given in the following:

context Hotel redundant constraint :

self.rooms->size = (self.rooms->size)@pre

Which is derived easily from the invariant and the time- based constraint by following simple rules. That is if self.numberOfRooms is constant and self.rooms->size equals to self.numberOfRooms, then it is easy to see that self.rooms->size is also constant. To show this, from the invariant we have:

(self.numberOfRooms = self.rooms->size)@pre =

(self.numberOfRooms = self.rooms->size)

By the properties of the operator @pre we have:

(self.numberOfRooms = self.rooms->size)@pre =

(self.numberOfRooms@pre) = (self.rooms->size)@pre

Here the operator @pre is applied to a boolean expression, with the rule that (b1=b2)@pre is equal to (b1@pre = b2@pre).

From this and the time-based constraint we have:

self.rooms->size = (self.rooms->size)@pre

In general, if an attribute f is related only to an attribute g, and g is a constant attribute, then it follows that f is also constant. Other interesting situations would arise with monotonic constraints and invariants. This example shows the interaction between invariants and time-based con- straints for deriving properties about the model.

Another idea which could be adopted from Larch/C++ is to limit a time-based constraint so that it only applies to some operations rather than all operations [3]. This can be used to group in one place common parts of the postconditions of several operations. This idea was inspired by that advocated by Borgida et al., for dealing with frame axioms [1].

5 CASE ANALYSIS Case analysis is a syntactical mechanism which can be used for decomposing a specification into more manageable parts. This syntactic sugar was first introduced by Wing [27] to split up a specification into several cases. This was also reinvented by Wills [26] and used in the object-ori- ented development method Catalysis [4].

As an example consider the specification of an operation increaseRent which increases the rent of a room depending on season:

context Room::increaseRent(season: {L, H})

pre : (season = L or season = H)

post : season = L implies rent = rent@pre +10

and

season = H implies rent = rent@pre +30

The precondition states that season is either low (L) or high (H). This actually is a derived (redundant) precondition since it is implied by the semantics of enumerated types. However, it is included to illustrate specifications with cases. The postcondition states that if the season is low then the rent is increased by ten units, and if the season is high the rent is increased by 30 units. This actually show a spec- ification with two cases.

Using the case analysis sugar this could be expressed in OCL as follows:

context Room::increaseRent(season: {L, H})

pre : season = L

post : rent = rent@pre +10

also

pre : season = H

post : rent = rent@pre +30

The sugared form of the specification is more readable than the other form because it shows each case clearly.

The case analysis sugaring is more effective when a specifi- cation involves several cases with each case corresponding to a long expression. Another reason is that OCL expres- sions tend to be long because of the use of textual syntax rather than symbolic syntax. Another important reason is that an operation specification may have several specifica- tions which have to be composed. For example, a part of the specification may come from a state diagram, while another part may come from the class diagram. Case analysis would allow a textual representation of the operation specification which mirrors the cases from the state diagram.

6 CONCLUSION This paper has described several enhancements to the Object Constraint Language for expressing various con- straints on UML object-oriented models. These enhance- ments apply generally to the specification technique which is based on preconditions and postconditions, and have already been incorporated within other specification lan- guages such as Larch/C++. These enhancements contribute to the expressiveness of the OCL which could help mod- ellers communicate more effectively with potential clients and implementers.

One of the enhancement which could prove effective in practice is that of case analysis sugar. This helps breaking up a specification into more manageable and easily under- stood parts. However, to be sure of the effectiveness of these enhancements, experimental tests are needed.

Another significant enhancement is that of adding examples to specifications. This can help debug specifications and make specifications clearer.

Future work may involve the incorporation of frame axioms within UML/OCL specifications.

ACKNOWLEDGEMENTS I am grateful to my colleagues at the University of Brighton for useful discussions.

REFERENCES 1. A. Borgida, J. Mylopoulos, and R. Reiter, On the Frame

Problem in Procedure Specifications, IEEE Transac- tions in Software Engineering, 1995; Vol. 21, No. 10.

2. S. Cook, and J. Daniels, Designing Object Systems: Object-Oriented Modelling with Syntropy, Prentice- Hall, Hemel Hempstead, UK, 1994, p. 389.

3. K. Dhara and G. Leavens, Forcing behavioral subtyping through specification inheritance, In Proceedings of the 18th International Conference on Software Engineering, IEEE Computer Society Press, 1996.

4. D. D'Souza, and A. Wills, Objects, Components and Frameworks with UML: The Catalysis Approach, Addi- son-Wesley, UK, 1998, also available at http:// www.trireme.com/catalysis.

5. M. Fowler, and K. Scott, UML Distilled, Addison-Wes- ley, 1997, p. 179.

6. S.J. Garland, J. Guttag, and J.H. Horning, Debugging Larch Shared Language specifications, IEEE Transac- tions on software Engineering, 16(6):1044-1057.

7. J. Guttag, and J. Horning, Larch: Languages and Tools for Formal Specifications, Springer-Verlag, 1993.

8. J. Guttag, J. Horning, S. Garland, K. Jones, A. Modet, and J. Wing, Larch: Languages and Tools for Formal Specifications, Springer-Verlag, New York, N. Y., 1992.

9. C. Jones, Systematic Software Development using VDM (2nd edition), Prentice-Hall, Hemel Hempstead, UK, 1990, p. 333.

10. A. Kleppe, J. Warmer, and S. Cook, “Informal Formal- ity? The Object Constraint Language and its application in the UML metamodel”, Proc. of UML’98 Interna- tional Workshop, P. Muller and J. Bezivin, ed., Mul- house, France, June 3-4, 1998, pp. 127-136.

11. S. Kent, “Constraint Diagrams: Visualising Invariants in Object-Oriented Models”, Proc. of OOPSLA97, ACM Press, 1997.

12. G. Leavens, A. Baker, and C. Ruby, Preliminary Design of JML: A Behavioral Interface Specification Language for Java. Technical Report, TR98-06, Dept. Computer Science, Iowa State University, USA, February 1999.

13. G. Leavens, and A. Baker, Enhancing the Pre- and Post- condition Technique for More Expressive Specifica- tions, Technical Report, TR97-19a, Dept. Computer Science, Iowa State University, USA, September 1997, revised February 1999.

14. G. Leavens, An overview of larch/C++: Behavioral specifications for C++ modules, In Haim Kilov and wil- liam Harvey, editors, Specification of Behavioral Semantics in Object-Oriented Information Modelling, chapter 8, pages 121-142. Kluwer Academic Publishers, Boston, 1996.

15. G. Leavens, Larch/C++ Reference Manual, version 5.25, Available in ftp://ftp.cs.iastate.edu/pub/larchc++/ lcpp.gz or on the World Wide Web at http:// www.cs.iastate.edu/~leavens/larchc++, January 1999.

16. B. Liskov and J. Wing, A behavioral notion of subtyp- ing, ACM Transactions on Programming Languages and Systems, 16(6):1811-1841, 1994.

17. B. Liskov and J. Wing, A, Specifications and their use in defining subtypes, ACM SIGPLAN Notices, 28(10)16-28, 1993, OOPSLA’93 Proceedings.

18. A. Hamie, F. Civello, J. Howse, S. Kent, and R. Mitch- ell, “Reflections on the Object Constraint Language”, Proc. of UML’98 International Workshop, P. Muller and J. Bezivin, ed., Mulhouse, France, June 3-4, 1998, pp. 137-145.

19. S. Stepney, R. Barden, and D. Cooper, editors, Object Orientation in Z, Workshops in Computing, Springer, UK, 1992.

20. M. Spivey, The Z notation (2nd ed.), Prentice Hall, UK, 1992.

21. Rational Software Corporation, Object Constraint Lan- guage Specification, Version 1.1, http://www.ratio- nal.com, 1997.

22. Rational Software Corporation, The Unified Modeling Language, Version 1.1, http://www.rational.com, 1997.

23. J. Rumbaugh, M. Blaha, W. Premerali, F. Eddy, and W. Lorensen, Object-Oriented Modelling and Design, Prentice-Hall, Emglewood Cliffs, New Jersy, 1991, p. 500.

24. Warmer, J., and Kleppe, A., The Object Constraint lan- guage: Precise Modelling with UML. Addison-Wesley, 1999.

25. Warmer, J., and Kleppe, A., OCL : The Constraint Lan- guage of the UML. JOOP, May, 1999.

26. A. Wills, Specification in Fresco, In Stepney et al [19], chapter 11, pages 127-135.

27. J. Wing, A two-tiered approach to specifying programs, Technical Report TR-299, Massachusetts Institute of technology, laboratory for Computer Science, 1983.

OCL Lecture 1_2013.pptx

Formal Methods in Software Engineering

Object Constraint Language (OCL) –Part 1

Sheryl Duggins

Model Driven Architecture (MDA)

MDA is a framework being built under supervision of the OMG

MDA defines how models defined in one language can be transformed into models in other languages.

3 Steps of MDA Process

Build a model with a high level of abstraction which is independent of any implementation technology called a Platform Independent Model (PIM)

Transform the PIM into one or more models tailored to specify your system in terms of the implementation constructs available in one specific implementation technology; called Platform Specific Models (PSMs)

Transform the PSMs to code

Automated Transformations

Key element of MDA is that transformations are executed by tools

Transformation from PIM to PSM is automated

Idea is combination of the Transformation Process Model and the Operational Specification Process Model

MDA Benefits

Portability and platform independence – because the PIM is platform independent and is used to generate several PSMs for different platforms

Productivity – productivity will be achieved by using tools to automate code generation from a PSM, and more when PSM is automatically generated from PIM

Cross-platform interoperability – standards based on multiple implementation technologies

Easier maintenance and documentation – building a PIM takes less effort than writing code

Why Do We Need OCL?

We need precision (formality) to achieve MDA-like modeling

Other formal specification languages are difficult to use; they are based on mathematics and have not been widely adopted.

OCL is one solution (among many), standardized, and integrated to UML

More About OCL?

OCL is a textual language of typed expressions based on mathematical sets and logic

Various other formal languages have also been used in software engineering

Most such languages have proven difficult for the average developer to use

The mathematical symbols are not well known and use obscure fonts

OCL was developed by IBM (1995); (Formally defined 1997.)

It emphasize precision and simplicity. There is no use of special mathematical symbols

What is a Constraint?

A constraint specifies a restriction on one or more values of (part of) an object-oriented model or system

A constraint is a valid OCL expression of type Boolean

Simple constraints on attributes of a class:

Customer

age >= 18 and age < 66

title = if isMale then 'Mr.' else 'Ms.' endif

name.size < 100

OCL: Declarative and Typed

Declarative

States what should be done, not how

Implementation independent

Expressions have no side effects

Evaluation does not change the system state.

Strongly typed

Each OCL expression has a type and evaluates to a value or to an object within the system:

A constraint is a valid OCL expression of type Boolean

Places to use OCL in UML models

Invariants

Constraint on a class or type that must always hold

Also applicable to types and stereotypes

Precondition

Constraint that must hold before the execution of an operation

Postcondition

Constraint that must hold after the execution of an operation

Guard

Constraint on the transition from one state to another

OCL is not limited to class diagrams!

Types in OCL

Predefined types:

Basic types: Integer, Real, String and Boolean

Collection types: Set and Sequence (there are others but they are outside the scope of this course)

User-defined model types:

Enumeration and all classes

Context of an OCL expression

Every OCL expression is bound to a specific context, where self can be used as a reference to this context.

Customer

“A customer must be between 18 and 66 years old”

context Customer

inv: self.age >= 18 and self.age < 66

Standard Operations for Real and Integer types

Standard Operations for the Boolean Type

Standard Operations for the String Type

Collection Types and Navigation in OCL Expressions

If self is class C, with attribute a then

self.a evaluates to the object stored in a.

If C has a 1..* association called R1 to another class D

self.R1 returns a Set whose elements are of type D

if R1 is {ordered} then a Sequence is returned

If D has attribute b then

self.R1.b evaluates to the set (or sequence if {ordered is used}) of all the b’s belonging to D

Navigating Associations

Account

Transaction

0..*

self.R1 returns a set of transactions if we are in the context Account

Book

Member

self.R2 returns a set of members if we are in the context Book

0..*

Navigating to Ordered Collections

The key word {ordered} is a predefined constraint in UML, which means the collection is ordered

self.R1 returns a sequence of accounts in the context Customer

Customer

1..*

Account

{ordered}

OCL Functions on Collection Types

With collection types, an OCL expression

states a fact about all objects in the collection, or

states a fact about the collection itself, e.g. the size of the collection.

Syntax: collection->function

Standard Operations on all Collection Types

Example using size() and notEmpty()

Customer

Account

1..*

Each account can have at most 2 customers

context Account inv: self.R1->size() <= 2

An account must be assigned to at least one customer

context Account inv: self.R1->notEmpty()

1..*

Example Using includes and includesAll

Flight

Person

1..*

pilots

is piloted by

has crew member

1..*

has flight

attendant

1..*

Example Using includes and includesAll (cont.)

A pilot is a member of the crew

All flight attendants are also crew members

Example Using includes and includesAll (cont.)

A pilot is a member of the crew

context Flight inv: self.R2->includes(self.R1)

All flight attendants are also crew members

Example Using includes and includesAll (cont.)

A pilot is a member of the crew

context Flight inv: self.R2->includes(self.R1)

All flight attendants are also crew members context Flight inv: self.R2->includesAll(self.R3)

Select, Reject, Collect, and Sum

collection->select(condition): creates a subcollection that contains objects that satisfy the condition

collection->reject(condition): creates a subcollection that contains objects that do not satisfy the condition

collection->sum(): returns the sum of the elements of the collection; these elements must be numerical

collection->collect(object.attribute): creates a collection of equal size with objects containing the attribute specified

Examples

Assume we are in the context Account, what is returned by each of the following expressions?

self.R1 -> select( value > 500 )

self.R1 -> reject(value > 500)

self.R1.value -> sum()

self.R1 -> sum(self.R1->collect ( value ))

Account

Transaction

value: Integer

1..*

forAll Expression

Evaluating some expression on every element of a collection

Syntax: collection->forAll ( Boolean-expression )

What does this expression mean?

context Account

inv: self.R1->forAll (name = 'Jack' )

Customer

Account

1..*

name

forAll with two variables

Considers each pair in the Cartesian product of employees

context Account

inv: self.R1->forAll( e1, e2 : Customer |

e1 <> e2 implies e1.id <> e2.id)

Customer

Account

1..*

Adding Pre-conditions and Post-conditions to Operations

Pre-conditions:

are predicates associated with a specific operation must be true before the operation is invoked.

Post-conditions:

are predicates associated with a specific operation

must be true after an operation is invoked

Example of Using pre and post Conditions

Customer

name

address

age

setAge(int)

getAge()

Precondition and postcondition:

context Customer::setAge(a: integer)

pre: a > 1

post: age = age@pre + 1

In OCL, we use the @pre suffix to indicate that we are referring to a value at the start of an operation

The return Keyword

The keyword return can be used in a post condition to indicate the return value of an operation:

context Customer::getAge(): integer

post: return = self.age

oclIsTypeOf and oclIsKindOf

oclIsTypeOf(t : OclType) : Boolean

true if the type of self and t are the same. (E.g.)

context Account

inv: self.oclIsTypeOf( Account ) -- is true

inv: self.oclIsTypeOf( Customer) -- is false

oclIsKindOf(t : OclType) : Boolean

true if t is either the direct type or one of the supertypes of an object

Case Study

Write OCL Constraints:

The start date for any mortgage must be before the end date.

A person may have a mortgage on a house only if that house is owned by himself or herself (one cannot get a mortgage on the house of one’s neighbor or friend!)

A person may have a mortgage on a house only if that house is owned by himself or herself (one cannot get a mortgage on the house of one’s neighbor or friend!). Second example, with Person as context.

The social security number of all persons must be unique. Use house as context. You can also use Person but you will need to use self.allInstance() that returns all instances of Person.

A new mortgage will be allowed only when the person’s income is sufficient. (assume that the yearly payment must be less than 30% of the salary)

A new mortgage will be allowed only when the counter value of the house is sufficient

References

“The Object Constraint Language (2nd edition), Getting Your Models Ready for MDA”

by Jos Warmer and Anneke Kleppe,

Addison Wesley, 2003

UML 2.0 OCL : http://www.omg.org/docs/ptc/03-10-14.pdf

OCL Center: http://www.klasse.nl/ocl/index.html

USE Demo:

http://cserg0.site.uottawa.ca/seg/bin/view/CSI5112/UsingUseForOCL

Operation Notation Result type

equals a = b Boolean

not equals a <> b Boolean

less a < b Boolean

more a > b Boolean

less or equal a <= b Boolean

more or equal a >= b Boolean

plus a + b Integer or Real

minus a - b Integer or Real

multiply a * b Integer or Real

divide a / b Real

modulus a.mod(b) Integer

integer division a.div(b) Integer

absolute value a.abs() Integer or Real

maximum a.max(b) Integer or Real

minimum a.min(b) Integer or Real

round a.round() Integer

floor a.floor() Integer

Operation	Notation	Result type
equals	a = b	Boolean
not equals	a <> b	Boolean
less	a < b	Boolean
more	a > b	Boolean
less or equal	a <= b	Boolean
more or equal	a >= b	Boolean
plus	a + b	Integer or Real
minus	a - b	Integer or Real
multiply	a * b	Integer or Real
divide	a / b	Real
modulus	a.mod(b)	Integer
integer division	a.div(b)	Integer
absolute value	a.abs()	Integer or Real
maximum	a.max(b)	Integer or Real
minimum	a.min(b)	Integer or Real
round	a.round()	Integer
floor	a.floor()	Integer

Operation Notation Result type

or a or b Boolean

and a and b Boolean

exclusive or a xor b Boolean

negation not a Boolean

equals a = b Boolean

not equals a <> b Boolean

implication a implies b Boolean

if then else if a then b1 else b2 endif type of b

Operation	Notation	Result type
or	a or b	Boolean
and	a and b	Boolean
exclusive or	a xor b	Boolean
negation	not a	Boolean
equals	a = b	Boolean
not equals	a <> b	Boolean
implication	a implies b	Boolean
if then else	if a then b1 else b2 endif	type of b

Operation Expression Result type

concatenation s.concat(string) String

size s.size() Integer

to lower case s.toLower() String

to upper case s.toUpper() String

substring s.substring(int, int) String

equals s1 = s2 Boolean

not equals s1 <> s2 Boolean

Operation	Expression	Result type
concatenation	s.concat(string)	String
size	s.size()	Integer
to lower case	s.toLower()	String
to upper case	s.toUpper()	String
substring	s.substring(int, int)	String
equals	s1 = s2	Boolean
not equals	s1 <> s2	Boolean

Operation Description

size() The number of elements in the collection

count(object) The number of occurences of object in the collection.

includes(object) True if the object is an element of the collection.

includesAll(collection) True if all elements of the parameter collection are present

in the current collection.

excludes(object)

True if the object is not an element of the collection.

excludesAll(collection)

True if all elements of the parameter collection are not

present in the current collection .

isEmpty() True if the collection contains no elements.

notEmpty() True if the collection contains one or more elements.

Operation	Description
size()	The number of elements in the collection
count(object)	The number of occurences of object in the collection.
includes(object)	True if the object is an element of the collection.
includesAll(collection)	True if all elements of the parameter collection are present in the current collection.
excludes(object)	True if the object is not an element of the collection.
excludesAll(collection)	True if all elements of the parameter collection are not present in the current collection.
isEmpty()	True if the collection contains no elements.
notEmpty()	True if the collection contains one or more elements.

Chapter 2 OCL Examples.pdf

programs

~ a c now : D a b

O..* transactions

Date is a utility class

Figure 2-1 Tlze Royal and Loyal model

I ..* b b

Customer name : String title i String isMale : Boolean

r LoyaltyProgram

- name : String enroll(c : Customer)

Transaction ' points : ~ n i date pate amount: Real program() :

Loyalty Program

getserviceso: Set(Services) programs o..*

Om.* transactions

dateOfBirth Date /age: Integer

age() : lnteger 1 ..*

o..* iparticipants program 1

partners I

Program Partner numberOfCustomers : lnteger name : String

I I

partner

O..* 1 levels

delivered Services

I owner 0

Membership

1 {ordered)

1 1 1 ..* currentlevel

cards

color : Color IprintedName : String

card d F Customercard

valid : Boolean validFrom : Date

Om.1 - LoyaltyAccount - goodThru : Date

ServiceLevel name : String

O..* O..* 1

condition : Boolean pointsEarned : Integer pointsBurned : Integer description : String serviceNr : Integer

level

points - number : Integer earn(i : Integer) burn(i : Integer) isEmpty() : Boolean

Services

Service available

calcPoints() : lnteger

I card

1 account

- transactions O..*

customers to save bonus points. Each individual program partner en and how many bonus points are allotted for a certain purchase.

points can be used to ''buy" specific services'from one of the pro- s. To account for the bonus points that are saved 'by a customer,

ership can be associated with a LoyaltyAccount. transactions on this account are possible. For example, the loyalty pro-

ver and Gold" has four program partners: a supermarket, a line of gas sf a car rental service, and an airline.

0 At the supermarket, the customer can use bonus points to purchase items. The customer earns five bonus points for any regular purchase over the amount of $25. The gas stations offer a discount of 5 percent on every purchase. The car rental service offers 20 bonus points for every $100 spent. Customers can save bonus points for free flights with the airline company. For every flight that is paid for normally, the airline offers one bonus point for each 15 miles of flight.

In this situation, there are two types of transactions. First, there are transactions in which the customer obtains bonus points. In the model (see Figure 2-I), these transactions are represented by a subclass of Transaction called Earning. Second, there are transactions in which the customer spends bonus points. In the model, they are represented by instances of the Burning subclass of Transaction. The gas stations offer simple discounts but do not offer or accept bonus points. Because the turnover generated by the customers needs to be recorded, this is entered as two simultanous transactions on the LoyaltyAccount, one Earning and one Burni~g for the same number of points.

Customers in the Silver and Gold program who make extensive use of the membership are rewarded with a hgher level of service: the gold card. In addi- tion to the regular services, customers who, have a gold card are also offered the following additional services:

Every two months, the supermarket offers an item that is completely free. The average value of the item is $25. The gas stations offer a discount of 10 percent on every purchase. %car rental service offers a larger car for the same price. The airline offers its gold card customers a business class seat for the economy class price.

Customers must meet at least one of the following conditions to get a gold card:

Three sequential years of membership with an average annual turnover of $5,000 One year of membership with a turnover of $15,000, where the turnover is the total turnover with all program partners /-

24 1 Chapter 2 / OCL B Y EXAMPLE

To administer different levels of service, the class SewiceLevel is introduced in the model. A service level is defined by the loyaIty program and used for each mem- bership.

R&L advertises the program and its conditions. It manages all customer data and transactions on the loyalty accounts. For this purpose, the program partners must inform R&L of all transactions on loyalty program membership cards. Each year, R&L sends new membership cards to all customers. When appropriate, R&L upgrades a membership card to a gold card. In this case, R&L sends the customer a new gold card along with information about the additional services offered, and R&L invalidates the old membership card.

The customer can withdraw from the program by sending a withdrawal form to R&L. Any remaining bonus points are canceled and the card is invalidated. R&L can invalidate a membership when the customer has not used the member- ship card for a certain period. For the Silver and Gold program, this period is one year.

We could tell you more about R&L, but the preceding description is sufficient for our purposes. The diagram in Figure 2-1 outlines the system model. Now it's time to add the neccessary details by adding some expressions and stating a num- ber of useful and indispensable constraints.

/ I l

I i I 2 . 2 A D D I N G E X T R A I N F O R M A T I O N , $1 The diagram in Figure 2-1 does not express all relevant information about the

i 1 1 R&L system. The following sections provide examples of additional information that cannot be expressed in the diagram, but should be specified in OCL expres- I' ' sions .

I:,

I/ I ' ,

/,/ , 1 , 2.2.1 Initial Values and Derivation Rules i i JII A very basic addition to the diagram shown in Figure 2-1 is to include rules that 1 1 state initial values for attributes and association ends. Initial value rules can be 1 expressed very simply. First, you indicate the class that holds the attribute or 1 association end. This class is called the context. Then you write the expression that I states your initial value rule. For instance, a loyalty account will always be initial-

I ized with zero points, and a customer card will always be valid at the moment it is issued: c o n t e x t Loyal tyAccount: : p o i nts i n i t : 0

c o n t e x t CustomerCard::valid 1 / i n i t : t r u e

sduggins

Highlight

ADDING EXTRA I N F O R M A T I O N 1 25

Another small but indispensable part of the model is the specification for deter- mining the value bf derived elements. A model may contain derived attributes and derived associations. For both, a so-called derivation rule can be specified. Again, the context of the expression is the class that holds the attribute or associa- tion end: The expression after the context states the derivation rule. For instance, the derived attribute printedName of CustornerCard is determined based on the name and title of the card owner.

c o n t e x t CustomerCard::printedName d e r i v e : owner .ti tle.concat( ' ' ) .concat(owner .name)

In this example, the printedName is the concatenation of the title of the Customer who owns the card, its name, and a space between both strings (e.g., "Mr. Johnson").

2.2.2 Query Operations Query operations are operations that do not change the state of the system; they simply return a value or set of values. The definition of the result of query opera- tions cannot be given in a diagram. In OCL, this can be defined by writing a body expression. The operation name, parameters, and return type (its signature) are given as context. For instance, suppose the class LoyaltyProgram has a query operation get- Services, which returns all services offered by all program partners in this program:

c o n t e x t Loyal typrogram: :getServices( : Set(Ser.vi ce) body: partners.deliveredServices->asset0

this example, the association-end deliveredSentices of ProgramPartner that holds t of Services is used. For all instances of ProgramPartner that are associated with LoyaltyProgram instance of which the operation getservices is called, these sets

and combined into one set. This set is the result of the

body expression, the parameters of the operation may be used. For , 'suppose you need a more refined version of the getservices operation.

operation takes as a parameter a program partner object and returns the ser- delivered by the parameter object, if it is a partner in this program. In this the refined operation can be specified as follows:

n t e x t LoyaltyProgram::getServices(pp: ProgramPartner) : Set(Service)

Y : if partners->incl udes.(pp) then pp.deliveredServices

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

26 1 Chapter 2 I O C L BY EXAMPLE

The result of this query operation is the set of Services held by the parameter pp, or an empty set if the parameter instance of ProgramPartner is not a partner of the LoyaltyProgram for which the query operation is called.

Note that there is no difference between a derived attribute and a query opera- tion that has no parameters, other than the notation. The query operation needs to be, written using parentheses.

2.2.3 Defining N e w Attributes and Operations Although most elements in the model are introduced in the UML diagrams, attributes and operations can be added to the model using an OCL expression. The context is the class to which the attribute or operation is added.

An attribute that has been defined in this manner is always a derived attribute. The expression that defines the attribute includes the name and type of the attribute, and the derivation rule. For instance, we might want to introduce an attribute called turnover in class LoyaltyAccount, which would sum the amount attributes of the transactions on the account. This attribute can be defined by the following expression. The part after the equal sign states the derivation rule for the new attribute:

c o n t e x t Loyal tyAccount d e f : turnover : Real = transactions.amount->sum0

The derivation rule results in a single real number that is calculated by summing the value of the amount attribute in all transactions associated with the LoyaltyAc- count instance that holds the newly defined attribute.

An operation that has been defined in an OCL expression is always a query operation. The expression after the equal sign states the body expression. For example, we might want to introduce the operation getServicesByLeve1 in the class LoyaltyProgram..This query operation returns the set of all delivered services for a certain level in a loyalty program:

c o n t e x t Loyal tyProgram d e f : getServicesByLeve1 (1evelName: String): Set(Service1

= levels->sel ect( name = l eve1 Name ) .avai 1 ableservi ces->asset()

The result of the body expression is calculated from a selection of the levels asso- ciated with the instance of LoyaltyProgram for which the operation getServicesBy- Level is called. It returns only the services available from the ServiceLeveI whose name is equal to the parameter 1eveliVame. The reason for using the asset operation is given in Section 2.4.2.

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

A D D I N G I N V A R I A N T S 1 27

2 . 3 A D D I N G I N V A R I A N T S More information can be added to the model in the form of invariants. An invari- ant is 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.

2.3.1 lnvariants on Attributes A reasonable rule for every loyalty program of R&L would be to require that every customer who enters a loyalty program be of legal age. In the model, this means that the attribute age of every customer object must be equal to or greater than 18. This can be written as an invariant:

context C u s t o m e r i n v o f A g e : a g e >= 18

Invariants on one or more attributes of a class can be expressed in a very simple manner. The class to which the invariant refers is the context of the invariant. It is followed by a boolean expression that states your invariant. All attributes of the context class may be used in this invariant.

2.3.2 The Type of the Attribute Is a Class When the attribute is not of a standard type, such as Boolean or integer, but its type is a class itself, you can use the attributes or query operations defined on that class to write the invariant, using a dot notation. For example, the class CustomerCavd contains two attributes validFrom and goodThru of type Date. A simple but useful invariant on these two date attributes states that validFrom should be earlier than goodThru:

context C u s t o m e r c a r d i n v c h e c k D a t e s : validFrom.isBefore(goodThru)

is invariant uses the operation isBefore in the Date class that checks whether the e in the parameter is later than the date object on which the operation is called.

results in a boolean value. Note that you may use only operations that do not e the value of any attributes; only the so-called query operations are

Invariants on Associated Objects y also state rules for associated objects. The rule that every card- be of age could also be stated as follows:

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

----

28 1 Chapter 2 / OCL B Y EXAMPLE

c o n t e x t Customercard inv ofAge: owner.age >= 18

Stating an invariant on associated objects is done by using the rolename on the association to refer to the object on the other end. If the rolename is not present, you should use the name of the class. Note that the previous version of OCL required-that the class name be written starting with a lowercase letter. In version 2, the name used should be identical to the name of the association class. Giving rolenames to each association end is preferred. Using rolenames to traverse an association to get to the corresponding instances is called navigation.

Finding the right context for an invariant can sometimes be challenging. Usu- ally, the right context is the context for which the invariant can be expressed in the simplest way and/or for which the invariant is simplest to check.

2.3.4 Using Association Classes Association classes may also be used in OCL expressions, but some special rules apply. Association classes may not have a rolename; therefore, the name of the association class is used to refer to an instance of that class. The previous version of OCL also required that the class name be written starting with a lowercase let- ter. In version 2, the name used should be identical to the name of the association class. For instance, the following invariant uses the association class Membership to state that the service level of each membership must be a service level known to the loyalty program for which the invariant holds:

c o n t e x t LoyaltyProgram i n v knownServi c e l e v e l : 1 eve1 s - >

i ncl udesA11 (Membership . c u r r e n t L e v e l ) I

Using the association class as context, you may navigate to the instances of both I classes at the end of the association to which the association class belongs, using their rolenames:

I 1

c o n t e x t Membershi p inv c o r r e c t c a r d : p a r t i c i p a n t s . c a r d ' s - > i n c l u d e s b e l f . c a r d )

Because an association class is in fact a class itself, it can have ordinary associa- tions with other classes. These may be referenced in the manner explained in Sec- ,

tion 2.3.3. For example, the following defines a query operation to the association class Membership using the ordinary association between Membership and Service- Level: ,I

$7 c o n t e x t Membershi p

- - c r , , m - n n + l n j ~ n l k l a r n ~ f \ : S t r i n q = c u r r e n t l e v e l .name i/ j3

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

WORKING W l T H COLLECTIONS OF OBJECTS 1 29

2.3.5 Using Enumerations In a UML model, enumeration types may be defined. An enumeration type may 'be used, for instance, as the type of an attribute of a class in a UML class model. The values of an enumeration type are indicated in an OCL expression by the name of the enumeration type, followed by two colons, followed by the value- name. An example can be found in the CustomerCard class, where the attribute color can have two values, either silver or gold. The following invariant states that the color of this card must match the service level of the membership:

c o n t e x t Membership i n v 1 eve1 AndCol o r :

c u r r e n t i e v e l .name = ' ~ i l v e r ' imp1 i e s c a r d . c o 1 o r = C o l o r : : s i l v e r a n d c u r r e n t l e v e l .name = 'Go1 d ' i mpl i e s c a r d . col o r = Col o r : : go1 d

2 . 4 W O R K I N G W I T H C O L L E C T l O N S O F O B J E C T S Often, the multiplicity of an association is greater than 1, thereby linking one object to a collection of objects of the associated class. To deal with such a collec- tion, OCL provides a wide range of collection operations, and distinguishes between different types of collections.

2.4.1 Using Collections Operations Whenever navigation results in a collection of objects, you can use one of the col- lection operations to manipulate this collection. To indicate the use of one of the predefined collection operations, you place an arrow between the rolename and the operation. When you use an operation defined in the UML model, you use a dot.

The size Operation R&L,it would be reasonable to require that a loyalty program offers at least service to its customers. Using the dot notation, you can navigate from the

text of a loyalty program through its program partners to the services they er. This results in a collection of Service instances. With the arrow notation, can apply the predefined operation size. The rule would be stated as follows:

c o n t e x t Loyal tyProgram i n v m i n s e r v i c e s : p a r t n e r s . d e l i v e r e d s e r v i c e s - > s i z e ( >= 1

er invariant on the R&L model requires that the number of valid cards for C l ] s t n r n n ~ - - - - L 1- - 7 * . I

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

j I

30 . 1 Chapter 2 / O C L B Y E X A M P L E

participates. This constraint can be stated using the select operation on sets. The select operation takes an OCL expression as parameter. The result of select is a sub- set of the set on which it is applied, where the parameter expression is true for all elements of the resulting subset. In the following example, the result of select is a subset of cards, where the attribute valid is true:

c o n t e x t Customer i n v sizes~gree:.

programs->size() = cards->select( valid = true 1->s.ize(

The forAII and isEmpfy Operations Also relevant to the R&L model is a requirement that if none of the services offered in a LoyaltyProgram credits or debits the LoyaltyAccount instances, then

I these instances are useless and should not be present. We use the forAll operation , I on the collection of all services to state that all services comply with this condi- I

: 1 tion. The forAll operation, like select, takes an expression as parameter. Its outcome is a boolean: true if the expression evaluates to true for all elements in the collec- //

tion, and otherwise false. The following invariant states that when the LoyaltyPro- gram does not offer the possibility to earn or burn points, the members of the Loyal tyProgram do not have Loyal t y A c c o u n ts; that is, the collection of Loyal t y A c - counts associated with the Memberships must be empty:

c o n t e x t Loyal tyProgram i n v noAccounts: forAll( partners . . . 1

c o n t e x t Loyal ty Program

In fact, this is an incorrect expression. The jorAll operation is used when we already have a subset of all instances of a class, and we want to check onuthe ele- ments of that subset. In the preceding example, all services delivered by the part- ners of a certain LoyaltyProgram are a subset of all instances of class Service. This subset is checked to include only those services for which pointsEamed and points- Burned are equal to zero. (See Section 3.10.3 for more information on this topic.)

The preceding example also introduces two logical operations: and and implies. The and operation is the normal logical and operation on boolean values. The implies operation states that if the first part is true, then the second part must also be true; however, if the first part is not true, it does not matter whether the second

1 1 ; I / / ! Y

1 1 i n v noAccounts: partners.de1iveredServices->forAll( i 1 1 pointsEarned = 0 and pointsBurned = 0 )

1 implies Membership.account->isEmptyO , / i / 1 Note that defining a constraint for a class already implies that the condition holds

1 I 1 1 for all instances of that class. There is no need to write the following:

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

WORKING WITH COLLECTIONS O F OBJECTS / 31

The collect Operation A collection operation that is used very often is the collect operation. For instance, it is used when you want to get the set of all values for a certain attribute of all objects in a collection. In fact, many of the examples in this chapter use this opera- tion, because the dot notation is an abbreviation for applying the collect operation. Take, for instance, the following expression in the context of LoyaltyProguam:

Another way to write it is

It means that for each element in the collection of partners of a loyalty program, the value of the attribute nz~mberOfCustomers is added to a new collection, in this case, containing integer values.

The resulting collection is not a subset of the original collection. In fact, in most cases, the type of the elements in the resulting collection is different from the type of the elements in the manipulated collection. In this case, the collection partners contains elements of type ProgramPartner, whereas the collection resulting from applying the collect operation contains elements of type integer.

The collect operation may be used not only to collect attribute values, but also to build a new collection from the objects held by association ends. The next expression, already used in this section, is an example of an implicit use of the col- lect operation on association ends:

p a r t n e r s . d e l i v e r e d s e r v i c e s

Another way to write this expression is

p a r t n e r s - > c o . l 1 e c t ( del i v e r e d s e r v i c e s 1

For each element in the collection of partners of a loyalty program, the value of the association end deliveredservices is added to a new collection, in this case, con-

taining references to instances of the class Service.

re Collection Operations section contains more collection operations (the complete list can be found in

which is true when the collection has at least one element bject ), which is true when object is an element of the collection

lection of objects ), which results in a collection of objects that holds the

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

32 1 C k a p f e r 2 / OCL B Y EXAMPLE

Q intersection( collection of objects ), which results in a collection of objects that holds all elements that are in both collections

2.4.2 Sets, Bags, OrderedSets, a n d Sequences When working with collections of objects, you should be aware of the difference between a Set, a Bag, an OrderedSet, and a Sequence. In a Set, each element may occur only once. In a Bag, elements may be present more than once. A Sequence is a bag in which the elements are ordered. An OrderedSet is a set in which the ele- ments are ordered.

Navigations Resulting in Sets and Bags To understand why these differences are important, take a look at the attribute numberOfCustomers of class ProgramPartner. We want to state that this attribute holds the number of customers who participate in one or more loyalty programs offered by this program partner. In OCL, this would be expressed as follows:

c o n t e x t ProgramPartner inv nr0fParticipants:

numberOfCustomers = programs.participants->size0

However, there is a problem with this expression. A customer can participate in more than one loyalty program. In other words, a reference to the same object of class Customer could be repeated in the collection program.participants. Therefore, this collection is a bag and not a set. In the preceding expression, these customers are counted twice, which is not what we intended.

In OCL, the rule is that when you navigate through more than one association with multiplicity greater than 1, you end up with a bag. That is, when you go from A to more than one B to more than one C, the result is a bag of Cs. When you navigate just one such association you get a set. There are standard operations that transform one of the types into any of the other types. Using one of these operations you can correct the previous invariant as follows:

context ProgramPartner 4 $

i n v nr0fParti c i pants: numberOfCustomers = programs .parti cipants->asset() ->si z e ( ) w j 4

4 When you navigate an association with multiplicity greater than 1 on the target $ end, and from there navigate an association with multiplicity greater than 1 on 4 the target end, you also end up with a bag. The expression transactions.generatedBy 1 from the context of CustomerCard denotes a bag of instances of Service. Every serv- 4 ice may be associated with more than one transaction, so when you take the serv-

- --& c - - c ~ p + i n n ~ some services might be present more than once.

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

sduggins

Highlight

ADDING PRECONDITIONS AND POSTCONDITIONS 1 33

Navigations Resulting in OrderedSets and Sequences When you navigate an association marked [ordered), the resulting collection is of type OrderedSet; and following the rules explained above, when you navigate more than one association and one of them is marked {ordered], you end up with a sequence. Several standard operations deal with the order of an ordered set or sequence: first, last, and at(index). The only ordered association in the R&L model lies between LoyaltyProgram and ServiceLevel. In the context of LoyaltyProg~am, the expression serviceLevel results in an ordered set. We can state that the first element of this ordered set must be named Silver as follows:

c o n t e x t Loyal tyProgram i n v f i r s t l e v e l : l e v e l s - > f i r s t O . n a m e = ' S i l v e r '

2 . 5 A D D I N G P R E C O N D I T I O N S A N D P O S T C O N D I T I O N S Preconditions and postconditions are constraints that specify the applicability and effect of an operation without stating an algorithm or implementation. Add- ing them to the model results in a more complete specification of the system.

2.5.1 Simple Preconditions and Postconditions The context of preconditions and postconditions is specified by the name of the class that holds the operation and the operation signature (its name, parmeters, and return type). In the R&L example, the class LoyaltyAccount has an operation isEmpty.' When the number of points on the account is zero, the operation returns the value true. The postcondition states this more precisely; it tells us that the operation returns the outcome of the boolean expression points = 0. The return value of the operation is indicated by the keyword result:

c o n t e x t Loyal tyAccount: : i s E m p t y ( : Boo1 ean p r e . - - none p o s t : r e s u l t = ( p o i n t s = 0)

ere is no precondition for this operation, so we include a comment, none, precondition should be placed, indicated by the double dash. Including ition, even if it is an empty one, is optional. Rather, it is a matter of style.

refer to state even empty preconditions, because we think this is clearer. If, tance, this example were part of a list of operations with their pre- and post- ions and the precondition for the isEmpty operation was the only one miss-

might misinterpret its meaning and think that the. precondition

sduggins

Highlight

34 I Chapter 2 I O C L B Y EXAMPLE

2.5.2 Previous Values in Postconditions In a postcondition, the expression can refer to values at two moments in time:

The value at the start of the operation Q The value upon completion of the operation

The normal.value of an attribute, association end, or query operation in a post- condition is the value upon completion of the operation. To refer to the value of a property at the start of the operation, postfix the property name with the keyword @pre, as shown in the following example:

context Customer::birthdayHappensO post: age = age@pre + 1

The term age refers to the value of the attribute after the execution of the opera- tion. The term age@pre refers to the value of the attribute age before the execution of the operation.

When you need the pre-value of a query operation, the @pre is postfixed to the operation name, before the parameters, as shown in the next example:

context Service::upgradePointsEarned(amount: Integer) post: calcPoints() = calcPoints@pre() + amount

The @pve postfix is allowed only in OCL expressions that are part of a postcondi- tion.

2.5.3 Messaging i n Postconditions Another thing allowed only in postconditions is specifying that communication has taken place. This can be done using the hassent (IA') operator. For example, you can specify the standard observer pattern:

context Subject::hasChangedO post: observerAupdate(12, 14)

The obseruerAupdate(12, 14) results in hue if an update message with arguments 1 2 and 14 was sent to the observer object during the execution of the operation haschangedo. update^ is either an operation defined in the class of observev, or a signal specified elsewhere in the UML model. The argument(s) of the message expression (12 and 14 in this example) must conform to the parameters of the ope- ration/signal definition.

TAKING INHERITANCE INTO ACCOUNT / 35

2 . 6 TAKING I N H E R l T A N C E I N T O ACCOUNT The advantage of using inheritance is that an object using the superclass interface need not know about the subclasses. However, sometimes you explicitly want to mention the subclasses. In the R&L example, the program partners want to limit the number of bonus points they give away; they have set a maximum of 10,000 points to be earned using services of one partner. The following invariant sums all the points of all transactions for a partner. It does not specify our intent, however, because it does not differentiate between burning and earning transactions:

context P r o g r a m P a r t n e r inv t o t a l P o i n t s :

deliveredServices.transactions.points->sum0 < 10,000

To determine the subclass to which an element of this collection of transactions belongs, we use the standard operation oclIsTypeOf, which takes a class, datatype, component, or interface name as parameter. To retrieve from the collection all instances of this subclass, we use the select operation. We use the collect operation to retrieve from the collection of earning transactions a collection of points. These are the points that are summed by the operation s u m and compared with the given maximum. Therefore, the correct invariant would be as follows:

context P r o g r a m P a r t n e r inv t o t a l P o i n t s E a r n i n g :

deliveredServices.transactions - > s e l e c t ( o c l I s T y p e O f ( E a r n i n g ) ) . p o i n t s - > s u m ( ) < 1 0 , 0 0 0

C O M M E N T S In any model, comments are necessary to facilitate human understanding. This holds for a UML/OCL model too. It is good practice to accompany every OCL expression with a comment. A line comment is indicated by two minus signs: --. After this marker, everything on the same line is considered to be comment. Com- ments that span more than one line can be enclosed between / * and */.

For example, the previous invariant could have been accompanied by the fol- , lowing comments:

/* t h e f o l l o w i n g i n v a r i a n t s t a t e s t h a t t h e maximum number o f p o i n t s t h a t may b e e a r n e d b y a l l s e r v i c e s o f a p r o g r a m p a r t n e r i s e q u a l t o 1 0 , 0 0 0

* / context P r o g r a m P a r t n e r inv t o t a l P o i n t s E a r n i n g :

d e l i v e r p d S ~ r v i r ~ s + r a n c a r t i n n c - - - 1 1 + m - * - - - . L 2 - . - -

36 1 C h a p t e r 2 I O C L B Y E X A M P L E

->select( ocl IsTypeOf( Earning ) ) - - select earning ones .points->sum() - - sum a1 1 points

< 10,000 - - sum smaller than 10,000

2 . 8 L E T E X P R E S S I O N S Some times than once. instead of

one writes large expressions in which a sub-expression is used more The let expression enables you to define a variable that can be used the sub-expression. The following example states that either the

validFrom or the goodThru date of a customer card needs to be adjusted when the card is invalidated. An extra variable named cowect~ateis defined to indicate whether or not the current date is between the validFrom and goodThru dates:.

context Customercard inv: let correctDate : Boolean =

self .val idFrom.isBefore(Date: :now) and self.goodThru.isAfter(Date::now)

i n if valid then

correctDate = false el se

correctDate = true endi f

A let expression may be included in any kind of OCL expression. The newly defined variable is known only within this specific expression.

2 . 9 S U M M A R Y In this chapter, you have learned how to write OCL expressions by example. Of course, the description of OCL in this chapter is not complete, detailed, or precise. Part 2 of this book provides the complete specification of the OCL language. The following chapters in this part discuss how you can use OCL expressions for modeling.

Chapter 3

This chapter shows how a UML model can be augmented by OCL expressions, resulting in a model that is rich enough to give to automated tools as input. All examples in this and the following chapters refer to the R&L system as depicted in Figure 2-1, unless stated otherwise.

3 . 1 W H A T IS A M O D E L ? Before we discuss how to build a model, we need to understand what is meant by the word model. This term is used in many contexts and often has a different meaning. For instance, the R&L system depicted in the previous chapter is often called a class model. A statechart is sometimes called a state model. Are these mod- els two separate, unrelated items, or should we consider them to be part of the same thing?

3.1 .I Definitions In this book a model describes a system using a well-defined language. Therefore, the answer to the question above should be that both are views of the same

el. Both class diagrams and the statecharts show items that describe the same em using the same language-namely, UML.

use the word model to refer to a consistent, coherent set of model elements ave features and restrictions, where model elements are the compositional

ments that may be used in artifacts written in UML and/or OCL. For example, s are model elements, and so are states. Attributes and operations are fea- of classes, and derivation rules and invariants are restrictions on attributes asses, respectively. Because most models are built using tools, we refer to

orage of all model elements as the model repository. indicate a certain view on the repository of model elements we use the word

Using these definitions, the picture shown in Figure 2-1 is a diagram g part of the R&L modP[ M n d ~ l P I P ~ P ~ ~ C ran hn c h n ~ ~ n - :- --- :- ----- -

OCL Slides Lecture 2_2013.ppt

The Object Constraint Language (OCL) Part 2

Topics

Why constraints?
Different kinds of constraints
Advanced OCL concepts
Modeling with constraints
Application to components

Why Use OCL

Many facts about a software system that a modeler would like to express, can not be expressed, or can not easily be expressed in a visual model.

Example

Class Diagram

Example

Class Diagram with invariants may simplify

The Scope of OCL

Software developers working with object-oriented methods needed constraints. Many developers made their own pseudo language. OCL is the UML standard.

Writing or (generating) constraints may result in a more secure product

Definition of Constraint

A constraint is a restriction on one or more values of (part of) an object-oriented model of system.

“Restriction” implies security aspects can be specified.

Kinds of Constraints (1)

Class Invariant
A constraint that must always be met by all instances of a class
Precondition of an operation
A constraint that must always be true BEFORE the execution of the operation

Kinds of Constraints (2)

Post-condition of an operation
A constraint that must always be true AFTER the execution of the operation
Guard condition
A constraint that must always be true before a transition in a Statechart/State Diagram, Sequence Diagram, and other behavioral diagrams in the UML

Format

context - a keyword, think of it as the current directory from which relative path names are derived
<identifier> is a class or operation name
<constraintType> is inv, pre, or post
<Boolean expression> is usually an equation

context <identifier> <constraintType>:

UML Stereotypes

A stereotype is, in effect, a new class of modeling element that is introduced at modeling time. It represents a subclass of an existing modeling element with the same form (attributes and relationships) but with a different intent. Generally a stereotype represents a usage distinction.
Example: <<Interface>>

Constraint Stereotypes

UML Defines three standard stereotypes for constraints
Invariant
context Class inv:
Precondition
context Class::operation(…):returntype pre:
Postcondition
context Class::operation (…)returntype post:

Formal but easy

OCL is designed to be a formal language
Precise
Unambiguous
No Side Effects
Strong Type Checking

OCL and the UML

OCL expressions are always bound to a UML Model
OCL expressions always put constraints on the elements of a UML model. This model describes which classes may be used and which attributes, operations, and associations are available for objects from these classes.

Example Model

How can constraints be used?

Constraint context and self

Every OCL expression is bound to a specific context.
The context may be denoted within the expression using the keyword self.

Notation

Constraints may be denoted within the UML model of in a separate document (context clear in both cases)

Example: use of Self

The expression:
The expression:
Context Flight inv: self.duration < 4
Is identical to
Context Flight inv: duration < 4
is Identical to

Elements of an OCL Expression

The following elements may be used:
Basic types: String, Boolean, Integer, Real
Classifiers from the UML Model and their features
Attributes and Classes
Query operations, and class query operations
(Note: operations that result in changing the system may not be used)
Enumeration types from the UML Model
Associations

Built in Primitives:

Keywords

Example: Basic Types

Context Airline inv: name.toLower = ‘klm’
Context Passenger inv:
Age >= ((9.6-3.5)*3.1).floor implies mature = true
Types and operations used in programming languages are acceptable

Example Query Operations

duration = arrival time – depart time

Example: Enumeration

Enumeration uses datatype followed by :: and the values
Context Passenger inv:
Self.age> 75 implies
Self.needsAssistance = Assistance::wheelchair

Associations and Navigation

Every association is a navigation path
The context of the expression is the starting point
Role names are used to identify the navigated associations

Example: Navigations

Remember Flight is a navigation
Context Flight
Inv: origin <> destination
Inv: origin.name = ‘Amersterdam’
Context Flight
Inv: airline.name = ‘KLM’

Association Classes

Uses association end descriptors

OCL Collections

Often associations are one-to-many or many-to-many. This means that in an OCL expression you are putting constraints on a collection of objects. Thus, OCL expressions either states a fact about all object in the collection or states facts about the collection itself e.g. the size of the collection.

Three Subtypes of Collections

Set:

a set is a collection in which every element can be present only once.

Bag:

a bag is a collection in which an element can be present more than one time.

Sequence:

a sequence is an ordered bag.

Collection Operations

There are several predefined operations on the collections types.
Syntax: collectionoperation
e.g. isEmpty, size, includes, union, etc.
An arrow, instead of a dot, before the operation indicates use of one of these collection operations. The reason is, of course, to avoid name clashes with operations defined in the model.

The Collect Operation

Syntax
collection->collect(elem : T | expr)
collection->collect(elem | expr)
collection->collect(expr)

The collect operation is one of the operations on collections that are used most often. It iterates over the collection, computes a value for each element, and gathers the evaluated values into a new collection. Its syntax has three variants.
Whenever it is clear what the type of the elements in the collection is ‘: T’ may be omitted.
The second variant is used when ‘elem’ has to be referred to explicitly in the expression,
in other cases ‘elem |’may be omitted.

The Collect Operation

Shorthand:

collection.expr

Because the collect is used so may times, a shorthand notation was introduced. This can be used when the expression ‘’expr” is a single attribute, operations or association.

Example: collect operation

Example:

context Airport inv:

self.arrivingFlightscollect(airLine)notEmpty

context Airport inv:

self.arrivingFlights.airLine->notEmpty

The first invariant gathers all Flight objects in the association with rolename ‘arrivingFlights’. It then collects all Airlines from these flights. Then it states that this collection may not be empty (every airport must have one or more airlines with flights arriving)

Example: Collection Operation

When invariant evaluated for airport1:

The Select and Reject Operations

Syntax:

collection->select(elem : T | expr)
collection->select(elem | expr)
collection->select(expression)
select: subset of all elements for which expression is true
reject: subset of all elements for which expression is false

Select and Reject Operations

The select and reject operations also result in a new collection, but the elements in this new collection always have the same type as the elements in the original collection.
The select and reject operations have the same syntactical variants as the collect operation. The shorthand notation can not be used, because it can not be distinguished from the collect operation.

Two Identical Invariants

context Airport
inv: self.departingFlights->select(duration<4)->notEmpty
inv: self.departingFlights->reject(duration>=4)->notEmpty

Identical Invariants Continued

A new collection is created

The forAll operation

Syntax:
collection->forAll(elem : T | expr)
collection->forAll(elem | expr)
collection->forAll(expression)
result is true if expression is true for all elements of the collection

Example: forAll Operation

context Airport inv:
self.departingFlightsforAll(departTime.hour >= 0)
This invariant states that on every airport all (departing) flights must depart before midnight.

The Exists Operation

Syntax:
collection->exists(elem : T | expr)
collection->exists(elem | expr)
collection->exists(expression)
result is true if there is at least one element in the collection for which the expression is true

Example: exists operation

context Airport inv:

self.departingFlightsexists(departTime.hour < 6)

The isUnique Operation

Syntax:
collection->isUnique(elem : T | expr)
collection->isUnique(elem | expr)
collection->isUnique(expression)
result is true if the expression evaluates to a different value for each element in the collection
e.g. context Airport inv:

self.departingFlights->isUnique(departTime)

Other Collection Operations

isEmpty: true if collection has no elements
notEmpty: true if collection has at least one element
size: number of elements in collection
count(elem): number of occurrences of elem in collection

More Collection Operations

includes(elem): true if elem is in collection
excludes(elem): true if elem is not in collection
includesAll(coll): true if all elements of coll are in collection

More Collection Operations

union(collection): collection containing all elements from both original collections
intersection(collection): collection containing the elements that are in both original collections
sum: the sum of all elements in the collection

More Collection Operations

asSet: Set containing all elements from the original collection
asBag: Bag containing all elements from the original collection
asSequence: Sequence containing all elements from the original collection
The different kinds of collections can be changed into other kinds. Making a set from a bag is a very common use.

Example

context Airline

inv: self.flights->size >= 100

inv: self.flights->forAll(

passengers->count(self.CEO) = 1 implies maxNrPassengers = 20 )

The first invariant states that every airline must have at least 100 flights.
The second invariant states that if on any flight of an airline the CEO is one of the passengers then the maximum number of passengers is 20.

Type Conformance Rules

Collection (type1) conforms to

Collection (type2) if type1 conforms to type2.

Set(type) does not conform to Bag(type), Sequence(type)

Type Conformance Example

Set(PassengerFlight) conforms to Set(Flight)
Bag(PassengerFlight) does not conform to Set(Flight)
Set(PassengerFlight) does not conform to Set(CargoFlight)

Instance Versus Collection

An instance can always be treated as a collection
A collection with one element can be used as an instance
Use of either the arrow (->) or the dot (.) distinguishes between these uses

Instance Versus Collections

To make writing and reading OCL simple, an instance can be treated as a set. Otherwise we would need to create a set from an instance explicitly.
Vice versa, a set with one element can be treated as an instance. Otherwise, the element needs to be taken from the set explicitly.
The arrow syntax denotes the use as a set, the dot syntax denotes the use as an instance.

No Nested Collections

OCL does not deal with collections of collections (of collections of …)
Complicates language
Can use nested forAlls in most cases

Advanced OCL

Pre- and Post-Conditions
State machines
Local variables
The iterate operation
Inheritance

Pre/Post Conditions

Constraints that specify the effect of an operation without stating an algorithm or implementation.

Design by Contract

Pre- and post-conditions of an operation specify a contract of the operation
All pre- and post-conditions of all operations of a class describe the class’ contract

OCL Pre/Post Conditions

Contextual object is the instance which performs the operation
context Airline::operation (params): resultType
pre: -- constraint must be met before op
post: -- constraint must be met after op

Special Syntax

“@pre” refers to value of property before execution
keyword “result” refers to return value

@pre in post condition

context Passenger::book(f : Flight)

pre: f.maxNrPassengers > f.passengerssize

post: f.passengers = f.passengers@pre->

including(self)

The precondition states that there may not be more passengers than the maximum number of passengers.
The postcondition states that after execution of this operation, the list of passengers must contain not only the passenger that where in there before but also the passenger which is the conceptual object.

Result in Postconditions

Example pre and postcondition

context Airline::servedAirports() : Set(Airport)
pre: -- none
post: result = flights.destination->asSet

Messaging in Post conditions

hasSent (‘^’) operator specifies that communication has taken place
Context Subject::hasChanged()

Post: observer^update(12,14)

Update message was sent to the observer during the execution of hasChanged()

Update is a operation defined in observer.

New Options in Post Conditions (OCL 2.0)

isSent
isSignalSent
isOperationCall
hasReturned
result

Guard Conditions

Act as preconditions

Statecharts: referring to states

The operation oclInState returns true if the object is in the specified state.
object.oclInState( statename )

Let for Local Variables

The Let construct defines variables
local to one constraint:
Let var : Type = <expression1> in <expression2>

Example Local Variable

context Airline inv:

let ps : Set(Passenger) = flights.passengers->asSet in ps->select(needsAssistence)->size / ps->size <= 0.1

Iterate

The iterate operation for collections is the most generic and complex building block.

collection->iterate(elem : Type; result : Type = <value> | <expression-with-elem-and-result>)
elem = iterator variable
result = accumulator (gets an initial values)
For each successive element the expression-with-elem-and-result is calculated using the previous value of the result variable

Example

context Airline inv:

flights->select(maxNrPassengers > 150)->notEmpty

Is identical to:

context Airline inv:

flights->iterate(f : Flight; answer : Set(Flight) = Set{ } | if f.maxNrPassengers > 150 then

answer->including(f) else answer endif )->notEmpty

Iterate Example

Set{1,2,3}iterate(i: Integer, sum: Integer = 0 | sum +1)

Inheritance of Constraints

Guiding principle Liskovs Substitution

Principle (LSP):

“Whenever an instance of a class is expected, one can always substitute an instance of any of its subclasses.”

Inheritance of Constraints

Inheritance of constraints, invariants as well as pre- and postconditions, is a difficult subject.To determine the meaning of inheritance of constraints within OCL we use Liskovs Substitution Principle as guideline.

Inheritance of Invariants

Consequences of LSP for invariants:
An invariant is always inherited by each subclass.
Subclasses may strengthen the invariant (specialization).

Inheritence of pre/postconidions

Consequences of LSP for

Pre-conditions and post-conditions:

A pre-condition may be weakened
A post-condition may be strengthened

Properties in Postconditions

The default rule is that attributes that are not mentioned in a postcondition are not changed by the operation.

Modeling with the OCL

OCL can be used help with various modeling problems.

Cycles in Class Diagrams

Cycles may have hidden/implicit constraints

Cycles in Models

Invariant:
context Airline inv:
airplanes->includesAll(flights.airplanes)
Or:
context Flight inv:
airplane.owner = airline
One implicit constraint in the previous example diagram might be that all flights of an airline must be done using its own airplanes.
This constraint may also be expressed using Flight as context.

Cycles in Class Diagrams

Without the previous invariants, the following might be true:
context Flight inv:
airplane.owner <> airline
Not stating these implicit constraints may lead to misunderstanding of the diagram and, eventually, to an erroneous implementation.

Constraining Patterns

May need to add constraint to reuse design.

Restrictions of Pattern Instances

Current models allow any combo of components

Restrictions of Patterns

Combinations of composites and leaves:

context Bicycle

inv: parts->select( oclIsKindOf(Frame) )->size <= 1

inv: parts->select( oclIsKindOf(Wheel) )->size <= 2

inv: Let nrSaddles : Integer = parts->

select(oclIsKindOf(Saddle) )->size in

(type = BicycleType::single implies nrSaddles <= 1)

and (type = BicycleType::tandem implies nrSaddles <= 2)

Restrictions

Within the Bicycle model, we need to add restrictions on the kind of parts that a bicycle (the composite) may contain.
The last restriction even depends on the specific instance of Bicycle.
The operation oclIsKindOf is described later on in this tutorial. It results in true if the object is of the specified type.

Uniqueness constraints

Specify that some value needs to be unique:
context Airline inv: flights->forAll(f1, f2 | f1 <> f2 implies

f1.flightNumber <> f2.flightNumber)

Better:
context Airline inv:
Flights->isUnique(flightNumber)

Multiplicity Constraints

Can be specified in the class model … but only for static constraints:

Multiplicity Constraints

Multiplicity “many” often restricted dynamically
context Flight inv:
passengers->size <= maxNrPassengers

Unlimited upper bounds can be avoided with OCL

Optional Multiplicity

Optional multiplicity often is required or disallowed depending on the state
context Car inv:
self.driving implies driver->notEmpty
context Person inv:
self.age < 18 implies car->isEmpty

The Type of An Object

oclIsTypeOf(Type) is true when the

object is a direct instance of Type

oclIsKindOf(Type)is true when the object is an instance of Type, or any of the subtypes of Type

oclAsType(Type)is the OCL variant of a “type-cast”

All instance of a type

Type.allInstances results in all instances of Type at a certain moment in time

OCL_Slides_Lectures_2_and_3.ppt

The Object Constraint Language

Slides based on your textbook: The Object Constraint Language, Second Edition: Getting Your Models Ready for MDA

Originally presented in the OMG Advanced UML Modeling Tutorial (omg.org) by

Jos Warmer

Acknowledgement: This slide-set is a subset of those presented by Jos Warmer in the OMG Advanced UML Modelling Tutorial

Overview

What are constraints?
Core OCL Concepts
Advanced OCL Concepts
Wrap up

This tutorial is a short introduction to the object constraint language (OCL) which is part of the UML standard.

Definition of constraint

“A constraint is a restriction on one or more values of (part of) an object-oriented model or system.”

First, we need to establish a working definition of constraint.

Different kinds of constraints

Class invariant
a constraint that must always be met by all instances of the class
Precondition of an operation
a constraint that must always be true BEFORE the execution of the operation
Postcondition of an operation
a constraint that must always be true AFTER the execution of the operation

There are a number of constraint types, which can be indicated by using stereotypes that are predefined in UML. There are

class invariants, which are mostly used in class diagrams.
preconditions on operations, which are used in all types of diagrams.
...

Constraint stereotypes

UML defines three standard stereotypes for constraints:
invariant
precondition
postcondition

In a separate document these may be denoted by:

context Class inv:
context Class::operation(...) : returntype pre:
context Class::operation(...) : returntype post:

Constraints and the UML model

OCL expressions are always bound to a UML model
OCL cannot be used independently of UML
Though the OCL syntax for a UML diagram may be contained in a separate document
OCL expressions can be bound to any model element in UML

OCL expressions always put constraints on the elements of a UML model. This model describes which classes may be used and which attributes, operations and associations are available for objects from these classes.

Why use OCL ?

What’s in it

for me?

Use the Object ConstraintLanguage

Before embarking on our journey into the details of OCL, we’ll give you some idea why using constraints can be a good idea for you too.

Can we make this more precise?

Flight

Airplane

CargoFlight

PassengerFlight

PassengerPlane

CargoPlane

0..*

flights

0..*

Many facts about a software system that a modeller would like to express, can not be expressed, or can not easily be expressed in a visual model.

Diagram with added invariants

{context Flight

inv: type = #cargo implies airplane.type = #cargo

inv: type = #passenger implies airplane.type = #passenger}

0..*

Flight

Airplane

type :

enum of cargo, passenger

type :

enum of cargo, passenger

flights

Using constraints simplifies the visual model and often points the way to a more flexible implementation.

Using constraints, we may explore many different variants of combining visual modelling with constraint modelling.

What is OCL?

OCL is
a textual language to describe constraints
the constraint language used in UML models
As well as the UML meta-model
Formal but easy to use
unambiguous
no side effects

OCL is designed to be a formal language. It is precise, unambiguous and has no side effects. It supports strong type checking. Still, OCL is easy to use: to write, read and understand. It is intended to be used by both the ‘normal ‘ programmer and the ‘scientific’ user of UML.

Like a black umbrella, OCL is a formal accessory but easy to use.

Core OCL Concepts

What are constraints
Core OCL Concepts
Advanced OCL Concepts
Wrap up

This tutorial is a short introduction to the object constraint language (OCL) which is part of the UML standard.

Example model

Airport

Flight

Passenger

Airline

$minAge: Integer

age: Integer

needsAssistance: Boolean

departTime: Time

/arrivalTime: Time

duration : Interval

maxNrPassengers: Integer

origin

desti-

nation

{ordered}

arriving

Flights

departing

Flights

CEO

0..1

flights

passengers

book(f : Flight)

0..1

airline

We will use this example model to explain the possibilities of constraints.

Constraint context and self

Every OCL expression is bound to a specific context.
The context is often the element that the constraint is attached to
The context may be denoted within the expression using the keyword ‘self’.
‘self’ is implicit in all OCL expressions
Similar to`this’ in C++

The context of an OCL expression is the starting point for our statement about the complete system. Within the expression we have a shorthand to indicate the constraint context: the word ‘self’. We may even omit this keyword if this is not ambiguous.

Notation

Constraints may be denoted within the UML model or in a separate document.
the expression:

context Flight inv: self.duration < 4

is identical to:

context Flight inv: duration < 4

is identical to:

Flight

duration: Integer

<<invariant>>

duration < 4

In the case that the constraints are written in a separate document the context is written above the expression. If a constraint is written in a note box in the diagram the context is clear from the dotted line.

In English this constraint would mean that all flight objects must have a duration attribute that is less than four.

Note that for reasons of simplicity, the duration attribute in this example is of type Integer, not of type Interval.

Elements of an OCL expression

In an OCL expression these elements may be used:
basic types: String, Boolean, Integer, Real.
classifiers from the UML model and their features
attributes, and class attributes
query operations, and class query operations (i.e., those operations that do not have side effects)
associations from the UML model
Including Rolenames at either end of an association
HINT: use Rolenames on class diagrams to simplify the OCL

An OCL expression can be built using a great number of elements. There are the basic (predefined) types and their (predefined) operations, the classes, interfaces and datatypes from the model.

Because all OCL expressions must be side effect free, only operations that simply return a value but do not change the state of the system, the query operations, may be used. The non-query operations of all classes may not be used within an OCL expression. All attributes and class attributes can be used.

Example: OCL basic types

context Airline inv:

name.toLower = ‘klm’

context Passenger inv:

age >= ((9.6 - 3.5)* 3.1).floor implies mature = true

Naturally, the types and operations used in any programming language are available in OCL. An exception is the extra operation on the Boolean type, one that is well known in mathematics: ‘implies’. Using ‘implies’ means that if the left-hand side is true then also the right-hand side is true.

Model classes and attributes

“Normal” attributes

context Flight inv:

self.maxNrPassengers <= 1000

Class attributes

context Passenger inv:

age >= Passenger.minAge

More interesting elements in an OCL expression come from the UML model.

The writer of OCL expressions can not ‘create’ new types. If there is any need for new types then the UML model should be adequately adapted.

Expressed in natural language the first constraint states that the maximum number of passengers on any flight may not exceed 1000. The second constraint expresses that for every passenger the age attribute must be greater than or equal to the class attribute minAge.

Example: query operations

context Flight inv:

self.departTime.difference(self.arrivalTime) .equals(self.duration)

Time

difference(t:Time):Interval

before(t: Time): Boolean

plus(d : Interval) : Time

Interval

equals(i:Interval):Boolean

Interval(d, h, m : Integer) :

Interval

midnight: Time

month : String

day : Integer

year : Integer

hour : Integer

minute : Integer

nrOfDays : Integer

nrOfHours : Integer

nrOfMinutes : Integer

Expressed in the English language this constraint states that the duration attribute of all flight objects must be equal to the difference between the arrivalTime attribute and the departTime attribute.

Note that difference( ) is an operation of the class Time. Underlined attributes and operations are class-scope (static) attributes and operations

Associations and navigations

Every association in the model is a navigation path.
The context of the expression is the starting point.
Role names are used to identify the navigated association.

Any OCL expression can navigate through the model by following the ‘path’ of the association. The constraint context is the starting point for these navigations and the object(s) on the other side of the association are identified by the rolename. If the rolename is not present then the name of the class may be used (in lower case).

A role name must be present if there are two or more associations between the same two classes.

Example: navigations

context Flight

inv: origin <> destination

inv: origin.name = ‘Amsterdam’

context Flight

inv: airline.name = ‘KLM’

Airport

Flight

departTime: Time

/arrivalTime: Time

duration : Interval

maxNrPassengers: Integer

origin

desti-

nation

arriving

Flights

departing

Flights

In an OCL expression one may put constraints on the associated object or on attributes of the associated object.

The first constraint states that the airport from which a flight is leaving is different from the destination airport.

The second constraint states that for every flight the name of the airport from which it is leaving, must be “Amsterdam”.

The third constraint states that for every flight the name of the airline must be “KLM”.

Association classes

context Person inv:

if employer.name = ‘Klasse Objecten’ then

job.type = #trainer

else

job.type = #programmer

endif

Person

Company

Job

employee

employer

type : {trainer, programmer}

name : String

When the UML model contains an association class, constraints can be made on instances of this association class using the class name (in lower case). The class ‘on the other side’ of the association may be navigated using the rolename (or class name if the role name is not present).

The ‘#’ symbol indicates that the value is of an enumerated type

The OCL Collection types

What are constraints
Core OCL Concepts
Collections
Advanced OCL Concepts
Wrap up

This tutorial is a short introduction to the object constraint language (OCL) which is part of the UML standard.

Significance of Collections in OCL

Most navigations return collections rather than single elements

0..*

Flight

Airplane

type :

enum of cargo, passenger

type :

enum of cargo, passenger

flights

Three Subtypes of Collection

Set:
arrivingFlights(from the context Airport)
Non-ordered, unique
Bag:
arrivingFlights.duration (from the context Airport)
Non-ordered, non-unique
Sequence:
passengers (from the context Flight)
Ordered, non-unique

OCL distinguishes between three kinds of collections:

a set is a collection in which every element can be present only once.
a bag is a collection in which an element can be present more than one time.
a sequence is an ordered bag.

Set, Bag, and Sequence all inherit features from the abstract Collection type.

When you navigate more than one association with a multiplicity greater than 1, you always end up with a Bag. When you navigate just one association with a multiplicity greater than 1 you always get a Set.

A Bag can be converted to a Set with the asSet operation (often needed when you want to identify how many non-identical elements are in a Bag) ; similarly conversions to Bags and Sequences can be made with asSequence and asBag.

Collection operations

OCL has a great number of predefined operations on the collection types.
Syntax:
collection->operation

Use of the “->” (arrow)

operator instead of the

“.” (dot) operator for predefined operations

There are a large number of predefined operations on collections, e.g. isEmpty, size, includes, union, etc. An arrow, instead of a dot, before the operation indicates use of one of these collection operations. The reason is, of course, to avoid name clashes with operations defined in the model.

The collect operation

Syntax:

collection->collect(elem : T | expr)

collection->collect(elem | expr)

collection->collect(expr)

Shorthand:

collection.expr

The collect operation results in the collection of the values resulting evaluating expr for all elements in the collection
Shorthand often trips people up. Be Careful!

The collect operation is one of the operations on collections that are used most often. It iterates over the collection, computes a value for each element, and gathers the evaluated values into a new collection.

Its syntax has three variants. Whenever it is clear what the type of the elements in the collection is ‘: T’ may be omitted. The second variant is used when ‘elem’ has to be referred to explicitly in the expression, in other cases ‘elem |’ may be omitted.

Because the collect is used so may times, a shorthand notation was introduced. This can be used when the expression ‘’expr” is a single attribute, operations or association.

The select operation

Syntax:

collection->select(elem : T | expression)

collection->select(elem | expression)

collection->select(expression)

The select operation results in the subset of all elements for which expression is true

The select and reject operations also result in a new collection, but the elements in this new collection always have the same type as the elements in the ‘old’ collection.

The select and reject operations have the same syntactical variants as the collect operation. The shorthand notation can not be used, because it can not be distinguished from the collect operation.

Example: collect operation

context Airport inv:

self.arrivingFlights -> collect(airLine) ->notEmpty

airp1

airp2

airline1

airline2

airline3

departing flights

arriving flights

When the invariant on the previous sheet is evaluated for Airport “airp1” we get the following results:

self.arrivingFlights is the collection { f4, f5 }

self.arrivingFlights->collect(airline) follows the airline link from f4 and f5 and results in the collection { airline2, airline3 }

Therefore the constraint holds true for airp1

The forAll operation

Syntax:
collection->forAll(elem : T | expr)
collection->forAll(elem | expr)
collection->forAll(expr)
The forAll operation results in true if expr is true for all elements of the collection

The forAll operation can be used to specify that a certain condition holds for all elements of a collection. The forAll operation has the same syntactical variants as the collect operation.

Example: forAll operation

context Airport inv:

self.departingFlights->forAll(departTime.hour>6)

departing flights

arriving flights

airp1

airp2

airline1

airline2

airline3

depart = 8

depart = 7

depart = 9

depart = 5

depart = 8

When the invariant on the previous sheet is evaluated for Airport “airp1” we get the following results:

self is the object "airp1"

self.departingFlights is the collection { f1, f2, f3 }

departTime.hour >= 6 is true for f1 but false for f2. Therefore the forAll results in false and the constraint is broken.

The exists operation

Syntax:

collection->exists(elem : T | expr)

collection->exists(elem | expr)

collection->exists(expr)

The exists operation results in true if there is at least one element in the collection for which the expression expr is true.

Again, the exists operation has the same syntactical variants as the collect operation.

Example: exists operation

context Airport inv:

self.departingFlights->exists(departTime.hour<6)

departing flights

arriving flights

airp1

airp2

airline1

airline2

airline3

depart = 8

depart = 7

depart = 9

depart = 5

depart = 8

When the invariant on the previous sheet is evaluated for Airport “airp1” we get the following results:

self is the object "airp1"

self.departingFlights is the collection { f1, f2, f3 }

departTime.hour < 6 is false for f1and f3 but true for f2. Therefore the exists results in true and the constraint is met for airp1

Example: collect operation

context Airport inv:

self.departingFlights->select(duration<4)->notEmpty

departing flights

arriving flights

airp1

airp2

airline1

airline2

airline3

duration = 2

duration = 5

duration = 3

When the invariant on the previous sheet is evaluated for Airport “airp1” we get the following results:

self.departingFlights is the collection { f1, f2, f3 }

self.departingFlights ->select(duration < 4) selects f1 and f3 from the collection and results in the collection {f1, f3}

Since the collection is not empty the constraint holds for airp1

Iterate

The iterate operation for collections is the most generic and complex building block.

collection->iterate(elem : Type;

answer : Type = <value> |

<expression-with-elem-and-answer>)

Another advanced construct in OCL is the iterate operation on Collections. This is both a very complex and a generic operation. With this operation you can write more and more constraints on collections.

Iterate example

Example iterate:

context Airline inv:

flights->select(maxNrPassengers > 150)->notEmpty

Is identical to:

context Airline inv:

flights->iterate (f : Flight;
answer : Set(Flight) = Set{ } |

if f.maxNrPassengers > 150 then

answer->including(f)

else

answer endif )->notEmpty

This slide shows how the select operation is described using the iterate operation. The other collection operations can also be defined in terms of the iterate operation.

Other collection operations

isEmpty: true if collection has no elements
notEmpty: true if collection has at least one element
size: number of elements in collection
count(elem): number of occurences of elem in collection
includes(elem): true if elem is in collection
excludes(elem): true if elem is not in collection
includesAll(coll): true if all elements of coll are in collection

This list is not exhausting, there are more collection operations. The operations mentioned in this tutorial are the ones used most often.

What are constraints
Core OCL Concepts
Advanced OCL Concepts
Wrap up

Advanced OCL Concepts

Result in postcondition

Example pre and postcondition

context Airline::servedAirports() : Set(Airport)

pre : -- none

post: result = flights.destination->asSet

The postcondition states that the return value of the operation is the set of airports where flights of this airline arrive.

Statechart: referring to states

The operation oclInState returns true if the object is in the specified state.

context Bottle inv:

self.oclInState(closed) implies filled = #full

Bottle

filled : enum {empty, half, full}

open

closed

A statechart for a class defined the states that an object of that class can be in.

In OCL expressions one can use this state information. This shows that statecharts and class diagrams are directly connected.

Local variables

The let construct defines variables local to one constraint:

Let var : Type = <expression1> in <expression2>

Example:

context Airport inv:

Let supportedAirlines : Set (Airline) =
self.arrivingFlights -> collect(airLine) in (supportedAirlines ->notEmpty) and
(supportedAirlines ->size < 500)

New since the UML version 1.3 is the let construct. This construct lets you define a variable local to the OCL expression, i.e. it may only be used in this expression.

Inheritance of constraints

Guiding principle Liskov’s Substitution Principle (LSP):
“Whenever an instance of a class is expected, one can always substitute an instance of any of its subclasses.”

Inheritance of constraints, invariants as well as pre- and postconditions, is a difficult subject.To determine the meaning of inheritance of constraints within OCL we used Liskov’s Substitution Principle as guideline.

Inheritance of constraints

Consequences of LSP for invariants:
An invariant is always inherited by each subclass.
Subclasses may strengthen the invariant.
Consequences of LSP for preconditions and postconditions:
A precondition may be weakened (contravariance)
A postcondition may be strengthened (covariance)

The conseqeunce of this principle is that invariant are always inherited by its subclasses. Subclasses may strengthen the invariant, not weaken it.

What are constraints
Core OCL Concepts
Advanced OCL Concepts
Wrap up

Wrap Up

Current Developments

Feedback from several OCL implementers handled in UML-RTF
e.g. the grammar has some loose ends
typical tool-related issues
Development of OCL metamodel
currently concrete syntax only
will result in abstract syntax
UML 2.0 RFP
meta-model as part of the UML meta-model
additional capabilities (e.g., business rules)

OCL Tools

FREE parser from IBM
http://www.software.ibm.com/ad/ocl
Cybernetics
www.cybernetic.org
University of Dresden
www-st.inf.tu-dresden.de/ocl/
Boldsoft
www.boldsoft.com
ICON computing
www.iconcomp.com
Royal Dutch Navy
Others … …

Conclusions and Tips

OCL invariants allow you to
model more precisely
remain implementation independent
OCL pre- and postconditions allow you to
specify contracts (design by contract)
specify interfaces of components more precisely
OCL usage tips
keep constraints simple
always combine natural language with OCL
use a tool to check your OCL

Further Resources for OCL

The Object Constraint Language
ISBN 0-201-37940-6
OCL home page
www.klasse.nl/ocl/index.htm

More information on OCL can be found in these references.

References

[UML 1.3] OMG UML Specification v. 1.3, OMG doc# ad/06-08-99
[UML 1.4] OMG UML Specification v. 1.4, UML Revision Task Force recommended final draft, OMG doc# ad/01-02-13.

Web:
UML 1.4 RTF: www.celigent.com/omg/umlrtf
OMG UML Tutorials: www.celigent.com/omg/umlrtf/tutorials.htm
UML 2.0 Working Group: www.celigent.com/omg/adptf/wgs/uml2wg.htm
OMG UML Resources: www.omg.org/uml/
Email
[email protected]
Contributors

Further Info

oz-ocl-mapping.pdf

OBJECT-Z TO OCL DICTIONARY

OZ OCL Comments

-- OZ: Use brackets and text in other font /* */ OZ: Text surrounding class schemas a.any(b) a.asBag() a.asOrderedSet() a.asSequence() a.asSet()

a.collectNested(b) OZ: Not needed; “collections” work just as they are defined.

a.flatten() OZ: Not needed; “collections” work just as they are defined.

a.floor() a.hasReturned() OZ: No notion of time; not needed. a.indexOf() a.insertAt(b) a.isOperationCall() a.isSignalSent() a.isUnique() a.iterate() a.oclAsType() a.oclInState() a.oclIsKindOf() a.oclIsNew() OZ: Not needed. Objects always exist. a.oclIsTypeOf() a.oclIsUndefined() a.result() a.round() a.sortedBy() a.subOrderedSet(n, m) a.subsequence(n, m) a.substring(b) a.substring(b) a.substring(n, m) a.toInteger() a.toLower() a.toReal() a.toUpper() a::b OZ: No notion of packages a^^b() a->b() OZ: Not needed

OZ OCL Comments attr Collection OZ: Abstract class, not needed context OZ: Class or operations schema derive OZ: Class invariant inv OZ: Predicates in class state oper OrderedSet package – endpackage OZ: No notion of packages post OZ: Predicates in operation pre OZ: Predicates in operation result OZ: Explicitly declared output variable String � OCL: Containment on UML Class Diagram − # { a : T × exp } a.count(exp) #a a.size() Σ a.sum() (a \ b) ¼ (b \ a) –or- (a ¼ b) \ (a » b)

a.symmetricDifference(b)

(a, b, c) Tuple {a, b, c} (Øa Ù b) Ú (a Ù Øb) a xor b { a : T × exp} a.select(exp) { a : T × Ø exp} a.reject(exp) | a | a.abs() ¡ a Set (a) ¡¦ a Set (a); a->size() > 0 ¯ ¸ Set { } ¿ Generalized union ˜ ^ Roughly › OCL: Polymorphic by default == def ± « ∄ b not a.exists(b) ¢ ¢¦ ¤ Integer ¥ Real © ¬ ® °

OZ OCL Comments † Distributed ‡ Distributed ‰ Generalized ¾ Generalized intersection a a@pre ª Á À ^ Roughly Â Ä Ã Å a - b a - b a * b a * b a : £ a : Integer; a >= 0 a : £¦ a : Integer; a > 0 a : b a : b a \ {b} a.excluding(b) a ¨ b Set (a x b) a + b a + b a < b a < b a = ¸ a.isEmpty() a = b a = b a > b a > b a » b a.intersection(b) a § b Tuple {a, b} a µ ¸ a.notEmpty() a µ b a <> b a ¼ {b} a.including(b) a ¼ b a.union(b) a ½ b a - b for set a ² b a.product(b) a ² b ² c TupleType (a, b, c) a ä b a >= b a ã b a <= b a div b a.div(b) a Ê b a.append(b) a Ê b a.concat(b) a mod b a.mod(b) a Ú b a or b a Ù b a and b a Û b a implies b a Ü b a implies b and b implies a a..b a .. b

OZ OCL Comments a.b a.b a.n a.at(n) a’ a a’ = a \ { b } a = [email protected](b) a’ = a ¼ { b } a = [email protected](b) Æ b ´ a a.excludes(b) b ¹ a a.includesAll(b) and a <> b proper subset b ³ a a.includes(b) b Ê a a.prepend(b) b º a a.includesAll(b) Ç disjoint < a, b > a.excludesAll(b) dom É È Ë Distributed concatenation enum ::= a | b | c enum::element_name OCL: Declared on UML Class Diagram false false first For ordered pair front head a a.first() Ï Ð { } Ì() OCL: In UML Class Diagram

Ïa, bÐ partition c a.excludesAll(b) and a.union(b) = c

id if then else if – then – else - endif INIT init OCL: In context of attribute not class iseq last a a.last() let let – in max (a, b) a.max(b) min (a, b) a.min(b) Ñ c : T(exp) × exp-withb Ò

a.collect(b : T | exp-with- b)

Ñ Ò Bag{}

ó OCL: In UML Class diagram (private derived attribute)

ö õ Ø a not a Ö a : A | exp-a × exp-b exists(exp-a and exp-b) Õ a : T a.allInstances()

OZ OCL Comments Ö a : T × exp a.exists(exp) Ó Ô ó() OCL: Can use ‘–- modifies’ and ‘-- query’ Ö¦ a : T × exp a.one(exp) Õa : A | exp-a × exp-b forAll(exp-a implies exp-b) Õa : T × exp a.forAll(exp) œ Boolean ran rev š second For ordered pair self self seq Sequence seq¦ a : Sequence ; a.Size() > 0 succ a a + 1 tail true true ™ ^ Roughly

Notes:

1. OZ class members (attributes from State Schema, Axiomatic Definitions, derived attributes, and Operations) are declared on UML Class Diagram.

2. Generally, OZ set variables are association ends on UML Class Diagram.

3. Predicates of OZ axiomatic definitions are expressed as class invariants in OCL.

4. OZ inheritance is shown as generalization on UML Class Diagram.

5. OZ visibility is also indicated on the UML Class Diagram.

6. To state that an object has been added to an existing set use: setName->including(object). This asserts that the previous contents are still there and that the object has been added. Using ‘includes’ would only show that it is in the set but doesn’t say anything about the set’s previous contents.

7. Object creation is handled in a function that returns an object of the desired type. Inside the function, you access the objects attributes to set their values via ‘result’.

8. OCL [0..1] association roles are of type ‘Type’ not ‘Set’. Therefore, to initialize an empty role you have to use the “init: OclUndefined” syntax instead of “Set { }”.

9. Generally, OZ class invariants involving universal quantification in OCL have to be expressed as class invariants of the containing class so that the ‘exists()’ operator has access to all instances of the class being constrained.

10. Where OZ would use schema composition operators, OCL uses the notion of messages being sent.

OZ OCL Comments

� OCL: Containment on UML Class Diagram − ¯ ¿ Generalized union › OCL: Polymorphic by default ± « ¢ ¢¦ © ¬ ® ° † Distributed ‡ Distributed ‰ Generalized ¾ Generalized intersection ª Á Â Ä Ã Å Æ Ç dom É È Ë Distributed concatenation first For ordered pair front Ì() OCL: In UML Class Diagram id iseq

ó OCL: In UML Class diagram (private derived attribute)

ö õ Ó Ô ó() OCL: Can use ‘–- modifies’ and ‘-- query’ ran rev

OZ OCL Comments š second For ordered pair tail -- OZ: Use brackets and text in other font /* */ OZ: Text surrounding class schemas ˜ ^ Roughly À ^ Roughly ™ ^ Roughly Ï Ð { } a’ a a - b a - b a ½ b a - b for set a * b a * b a..b a .. b a : b a : b a : £¦ a : Integer; a > 0 a : £ a : Integer; a >= 0 seq¦ a : Sequence ; a.Size() > 0 succ a a + 1 a + b a + b a < b a < b a ã b a <= b a µ b a <> b a’ = a \ { b } a = [email protected](b) a’ = a ¼ { b } a = [email protected](b) a = b a = b a > b a > b a ä b a >= b a Ù b a and b a Û b a implies b a Ü b a implies b and b implies a a Ú b a or b (Øa Ù b) Ú (a Ù Øb) a xor b | a | a.abs() Õ a : T a.allInstances() a.any(b) a Ê b a.append(b) a.asBag() a.asOrderedSet() a.asSequence() a.asSet() a.n a.at(n) a.b a.b Ñ c : T(exp) × exp-withb a.collect(b : T | exp-with-

OZ OCL Comments Ò b)

a.collectNested(b) OZ: Not needed; “collections” work just as they are defined.

a Ê b a.concat(b) # { a : T × exp } a.count(exp) a div b a.div(b) b ´ a a.excludes(b) disjoint < a, b > a.excludesAll(b)

Ïa, bÐ partition c a.excludesAll(b) and a.union(b) = c

a \ {b} a.excluding(b) Ö a : T × exp a.exists(exp) head a a.first()

a.flatten() OZ: Not needed; “collections” work just as they are defined.

a.floor() Õa : T × exp a.forAll(exp) a.hasReturned() OZ: No notion of time; not needed. b ³ a a.includes(b) b º a a.includesAll(b) b ¹ a a.includesAll(b) and a <> b proper subset a ¼ {b} a.including(b) a.indexOf() a.insertAt(b) a » b a.intersection(b) a = ¸ a.isEmpty() a.isOperationCall() a.isSignalSent() a.isUnique() a.iterate() last a a.last() max (a, b) a.max(b) min (a, b) a.min(b) a mod b a.mod(b) a µ ¸ a.notEmpty() a.oclAsType() a.oclInState() a.oclIsKindOf() a.oclIsNew() OZ: Not needed. Objects always exist. a.oclIsTypeOf() a.oclIsUndefined() Ö¦ a : T × exp a.one(exp) b Ê a a.prepend(b) a ² b a.product(b)

OZ OCL Comments { a : T × Ø exp} a.reject(exp) a.result() a.round() { a : T × exp} a.select(exp) #a a.size() a.sortedBy() a.subOrderedSet(n, m) a.subsequence(n, m) a.substring(b) a.substring(b) a.substring(n, m) Σ a.sum() (a \ b) ¼ (b \ a) –or- (a ¼ b) \ (a » b)

a.symmetricDifference(b)

a.toInteger() a.toLower() a.toReal() a.toUpper() a ¼ b a.union(b) a::b OZ: No notion of packages a a@pre a^^b() a->b() OZ: Not needed attr Ñ Ò Bag{} œ Boolean Collection OZ: Abstract class, not needed context OZ: Class or operations schema == def derive OZ: Class invariant enum ::= a | b | c enum::element_name OCL: Declared on UML Class Diagram Ö a : A | exp-a × exp-b exists(exp-a and exp-b) false false Õa : A | exp-a × exp-b forAll(exp-a implies exp-b) if then else if – then – else - endif INIT init OCL: In context of attribute not class ¤ Integer inv OZ: Predicates in class state let let – in Ø a not a ∄ b not a.exists(b) oper OrderedSet

OZ OCL Comments package – endpackage OZ: No notion of packages post OZ: Predicates in operation pre OZ: Predicates in operation ¥ Real result OZ: Explicitly declared output variable self self seq Sequence a ¨ b Set (a x b) ¡ a Set (a) ¡¦ a Set (a); a->size() > 0 ¸ Set { } String true true (a, b, c) Tuple {a, b, c} a § b Tuple {a, b} a ² b ² c TupleType (a, b, c)