为什么在箭头表达式中使用时字段不同？答案

【问题标题】：Why are fields different when used in an arrow expression?为什么在箭头表达式中使用时字段不同？
【发布时间】：2017-10-25 19:15:26
【问题描述】：

以下签名描述了照片管理应用程序的状态：

sig ApplicationState {
    catalogs: set Catalog,
    catalogState: catalogs -> one CatalogState
}

当然，一个签名会创建一个集合。在这种情况下，它会创建一组 ApplicationState：

ApplicationState0
ApplicationState1
...

目录是一个字段。它将每个 ApplicationState 映射到一组 Catalog 值：

ApplicationState0, Catalog0
ApplicationState0, Catalog1
ApplicationState1, Catalog0
...

catalogState 也是一个字段。它将每个 ApplicationState 映射到一个关系。关系是：

catalogs -> one CatalogState

该关系表示：将目录的每个值映射到一个 CatalogState 值。我们已经看过目录，我将在此重复：

ApplicationState0, Catalog0
ApplicationState0, Catalog1
ApplicationState1, Catalog0
...

因此，关系表示将每个元组映射到一个 CatalogState，如下所示：

ApplicationState0, Catalog0, CatalogState0
ApplicationState0, Catalog1, CatalogState0
ApplicationState1, Catalog0, CatalogState0
...

好的，回到目录状态。之前我们说过它将每个 ApplicationState 映射到一个关系，我们刚刚看到了这个关系是什么。所以，我相信 catalogState 表示与 arity=4 的关系，如下所示：

ApplicationState0, ApplicationState0, Catalog0, CatalogState0
ApplicationState0, ApplicationState0, Catalog1, CatalogState0
ApplicationState0, ApplicationState1, Catalog0, CatalogState0
...

但是，当我运行 Alloy Evaluator 时，它说 catalogState 是一个三元关系。我从这个例子中得出的结论是：

通常，字段名称表示关系。
箭头表达式中使用的字段名称不表示关系。相反，它表示关系的第 2 列（关系的范围）。

是这样吗？这在 Software Abstractions 书中哪里有解释？

【问题讨论】：

标签： alloy

【解决方案1】：

Sofware Abstractions 的第 4.2.2 节（第二版第 97 页）开始

关系被声明为签名字段。

我认为，这至少解决了您的部分问题。（我认为处理“字段”和关系的索引条目并阅读它们指向的每个部分可能会有所帮助。）

你说

箭头表达式中使用的字段名称不表示关系。相反，它表示关系的第 2 列（关系的范围）。

这听起来可能很迂腐，但不是：字段名称总是表示关系。然而，在签名声明的上下文中，它们隐含地以this. 为前缀，这会删除关系的第一列。在您的声明catalogState: catalogs -> one CatalogState 中，对catalogs 的引用确实是对ApplicationState 和Catalog 上的二元关系的引用。但是，在这种情况下，它会默默地扩展为 this.catalogs，它评估为一组 Catalog 个体。关键字this在软件抽象的4.2.2节中介绍。

声明的基数限制也可能是您的示例中的一个复杂因素；我不会在这里解释它们的作用。我只会说，当我遇到基数约束问题时，我经常发现非常仔细地阅读附录 B 中语言参考的相关部分通常足以让我理解发生了什么。（我承认有时它需要阅读不止一次。）

【讨论】：