logic - 分离逻辑的例子？

Question

谁能解释一下这个分离逻辑的例子？

第一行和第二行有什么区别？

Answer 1

第一行说堆只包含一个小堆，因此存储中的引用 x 指向它，并且它包含值 4,4。

在 A 中为假，因为它忘记了 y 指向的小堆(它没有正确表征整个堆)。

---

第二行表示堆可以分成两个不相交 heaplet，这样其中一个由引用 x 指向并包含 4,4 和第二个可以是任何东西。

在A中，第二个heaplet可以是y指向的那个。在 B 中，第二个小堆可以是 emp。

---

第三行仅在 A 中为真，因为在 B 中指向 4,4 的 heaplet 不相交。

---

第四行仅在 B 中为真，因为它说整个堆可以描述为包含 4,4 被 x 引用，并且包含 4,4被 y 引用。它在 A 中不正确，因为 A 包含 4,4 的两个不相交的副本，因此应该使用分隔连词来描述它。