首页 文章

4.2中的语义变化?

提问于
浏览
4

我的问题是,合金4.2中字段声明中的()语义是否发生了变化 .

我在“软件抽象”中读到了这一点

addr: (Book -> Name) -> lone Addr

意味着关系addr将 at most 一个地址与每个地址簿和名称对相关联,但这在运行Alloy 4.2时不成立

例如,为

sig Book, Name, Addr  {}
sig AddBX {
  addr : (Book -> Name) -> lone Addr
}

run XRun {
  some B : Book, N : Name, X : AddBX | #X.addr[B][N] = 2
}

Alloy 4.2找到一个模型实例,例如AddBX $ 2

Book$1 ->Name$0 ->Addr$0
Book$1 ->Name$0 ->Addr$1
Book$1 ->Name$0 ->Addr$2

如果我改用

addr : Book -> Name -> lone Addr

然后找不到同一次运行的实例 . 这似乎表明在合金4.2中,这是如何声明关系addr将 at most 一个地址与每个地址簿和名称对相关联,但我想对此进行确认 .

1 回答

相关问题