7.8 解析属性

对于任意属性（attribute, 操作，或是导航）其完整的表示要包含该属性所属的对象。正如在7.3.3 不变式 中所看到的，self可以省略，集合操作中的迭代器变量也一样。在表达式的任何地方，只要迭代器被省略，那么就会引入一个隐式的迭代器变量。举个例子：

context Person inv:
    employer->forAll(employee->exists(lastName=name))

该例引入了三个隐含变量。第一个是self，它总是约束开始的实例。第二个是由forAll引入的隐式迭代器，第三个是由exists隐式引入的迭代器。隐式的迭代器变量没有名称。属性employer, employee, lastName和name所属的对象也都被省略。需要按如下规则来对它们进行解析：

• employer处有一个隐式的变量：self : Person。因此，employer必须是self的一个属性。
• employee处有两个隐式的变量：self : Person和iter1 : Company。因此，employee（译者注：规范中是employer，译者认为是一处错误）必须是self或iter1二者之一的一个属性。如果employee既是slef又是iter1的属性，那么它被定义为属于最内层变量，即iter1。
• lastName和name处有三个隐式的变量：self : Person, iter1 : Company 和 iter2 : Person。因此，lastName和name必须是self, iter1, iter2三者之一的属性。在该UML模型中，name是iter1的属性。然而，lastNamee既是slef又是iter2的属性。这存在二义性因此lastName指的是最内层变量，即iter2。

下述两个不变式约束都是正确的，但具有不同的含义：

context Person
    inv: employer->forAll(employee->exists(p | p.lastName = name))
    inv: employer->forAll(employee->exists(self.lastName = name))

一个closure迭代可能在每一层递归都引入一个隐含迭代器变量，因此有多个迭代器变量候选可以做为隐式的self。既然所有的候选都具有相同的静态类型，它只能是最外层嵌套的候选。