Eclipse OCL中如何获取集合元素索引？含连续动作约束问题

嗨，我来帮你搞定这个OCL索引的问题！你遇到的indexOf(element)无法识别的情况，核心是OCL语法调用方式不对——得通过序列对象来调用indexOf，而非直接对元素调用。更关键的是，用indexOf判断相邻元素其实不是最优方案，容易出错还效率低，下面给你两种更靠谱的实现方式：

方式一：通过索引遍历序列 #

OCL里的Sequence索引是从1开始的，我们可以直接遍历索引，检查每一对相邻元素：

class Choreography {
    property actions : Action[+|1] { ordered composes };
    attribute name : String[?];
    /* 不允许连续出现两个Rotate类型的动作 */
    invariant rotate_succ: 
        self.actions->asSequence()->forAll(i : Integer | 
            i >= 1 and i < self.actions->size() implies 
                not (self.actions->at(i).oclIsTypeOf(Rotate) and self.actions->at(i+1).oclIsTypeOf(Rotate))
        );
}

• 细节说明：self.actions->asSequence()把有序属性转换成Sequence类型（虽然你的actions已经标记为ordered，但显式转换逻辑更清晰）；
• 遍历从1到size()-1的索引i，检查第i个和第i+1个元素是否同时为Rotate类型，用not确保这种违规情况不会发生。

方式二：用adjacentPairs()简化写法 #

OCL 2.0及以上版本提供了adjacentPairs()方法，它会直接返回序列中所有相邻元素对的序列（比如[a1,a2,a3]会生成[[a1,a2], [a2,a3]]），写法更简洁直观：

class Choreography {
    property actions : Action[+|1] { ordered composes };
    attribute name : String[?];
    /* 不允许连续出现两个Rotate类型的动作 */
    invariant rotate_succ: 
        self.actions->asSequence()->adjacentPairs()->forAll(pair : Sequence(Action) | 
            not (pair->first().oclIsTypeOf(Rotate) and pair->second().oclIsTypeOf(Rotate))
        );
}

• 细节说明：adjacentPairs()帮你自动生成相邻元素对，你只需要遍历这些对，确保没有一对都是Rotate类型即可。

为什么原来的indexOf写法行不通？ #

你原来的代码里indexOf(a1)是错误语法——OCL中必须通过序列对象调用indexOf，比如self.actions->asSequence()->indexOf(a1)。但就算修正了语法，这种写法仍有隐患：如果序列中有重复的Action实例（虽然这里是composes关联，每个Action理论上唯一，但逻辑上仍有风险），indexOf会返回第一个匹配元素的索引，导致相邻关系判断出错。

另外要注意，Eclipse的OCL编辑器对语法版本要求严格，如果你的环境版本较低不支持adjacentPairs()，优先用索引遍历的方式就好。

内容的提问来源于stack exchange，提问作者Marwa