2

下界多重性some和one三元关系的语义很难掌握。根据Software Abstractions (Rev. ed.) pp.79-80，关系addr: Book -> (Name -> some Addr)应该等同于all b: Book | b.addr in Name -> some Addr（另见 p.97）。但是后一个公式究竟是什么意思呢？我的想象力在这里失败了。这就是为什么我在 Alloy Analyzer 4.1.0 中做了一些实验。该模型的含义：

sig Name, Addr {}
sig Book { addr: Name -> some Addr }
assert implication {
 #Book = 0 or all n: Name | some b: Book, a: Addr | n in b.addr.a
}
check implication

成立（没有找到反例）。因此，如果有任何书籍，则每个名称都应至少在其中一本中注册。允许未记录的地址，并且没有书籍，未记录的名称突然似乎也被允许。

以下模型中的含义：

sig Name, Addr {}
sig Book { addr: Name some -> Addr }
assert implication {
  #Book = 0 or all a: Addr | some b: Book | #b.addr.a > 0
}
check implication

再次持有。这是之前模型的镜像：禁止无证 Addrs，除非根本没有 Book。并且对于名称的文档没有任何限制。

两种模型都可以组合起来更简洁：

sig Name, Addr {}
sig Book { addr1: Name -> some Addr, addr2: Name some -> Addr }
assert implications {
  some Book implies Name in Book.addr1.Addr and Addr in Book.addr2[Name]
}
check implications

因此，如果有任何 Book，所有Names 都应该参与关系 addr1，所有Addr 都应该参与 addr2。多重one性行为相似。

就下界约束而言，似乎软件抽象和分析器并没有讲述关于R: A -> (B m -> n C)之类的构造的相同故事，但我可能遗漏了一些东西。我发现的含义不是我所期望的，并且可能还有其他我尚未发现的奇怪含义。我越来越觉得嵌套的下界多重性根本没有意义。我能说对吗？

4

1 回答 1

1

第一个例子让我困惑了很久。令我惊讶的是，在任何情况下都没有未映射的名称。然而，对于它的价值，我在 p 上找到了。第一版的第 78 条声明“多重性只是一种简写，可以用标准约束代替；多重性约束在

r: A m -> n B

可以写成

all a: A | n a.r
all b: B | m r.b

将这些重写规则中的第一个应用于语句

all b: Book | b.addr in Name -> some Addr

您从第一个示例模型中得出，我们得到

all b: Book | all n: Name | some n.(b.addr)

或者在散文中“对于所有书籍b和名称n ，在b.addr中有一些映射n ”，这至少解决了我最初的困惑。要允许未映射的名称，必须编写或（如 Whirlwind Tour 中后面的示例）。sig Book { addr: set (Name -> Addr) }sig Book { names: set Name, addr: names -> some Addr}

我在第二个重写规则（涉及m的那个）上遇到了更多麻烦。Name(no m )上没有明确的多重性，我花了一些时间翻阅本书以找到关系的默认多重性约束的规范（类似于one其他字段的默认值），并尝试了各种编写等效约束的方法，在得出没有默认多重性约束的结论之前；相反，默认设置是没有多重性约束。所以第二个重写规则在 p 上给出。78 不适用于Name -> some Addr; 没有多重性约束，效果是对于 Addr 中的每个a, (b.addr).a可能有零个或多个实例。

我想从语言设计的角度来看，我认为有一个明确的“默认多重性约束”set并允许像这样的语句可能会有所帮助

all b: Book | all a: Addr | set (b.addr).a
/* currently produces type error */

这意味着每个地址的b.addr中可能有零个或多个条目。

但我倾向于认为，不管有没有这样的变化，你仍然可以说三元关系的影响some和one在三元关系中可能难以掌握。

于 2012-09-21T18:53:18.217 回答