Resolving Properties
For any property (attribute, operation, or navigation), the full
notation
includes the object of which the property is taken. As seen in Section
7.3.3, self can be left implicit, and so can the iterator variables
in collection operations. At any place in an expression, when an
iterator
is left out, an implicit iterator-variable is introduced. For example
in:
context
Person
inv:
employer->forAll(
employee->exists(
lastName = name) )
three implicit variables are introduced. The first is self,
which
is always the instance from which the constraint starts. Secondly an
implicit
iterator is introduced by the forAll and third by the exists.
The implicit iterator variables are unnamed. The properties employer,
employee,
lastName
and name all have the object on which they are applied left
out.
Resolving these goes as follows:
-
at the place of employer there is one implicit variable:
self
: Person. Therefore employer must be a property of self.
-
at the place of employee there are two implicit variables:
self
: Person and iter1 : Company. Therefore employer must
be a property of either self or iter1. If employee
is a property of both self and iter1 then it is defined
to
belong to the variable in the most inner scope, which is iter1.
-
at the place of lastName and name there are three
implicit
variables: self : Person , iter1 : Company and iter2
:
Person. Therefore lastName and name must both be
a property
of either self or iter1 or iter2. In the UML
model
property
name is a property of iter1. However, lastName
is a property of both self and iter2. This is
ambiguous
and therefore the
lastName refers to the variable in the most inner
scope, which is
iter2.
Both of the following invariant constraint are correct, but have a
different
meaning:
context
Person
inv:
employer->forAll(
employee->exists( p | p.lastName = name) )
inv:
employer->forAll(
employee->exists( self.lastName = name) )