Model-Driven Engineering - Model-Driven and Software Product Line Engineering - page 69

the global context or an element of the considered diagram.
The textual notation provides the context keyword, but, in
addition, we should also define the kind of information. An
invariant specifies a property, which must hold at each state
of the computation. This is a common property in computer
science and it is expressed by the inv keyword. A simple
invariantfor Attribute couldbe context Attribute inv:
not(name = "") . The context notation must denote the
exact element, and sometimes it is required to apply the ::
operator to navigate inside a package or inside a class. For
instance, context foo::bar::Attribute denotes the class
Attribute in package bar inside the foo package. In such a
context,aswithOOPinamethod,itcouldbeusefultoreference
the receiver object that is denoted by Self as in context
Attribute inv: not(Self.name = "Foo") .

To specify a method is a bit more complex;the first task is to
define the name, the parameters, and the resulting type. The
keywords pre and post are related to the description of the
pre-conditions and post-conditions (as per the usual Hoare's
meaning[HOA69]).Asimpleexampleforamethodthatchecks
if the attribute name is equal to some name n is given in
Listing 3.1.

1 context Attribute :: check(String n): Boolean
2 pre: not( Self .name=
3 post: result = (Self.name = n)

"" )

Listing 3.1. OCL method behavior

The keyword result denotes the value returned by the
method. The meaning of this expression is the following: if the
pre-conditions hold (that is the name exists) then after the call
to check thepost-conditionisensured(i.e.thefunctionreturns
if the name is equal to n or not).

Sometimes, auxiliary variables are required and can be
defined using the let <variable>:<Type> = <request>