合金航海风格背后的理论基础是什么？

Question

在Daniel的“合金通晓的书”中，他写了三种在合金中指定约束的不同风格: 1)谓词演算2)导航样式和3)关系演算。(第3.1节，第34页)

第一种和最后一种方法的理论对我来说是很清楚的，因为第一种是传统的一阶逻辑，当我们把关系作为谓词时；最后一种是关系演算，在关系演算中，一切都是关系，约束是用方程符号和一些代数运算(没有量词)来指定的。在这本书中，有人说是第二个最具表现力的(第35页)。

我的问题：，第二个(即导航风格)背后的理论是什么？在理论上，我应该在哪里寻找(以及使用哪个术语)来获得更多关于这一项的信息。

Answer 1

导航风格的动机是，您希望在谓词演算(它没有对集合或关系进行操作)和关系演算(因为缺乏传递闭包)和关系演算(这给您关系运算符，但没有量词)之间提供一些东西，这对大多数人来说都是很不自然的(但它允许一些漂亮简洁的方法来表达属性)。导航风格介于这两种语言之间，给出了集合/关系运算符和量词，所以在这个意义上--至少在非正式上--如果你仔细定义这三种子语言，它也可能是正式的--它比这两种语言都更具表现力。同时，我的想法是，大多数人对简单的一阶量词很满意，但对关系连接不太满意，因此倾向于编写表达式表示集合的公式。您可以认为这些表达式中的每一个都从某个原子开始，由一个量化的变量表示，然后沿着关系“导航”，得到越来越大的表示原子集合的表达式。这就是我对me.parents.children这样的表达式的看法:你从我开始，导航到我的父母，然后从他们到他们的孩子--结果就是包含我和我兄弟姐妹的集合。根据我的经验，这种导航风格是大多数人天生就喜欢的。

的确，如果您必须从匹配OCL的三种样式中选择一种，那就是这种导航风格，尽管OCL的语义非常复杂(因为在每一步中都会自动发生各种矫顽力和扁平化)，在合金语义学中，它只是标准集和关系。语法可能更受Java等面向对象语言的影响，尽管它们没有合金所具有的那种关系映像(也就是说，如果您有一个字段f并可以编写x.f，那么您就不能从集合xs中的对象中为f映射到的所有对象的集合编写xs.f )。但是请注意，这里没有特殊的语法；这些只是使用相同运算符的样式。

当我在书中写这一页时，我以为它会给读者一些有用的直觉，但它似乎只是造成了更多的混乱！

Answer 2

在附录E-替代方法中，Daniel Jackson讨论了OCL，它具有导航风格。我假设他借用了它的语法，因为他把它作为合金之前的相关工作来讨论。