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)に依存するのではなく、明示的に書き込むことです。abvthis.abv

于 2012-11-22T15:02:46.033 に答える