合金 - 移除对象时获取空集

Question

考虑以下合金规范：

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

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

假设我们有一个实例 $univ = {Books$0, Books$1, Books$2}$。用 $Books$0$ 评估函数 f 会产生空集而不是 ${Books$1, Books$2}$：

f[Books$0]
{}

有什么想法吗？

Answer 1

这是因为集合理解的工作方式。

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

这个表达式提供了Books 的所有singleton 子集，它们等于Books - b。但是Books - b 是一个二元集合。所以没有单例集等于它，整体结果是{}。

你可能只是想要：

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