1

Alloy の次の仕様を検討してください。

sig Books {}
fun f[b:Books] : Books {

    {b':Books | b' = Books -b }
}
run show {}

$univ = {Books$0, Books$1, Books$2}$ のインスタンスがあるとします。関数 f を $Books$0$ で評価すると、${Books$1, Books$2}$ の代わりに空のセットが生成されます。

f[Books$0]
{}

理由はありますか？

4

1 に答える 1

3

これは、集合内包表記の仕組みによるものです。

{b':Books | b' = Books - b }

この式は、と等しいすべてのシングルトンサブセットを提供します。しかし、2要素セットです。したがって、それに等しいシングルトン セットはなく、全体的な結果はです。BooksBooks - bBooks - b{}

あなたはおそらく単に欲しい：

fun f[b:Books] : Books {
   Books - b
}
于 2013-10-29T08:55:16.603 に答える