分离逻辑的例子？

Question

分离逻辑的例子？

logic

3

有人可以解释一下这个分离逻辑的例子吗？

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

Example

- Hoang-Mai Dinh

1

这个问题属于http://cstheory.stackexchange.com/。 - Thomash

感谢您的评论，我将在cstheory.stackexchange.com上提出问题。 - Marco Dinh

2个回答

0

这些是关于分离逻辑的公理。我能理解第一个、第二个和最后一个，但是我不能理解第三个。

有人可以解释一下吗？"[X/x]" 是什么意思？

"在 e 中的每个 x 都将被替换为 X"，是这样吗？

enter image description here

- Marco Dinh

1

{X = x /\ e -> Y} x := [e] {e[X/x] -> Y /\ Y = x} 表示：考虑一个包含某个值 Y 的堆，其中有一个位置 e，以及存储位置 x 包含一个值 X。执行 x := [e] 会导致堆中的位置 e[X/x] 包含相同的值 Y，而存储位置 x 现在包含值 Y。执行此语句不会影响堆（仍然只有一个包含值 Y 的位置），但会影响存储位置 x。Y 和 X 只是占位符变量，用于表示前后关系。这个表达式非常通用，可以适应例如 x := [x + 1] 的情况。 - Ptival

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Ptival · Accepted Answer

第一行表示堆只包含一个堆块，其中存储在store中的引用x指向它，且它包含值4,4。

对于A来说是错误的，因为它忘记了y指向的堆块（它没有正确地描述整个堆）。

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

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

第三行仅在A中正确，因为在B中，指向4,4的堆块不是不相交的。

第四行仅在B中正确，因为它表示整个堆都包含x引用的4,4和y引用的4,4。在A中不正确，因为A包含两个不相交的4,4副本，因此应使用分离合取式进行描述。