0

在下面

sig building{
    abv: Man -> Man
 }
 {
 all m:Man | Above(m,m.abv)
 }

下面是什么意思？它与签名定义有什么关系？这是 sig 的关系吗？

 {
 all m:Man | Above(m,m.abv)
 }
4

1 回答 1

1

这称为“附加事实”，意思是它必须适用于相应 sig 的所有原子。因此，您的模型的等效事实是

fact {
  all b: building |
    all m: Man | Above[m, m.(b.abv)]
}

在附加事实中，您可以使用this关键字来引用相应 sig 的当前原子，因此编写附加事实的更清晰的方法是显式地写入m.(this.abv)，而不是依赖于abv隐式扩展为this.abv.

于 2012-11-22T15:02:46.033 回答