分离逻辑的例子？

Question

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

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

Answer 1

第一行表示堆仅包含一个 heaplet，因此存储中的引用 x 指向它，并且它包含值4,4。

它在 A 中是错误的，因为它忘记了 y 指向的 heaplet（它没有正确描述整个堆的特征）。

第二行表示堆可以分为两个不相交的heaplet，其中一个由引用 x 指向并包含4,4，第二个可以是任何内容。

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

第三行仅在 A 中成立，因为在 B 中指向的 heaplets4,4不是不相交的。

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