Home Articles

三元关系中的多重性

Asked
Viewed 773 times
2

三元关系中下界多重性 someone 的语义很难掌握 . 根据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中可能有零个或多个条目 .

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

Related