三元关系中的多重性-Java 学习之路

三元关系中下界多重性 some 和 one 的语义很难掌握 . 根据Software Abstractions（Rev. ed . ）第79-80页，关系 addr: Book -> (Name -> some Addr) 应该等同于 all b: Book | b.addr in Name -> some Addr （另见第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 . 名称的文档没有任何限制 .

两种型号可以组合使用，配方更简洁：

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关系，所有Addrs都应该参与addr2 . 多重性 one 表现相似 .

似乎软件抽象和分析器并没有讲述关于 R: A -> (B m -> n C) 这样的结构的相同故事，就下限约束而言，但我可能错过了一些东西 . 我发现的含义不是我所预期的，可能还有其他奇怪的含义，我还没有发现 . 我越来越觉得嵌套的下限多重性毫无意义 . 我能说对吗？

1 Answer

1
第一个例子困惑了我很久;令我感到惊讶的是，在任何情况下都没有未映射的名称 . 然而，对于它的 Value ，我在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有一些映射”，这至少解决了我最初的困惑 . 要允许未映射的名称，必须编写 sig Book { addr: set (Name -> Addr) } 或（如旋风之旅后面的示例中） sig Book { names: set Name, addr: names -> some Addr} .

第二次重写规则（涉及m的那个）我遇到了一些麻烦 . 在 Name （没有m）上没有明确的多样性，我花了一些时间浏览这本书，找到关系上的默认多重性约束的规范（类似于其他字段的默认 one ），并尝试各种写作方式在得出没有默认多重性约束的结论之前，等效约束;相反，默认情况是没有多重性约束 . 所以第二次重写规则给出了p . 78不适用于 Name -> some Addr ;没有多重约束，并且效果是对于Addr中的每个a，可能存在零个或多个（b.addr）.a的实例 .

我想从语言设计的角度来看，我认为有一个明确的"default multiplicity constraint"的 set 可能会有所帮助，并允许这样的陈述
```
all b: Book | all a: Addr | set (b.addr).a
/* currently produces type error */
```
意思是每个地址的b.addr中可能有零个或多个条目 .

但我倾向于认为无论有没有这样的改变，你仍然可以说，三元关系中的影响很难掌握 .
Answered 十二月 21, 2018

三元关系中的多重性

1 Answer

Related