了解合金中的复杂特征

Question

在下面

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

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

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

Answer 1

这就是所谓的“附加事实”，意思是它必须对对应sig的所有原子都成立。因此，您的模型的等效事实是

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

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