下面是电子邮件地址簿的Alloy模型 . 地址簿中的每个名称都映射到名称或地址 .
我希望每个名称最终映射到一个地址,例如,Family - > Tom - > Tom_addr . 我创建了一个实现这个的事实 . 为了检查我的事实是否正确,我创建了一个断言 .
我对这个断言中的内容感到困惑很长一段时间 . 奇怪的是,我放在“事实”部分中的表达似乎是置于断言中的正确表达式 . 但那么断言只会重复这个事实,这是没有用的 . 所以我在assert中创建了其他东西 .
我并不完全相信我在“断言”部分放置的内容实际上会检查每个名称最终都会映射到一个地址 .
问题:
在“事实”部分,我是否正确地表达了每个名称最终映射到地址的约束?
在“断言”部分,是否有更好的方法断言每个名称最终映射到一个地址?
sig Addr {}
sig Name {
address: some Addr + Name
}
fact {
// No cycles.
no n: Name | n in n.^address
// All names eventually map to an Addr.
// Here's how I implemented the constraint:
// There is no name n that is mapped-to (i.e., m -> n),
// which does not map-to something (i.e., n -> p).
no n: Name {
n in univ.address
n not in address.univ
}
}
assert All_names_eventually_map_to_an_Addr {
all n: Name | some n.^address & Addr
}
check All_names_eventually_map_to_an_Addr
1 回答
重复这个事实的断言是你可能不想拥有的东西,因为它确实有用 . (考虑在假设下检查/证明 property - 形式(Q和P)的含义意味着P明显适用于任何P和Q.)
有了这个说, property :
应正确表达,如代码段中所示 . (闭包只能映射到
Address
的一个元素,因为没有为Address
的实例定义关系address
. )