1. 分离逻辑基本思想

Reynolds JC. Separation logic: A logic for shared mutable data structures. In: Proc. of the LICS 2002. Copenhagen, 2002. 55−74.

Reynolds JC. An overview of separation logic. In: Proc. of the Verified Software: Theories, Tools, Experiments. Zurich, 2005.

460−469.

分离逻辑是霍尔逻辑的一种扩展。霍尔逻辑是广泛应用的程序验证逻辑系统，用于对命令式语言程序进行推理验证，其基本思想是：在代码段及其调用者之间构建一种合同似的规格说明，由一个前置条件和一个后置条件构成。前置条件是一个断言（assert），描述这个代码段执行前程序状态必须满足的条件；后置条件也是一个断言，描述在代码段正确运行后程序状态所需要满足的条件，调用者可以确信在代码段执行结束后这个状态条件为真。

分离逻辑对程序的推理仍然是采用霍尔三元组{P}C{Q}\{P\} C\{Q\}，其中，PP表示前置条件，QQ表示后置条件，而CC表示代码段。例如：

{x==N} code {x==N∧y==N!}\{x==N\} \text { code }\{x==N \wedge y==N !\}

可以应用到”将变量 x 值的阶乘赋值于 y”程序的验证中。

在分离逻辑中,前置条件和后置条件中的程序状态主要由栈SS和堆HH构成，栈是变量到值的映射，而堆是有限的地址集合到值的映射。在程序验证时，可以将栈看作对寄存器内容的描述，而堆是对可寻址内存内容的描述。

S= def  Variables → Values, H= def  Addresses →fin  Values, States = def S×H.S \stackrel{\text { def }}{=} \text { Variables } \rightarrow \text { Values, } H \stackrel{\text { def }}{=} \text { Addresses } \rightarrow{ }_{\text {fin }} \text { Values, States } \stackrel{\text { def }}{=} S \times H .

分离逻辑对霍尔逻辑的最重要扩展,在于引入了两个新的分离逻辑连接词：分离合取（Separating Conjunction）∗*，分离蕴含（Separating Implication）−∗-*，语义形式化表示如下：

如果令ss表示栈，hh表示堆，h0⊥h1h_0 \perp h_1表示堆h0h_0和h1h_1不相交，h0⋅h1h_0 \cdot h_1表示堆h0h_0和h1h_1的联合，则

[P∗Q]sh= def ∃h0h1⋅h0⊥h1 and h0⋅h1=h and Psh0 and Qsh1. \left[P^* Q\right] s h \stackrel{\text { def }}{=} \exists h_0 h_1 \cdot h_0 \perp h_1 \text { and } h_0 \cdot h_1=h \text { and } P s h_0 \text { and } Q s h_1 \text {. }

[P∗Q]sh\left[P^* Q\right] s h断言整个堆hh被分成两个不相交的部分h0h_0和h1h_1，并且对子堆h0h_0断言PP成立，而对子堆h1h_1断言QQ成立。

[P−∗Q]sh= def ∀h′⋅(h′⊥h and Psh′) implies Qs(h⋅h′). [P-* Q] s h \stackrel{\text { def }}{=} \forall h^{\prime} \cdot\left(h^{\prime} \perp h \text { and } P s h^{\prime}\right) \text { implies } Q s\left(h \cdot h^{\prime}\right) \text {. }

分离蕴含表示，如果当前堆hh通过一个分离的部分h′h^{\prime}扩展，并且对h′h^{\prime}断言PP成立，则对扩展后的堆(h⋅h′)\left(h \cdot h^{\prime}\right)断言QQ成立。

通过使∗*用而不是通常的布尔连接符∧\wedge，确保xx和yy不出现别名混淆，即多个变量指向同一地址。参考下图理解。

分离与、逻辑与

2. 分离逻辑的语法和断言语言

了解分离逻辑的对计算机存储的抽象，便可以如下定义分离逻辑的语法的BNF表示：

v∈V,n∈ Values  Integer Expns i::=v∣n∣i1+i2∣i1−i2∣i1×i2 Pointer Expns k::=v∣v,n∣ null  Boolean Expns b::=T∣F∣i1=i2∣k1=k2∣i1⩽i2∣b1∨b2∣b∣b1∧b2∣b1→b2 Expressions e::=i∣b∣k Assertions p,q::=b∣k↦e∣emp⁡∣p∧q∣p∨q∣p⇒q∣p∗q∣p∣p−∗q∣∀v⋅p∣∃v⋅p\begin{aligned} & v \in V, n \in \text { Values } \\ & \text { Integer Expns } \quad i::=v|n| i_1+i_2\left|i_1-i_2\right| i_1 \times i_2 \\ & \text { Pointer Expns } \quad k::=v|v, n| \text { null } \\ & \text { Boolean Expns } \quad b::=T|F| i_1=i_2\left|k_1=k_2\right| i_1 \leqslant i_2 \mid b_1 \vee b_2|b| b_1 \wedge b_2 \mid b_1 \rightarrow b_2 \\ & \text { Expressions } \quad e::=i|b| k \\ & \text { Assertions } \quad p, q::=b|k \mapsto e| \operatorname{emp}|p \wedge q| p \vee q \mid p \Rightarrow q\left|p^* q\right| p|p-* q| \forall v \cdot p \mid \exists v \cdot p \\ & \end{aligned}

其中，VV表示变量。

分离逻辑对于Hoare逻辑的拓展主要是通过引入4种新的断言形式，以细化对计算机系统存储状态的描述。下面主要介绍这些新引入的断言：

 Assertions p,q::=⋯∣emp 空堆 ∣k↦e 单堆 ∣p∗q 分离合取 ∣p−∗q 分离蕴含 \begin{aligned} &\text { Assertions } \quad p, q::=\cdots\\ &\begin{array}{ll} \mid e m p & \text { 空堆 } \\ \mid k \mapsto e & \text { 单堆 } \\ \mid p^* q & \text { 分离合取 } \\ \mid p-* q & \text { 分离蕴含 } \end{array} \end{aligned}

空堆即堆hh为空；

3. 分离逻辑的推导规则

作为一个形式化系统的推理工具，推导规则在验证过程中起到了很重要的作用。下图包含了分离逻辑中的部分规则，这些规则被分为描述基础数据更改操作的小公理和用于模块化推理的局部推理规则。推理规则可以被理解为“如果横线上面的可以被推导出来，那么就可以推导出横线下的结果”，而公理是已知的可满足公式。

分离逻辑的部分推导规则
  1. 第一条公理表示如果xx之前指向某个值，把其地址对应的内容改为vv后，xx将指向新的值vv；
  2. 第二条公理表示如果xx之前存储了值vv，用变量yy读取xx地址所对应的内容时，yy将会暂存vv的值。这条公理为我们区分值在寄存器和堆中的不同描述：由于yy只是将值vv用作暂存，不会被分配地址空间，也就不会对堆产生更改，因此用y==xy==x表示，该公理假设xx不出现在表达式vv中；
  3. 第三条公理表示如果开始时没有堆，执行分配操作后就会产生大小为1的堆；
  4. 反之，第四条公理表示如果开始时是大小为1的堆，那么执行释放操作后将以空堆作为结束。

从某种意义上，小公理涵盖了它们所描述语句的关键信息。直观来讲，这些简单的语句每次只更新或访问一个内存单元，那么仅描述这个单元格发生什么就足够了，以此可以运用就地推理的策略对程序状态进行验证，即仅在上一个状态的基础上作更新。但又因为小公理过于简单，所以它暂时不能基于系统全局的状态进行推理。

框架规则(Frame Rule) 则为分离逻辑提供了从局部推导到全局推导的逻辑上的帮助。它允许我们将推理从一个拓展到多个存储单元，因此，仅作用于一个单元的小公理便不会再是一种限制，反而成为了一种简洁直观的描述。