文章/答案/技术大牛

发布

问三元关系中的多重性
EN

Stack Overflow用户

提问于 2012-09-19 19:17:56

回答 1查看 1K关注 0票数 2

三值关系中的下界多重性some和one的语义很难理解.根据软件摘要(修订版)第79-80页关系addr: Book -> (Name -> some Addr)应等同于all b: Book | b.addr in Name -> some Addr (另见第97页)。但后一个公式到底是什么意思呢？我的想象力在这里失败了。这就是为什么我在合金分析器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

保持(没有发现反例)。因此，如果有任何图书，每个名称应该注册在其中的至少一本。允许使用无文档的Addrs，而如果没有Books，就会突然出现无文档的名称。

以下模式的含义：

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

因此，如果有任何图书，所有名称都应该参与关系addr1，所有Addrs都应该参与addr2。多重性one的行为相似。

软件抽象和分析器似乎没有讲述类似R: a -> (B m -> n C)E 217之类的构造，但我可能遗漏了一些东西。我发现的暗示不是我所期望的，而且可能还有其他一些我还没有发现的奇怪的暗示。越来越多的我觉得嵌套的下限多重性完全没有意义。我能说得对吗？

alloy

回答 1

Stack Overflow用户

回答已采纳

发布于 2012-09-21 18:53:18

第一个例子使我困惑了很长一段时间；它使我感到惊讶的是，在任何情况下都没有未映射的名称。然而，在第一版的第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 (no )上没有显式的多重性，我花了一段时间阅读这本书，找出关系上的默认多重性约束的规范(类似于其他字段的默认one )，并尝试各种编写等效约束的方法，然后得出没有默认多重性约束的结论；相反，默认的是没有多重性约束。因此，第78页上给出的第二条重写规则不适用于Name -> some Addr；不存在多重性约束，其效果是，对于附加的每个a，可能有零个或多个(b.addr).a的实例。

我想从语言设计的角度来看，我认为有一个显式的set“默认多重性约束”和允许类似的语句可能会有所帮助。

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

意思是每个地址在b.addr中可能有零个或更多的条目。

但我倾向于认为，不管有没有这样的变化，你仍然可以正确地说，some和one在三元关系中的作用可能很难理解。

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/12501430

复制

相似问题

问三元关系中的多重性
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问三元关系中的多重性EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问三元关系中的多重性
EN