合金中的关系产品

Question

我有以下签名

Sig Name, Addr {}
Sig Book { addr: Name -> lone Addr }

我想为删除操作定义一个谓词，即删除名称为n的地址。

pred remove [b, b':Book, n: Name] {
   // What to do?
}

其中b 和b' 表示书的前/后状态。

谢谢！

Answer 1

pred remove [b, b':Book, n: Name] {
    b'.addr = b.addr - n -> Addr
}