首页 文章

我怎么能确定我的断言实际上是在检查我要检查的东西?

提问于
浏览
0

下面是电子邮件地址簿的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 回答

  • 1

    重复这个事实的断言是你可能不想拥有的东西,因为它确实有用 . (考虑在假设下检查/证明 property - 形式(Q和P)的含义意味着P明显适用于任何P和Q.)

    有了这个说, property :

    每个名字最终都映射到一个地址

    应正确表达,如代码段中所示 . (闭包只能映射到 Address 的一个元素,因为没有为 Address 的实例定义关系 address . )

相关问题