嵌套OCL forAlls

Question

我在一阶逻辑中有以下公式。

forAll a:A | forAll b :B | if a.r1=b then a.r2=b

简单地说，对于A类型的所有对象和B类型的所有对象，如果它们是由r1关联的，那么它们也是由r2关联的。

下面是类图：

​

​

请有人提供上述公式的OCL表示。

Answer 1

这里回答了这个问题。

我重复答案，以遵循堆栈溢出规则：

A.allInstances()->forAll(a | B.allInstances()->forAll(b | a.r1=b implies 
a.r2=b))

这在我看来很笨重！但看起来是这样的！

Answer 2

我没有一种方便的方法来测试这一点，但我认为语法是r1->forall(i | r2->exists(i))。

更简单地说，如果您只想说r1是r2的一个子集，就可以声明它。