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:

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) )