Separation Logic Review

进步是什么？我们刚才已经说过，是人民永久的生命。

记录一下对 separating conjunction 的理解，即解决一个核心问题：既然$P*Q\Leftrightarrow P\wedge Q\wedge\text{dom}(P)\cap\text{dom}(Q)=\emptyset$，我们为什么还要引入$P*Q$？

1. 在经典中，$\text{dom}(P)$ 并不好判断。有指针的情况下无法判断一个数是地址还是值。此时我们会暂时隐藏，隐含到$*$ 的含义里。
2. $*$ 的目的就是将对$\text{dom}(P)$ 的判断，延缓到具体语句执行时再进行。譬如已经到某一条语句$*p=3$ 时，我们再从 precondition 中 separate 一个含$p$ 的 predicate 出来。此时分离出来的 predicate 的 domain 就是一个$p$。
3. 而且这样做可以将多条语句在语法上分离。更具体地，就是一次 in-place alteration 只可能影响到一个$*$-clause。在 local reasoning 中，我们只需要找到 precondition 中的一个$*$-clause 并分析他在语句执行后的结果。而其他很大一部分的 precondition 都可以利用 frame rule 直接得到。我认为这是 separation logic 在分析大规模程序时的优越性。
4. 但是这在量子中却有问题。因为酉门可以同时作用于两个 qubit，一条语句可以 access 两个$*$-clause，这有违经典 separation logic 的想法。此时即使有 "$*$" 这个 operator，但是也没有起到本质性的作用，因为无法确定有多少个 clause 被影响到了，而且量子下也没有 1. 中所述的问题。

文献：https://doi.org/10.1145/3211968

Key insights:

• Separation logic supports in-place updating of facts as we reason, in a way that mirrors in-place update of memory during execution, and this leads to logical proofs about imperative programs that match computational intuition.
• Separation logic supports scalable reasoning by using an inference rule (the frame rule) that allows a proof to be localized to the resources that a program component accesses (its footprint).
• Concurrent separation logic shows that modular reasoning about threads that share storage and other resources is possible.

Key problem:

"The main difficulty is not one of finding an in-principle adequate axiomatization of pointer operations; rather there is a mismatch between simple intuitions about the way that pointer operations work and the complexity of their axiomatic treatments.…when there is aliasing, arising from several pointers to a given cell, an alteration to a cell may affect the values of many syntactically unrelated expressions.

The use of $*$ rather than the usual Boolean conjunction $\wedge$ ensures that pointers are not aliases (distinct names for the same location).

A central principle is that a command that mutates a single location affects only one $*$-conjunct: operational in-place update is mirrored in the logic, addressing the key difficulty where “an alteration to a cell may affect the values of many syntactically unrelated expressions.”

O’Hearn proposed the following principle of local reasoning, both as a way to describe what was special about SL and as a guiding principle for development of reasoning methods.

“To understand how a program works, it should be possible for reasoning and specification to be confined to the cells that the program actually accesses. The value of any other cell will automatically remain unchanged.”

The frame rule allows to infer that cells remain unchanged when they are not mentioned in a precondition.