程序验证（6）- 分离逻辑

奋斗的小鸟

前言

本篇我们打算讲一些和这一系列主题相关性较低的内容——分离逻辑（Separation Logic）[1]。之所以如此设定，是因为后续验证算法的介绍，比如谓词抽象、路径抽象、反例制导抽象精化等等，都需要一些图示才能达到比较好的效果。而目前的文档编辑器似乎不支持使用\LaTeX的tikz包，或者其他矢量图绘制方式进行绘图。但笔者又不太喜欢使用非矢量图以及在线图床，所以正在寻找解决办法。接下来的几篇，可能都会是些题外话。
本篇比较全面地讲解了分离逻辑的基本知识，并使用了几个小例子，以及一个综合验证案例来演示分离逻辑的应用。本篇篇幅较长，但内容非常浅显易懂，希望读者仔细耐心阅读。另外，本篇不会介绍过多的理论内容，如分离逻辑推理的正确性和完备性的证明，以及分离逻辑的形式化数学基础部分交换夭半群（Partial Commutative Monoid，PCM）。
Frame问题

在前文中，我们介绍了霍尔逻辑。霍尔逻辑可以用于描述一般程序的验证，但是对于和内存状态相关的程序，比如说带有动态指针、复杂数据结构的程序，霍尔逻辑并不能很好地进行处理。其中最核心的也就是Frame问题（这个词不太好翻译）。Frame问题是说当验证问题涉及动态内存操作时，我们需要引入一些约束来描述内存的状态，即程序的操作改变了哪些内存区，而哪些内存区又没有被改变。我们用一个例子来解释这个问题。例如，我们想证明如下的霍尔三元组成立：
\{true\} \\\mathtt{*p = 1;} \\\mathtt{*q = 2;} \\\mathtt{x = *p + *q;} \\\{x = 3\}
我们使用最弱前置条件的计算规则，主要是赋值语句规则，来从后置条件往前，逐步进行证明：
\underline{\mathbf{\{*p + *q = 3\}}} \\\mathtt{x = *p + *q;} \\\{x = 3\}
这一步前置条件的计算没有什么问题。我们再继续往前计算。
\underline{\mathbf{\{*p + 2 = 3\}}} \\ \mathtt{*q = 2;} \\\{*p + *q = 3\} \\\mathtt{x = *p + *q;} \\\{x = 3\}
这一步也没有太大问题。我们继续往前计算。
\underline{\mathbf{\{1 + 2 = 3\} \quad \times }} \\ \mathtt{*p = 1;} \\\{*p + 2 = 3\} \\\mathtt{*q = 2;} \\\{*p + *q = 3\} \\\mathtt{x = *p + *q;} \\\{x = 3\}
这一步貌似成立，而且最弱前置条件1 + 2 = 3也可以简化为true，我们好像已经证明了霍尔三元组。但是这实际上是有问题的，因为两个指针可以指向同一个地址，这在C语言中是允许的。倘若指针p和q指向了同一个地址，那么*p和*q的值都会是2。这也就是说，我们的推理是不正确的（Unsound）。
为了在涉及指针操作时，仍然保证霍尔逻辑推理的正确性（Soundness）。我们需要加入额外的谓词来描述以下实事：我们在对p指向的内存区进行操作时，q指向的内存区不会发生改变，反过来也一样。我们将这个问题称为Frame问题，而把额外加入描述内存约束的谓词称之为Frame约束。
很多时候，我们在使用霍尔逻辑进行证明时，需要花费大量的精力来解决Frame问题。有时，花费在证明Frame相关的约束上的时间，甚至比证明目标本身更多，这造成了极大的资源浪费。我们亟需一套通用的方法来解决Frame问题。分离逻辑（Separation Loigc）就是在这样的背景下，总结出的一套解决方法，它是对一般霍尔逻辑的一种扩展。
分离逻辑运算符

分离逻辑的核心内容是引入了分离与（Separating Conjunction）运算，记为A * B。在介绍分离与的语义前，我们先介绍分离逻辑的语义模型。分离逻辑中假定有一个值函数（Store）s，将变量映射到它的值。例如，s(x) = 10意味着变量x = 10。在一般霍尔逻辑中，当提及一个变量x时，我们默认对x做取值处理，所以我们一般会忽略值函数，直接用x表示s(x)。但在分离逻辑中情况不同，因为分离逻辑需要单独考虑内存，所以对分离逻辑中的变量，不仅仅有取值处理，我们还可以将它们视为内存中的地址。这就像C语言中，变量x可以是一个整型值，也可以作为一个指针。所以，在分离逻辑中，除了值函数s，还有一个堆函数（Heap）h，将地址映射到堆中的值。例如h(x) = 10意味着在内存地址x处的存储的值为10，可以理解为C语言代码*x == 10。如果两个堆函数h_1和h_2的定义域没有公共的地址，我们说它们不相交（Disjoint）。我们也可以把堆函数理解成实际的内存堆，不相交意味着两个堆没有公共内存地址。我们也可以把一个堆划分（Separate）为不相交的两个子堆。
在分离逻辑中，我们还会引入一个谓词\mathbf{emp}，表示堆是空的（Empty）。此外，还会有个一指向运算符\mapsto，比如，x \mapsto y表示x的值对应的地址，在堆上对应的值等于y的值，即h(s(x)) = s(y)，可以简写为h(x) = y。指向运算符可以直观地理解成C语言的指针取值运算，如x \mapsto y可以大概理解为*x == y。在分离逻辑中，我们会试图证明s, h \models P，表示在给定的s, h下，分离逻辑公式P是有效的。通常，我们会省略s, h \models，简记为公式P。
接下来介绍分离与的语义。我们以分离逻辑公式s, h \models x \mapsto y * y \mapsto x为例来说明。该公式表达的是，我们可以把堆h划分为不相交的两部分h_1和h_2，有s, h_1 \models x \mapsto y且s, h_2 \models y \mapsto x。这个公式实际上要求x和y的值不同，且x指向的地址的值为y，y指向的地址的值为x。
如下所示的s, h满足分离逻辑公式x \mapsto y * y \mapsto x。其中，val表示值，adr表示地址。
s: x = 10    h:  val:    42       10      
   y = 42        adr: 09 10 11 .. 42 43   
原因很简单，我们对堆h进行如下的分割，将其分割为不相交的h_1和h_2，显然有s, h_1 \models x \mapsto y且s, h_2 \models y \mapsto x。
                               |
                      h1:      | h2:        
s: x = 10    h:  val:    42    |    10      
   y = 42        adr: 09 10 11 | .. 42 43   
                               |            
分离与（*）可以看作是一种新的与运算。同普通的逻辑与（\wedge）相比，分离与不仅要求运算符两边的公式都成立，还要求它们在原堆划分出的两个不相交子堆中分别成立。这一点是非常重要的，正是因为要求子堆不相交，我们在进行分离逻辑推理时，不再需要显示地添加Frame约束。我们可以使用几个例子来展示分离与和逻辑与之间的差别。对于逻辑与，显然有公式P \wedge P = P成立。但是对于分离与，P * P = P不一定成立。比如我们让P为x \mapsto v，那么公式x \mapsto v * x \mapsto v是不成立的。因为我们无法将一个堆分割为不相交的两部分，使得两部分都有x对应的地址。所以x \mapsto v * x \mapsto v等值于false。
有了新的与运算，那么对应也会有新的其他运算，典型的就是分离蕴含（Separating Implication），记为A \mathrel{-*} B。类比逻辑蕴含和逻辑与，我们可以从P \wedge (P \Rightarrow Q)得到Q。在分离逻辑中，我们也可以从P * (P \mathrel{-*} Q)得到Q。分离蕴含使用得不太多，我们在此暂不多做介绍，有兴趣的读者可以自行了解。
分离逻辑描述能力

分离逻辑对指针表示的递归数据结构的表达非常友好。我们用几个例子来说明。如下所示是一个链表（Linked List）。假定我们已经有了一个谓词list(x, y)用来表示从结点x到结点y形成了一个无环的链。

事实上，我们可以以大致如此的形式（非严格）使用分离逻辑递归定义谓词list(x, y)。
list(x,y) \triangleq x \mapsto z * list(z, y)

x     z           y     0
o --> o --> o --> o --> o
例如，我们可以使用分离逻辑来描述，t是链表中的一个结点。在如下的描述中，分离逻辑已经帮我们处理好了各个指针都指向不同内存区这一约束。我们无需添加额外的约束来说明。
list(x, t) * t \mapsto y * list(y, 0)
x           t     y           0
o --> o --> o --> o --> o --> o
再比如，我们可以用分离逻辑组成的霍尔三元组来描述链表的插入操作。假定我们操作的是一个不带数据域的链表，即执行*x = y后有x \mapsto y。以下的霍尔三元组描述了对一个给定头指针为x的链表的插入操作。需要注意其中我们使用y \mapsto -（通配符-）表示我们不关心指针y指向的内存区的值。
\{ x \mapsto z * list(z, 0) * y \mapsto - \} \\\mathtt{*x = y; *y = z;} \\\{ x \mapsto y * list(z, 0) * y \mapsto z \}
x     z           0     y     
o --> o --> o --> o     o -->

            |
            V

x     y     z           0
o --> o --> o --> o --> o
分离逻辑推理规则

首先，分离逻辑是对基于谓词逻辑的一般霍尔逻辑的扩展，所以分离逻辑包含一般霍尔逻辑的全部推理规则，如空语句规则，赋值语句规则，顺序语句规则，条件语句规则，循环语句规则，增强弱化规则等等。此外，因为分离逻辑需要描述动态内存，所以我们需要引入这方面对应的规则。
内存申请规则（Allocation）

这条规则非常自然。在空堆上为指针x申请内存成功后，x将指向一片值未定的内存区（用通配符-表示）。这里我们不考虑申请内存失败的情况。
\mathtt{Alloc}\ \frac{\ }{\{\mathbf{emp}\} \mathtt{x = alloc()} \{x \mapsto -\}}
内存释放规则（De-Allocation）

这条规则也同样简单。若仅存在一个指向堆上某片内存区的指针x，在释放x后，堆变为空。
\mathtt{Deloc}\ \frac{\ }{\{x \mapsto -\} \mathtt{free(x)} \{\mathbf{emp}\}}
指针写入规则（Pointer Write/Store）

指针写入规则同样简单易懂。若指针x指向某片内存区，那么将x指向的值赋值为v后，x指向的值将为v。
\mathtt{Store}\ \frac{\ }{\{x \mapsto -\} \mathtt{*x = v} \{x \mapsto v\}}
指针读取规则（Pointer Read/Load）

指针读取规则也很简单。若x指向的值将为v，那么将y赋值为x指向的值后，y的值将变为v，同时x指向的值不变。
\mathtt{Load}\ \frac{\ }{\{x \mapsto v\} \mathtt{y = *x} \{y = v \wedge x \mapsto v\}}
以上四条规则都是无前提的，相当于为了处理动态内存而引入的公理（Axioms）。而分离逻辑最具特色，也是最核心的规则，是以下的Frame规则。
Frame规则

Frame规则是分离逻辑的核心规则。它说的是，如果霍尔三元组在一片小的堆内存区（Heaplet）上成立，那么我们可以把前置/后置条件分离与上其他公式，使得新的霍尔三元组在更大的内存区上成立。这一规则可能需要反复理解几遍，但实际上也是非常简单的。
\mathtt{Frame}\ \frac{\{P\} \mathtt{c} \{Q\}}{\{P \underline{* F}\} \mathtt{c} \{Q \underline{* F}\}} \ \mathrm{mod}(C) \cap \mathrm{fv}(F) = \emptyset
需要注意的是，Frame规则要求代码片段c不能修改（\mathrm{mod}(C)）分离与上的公式F中自由出现的变量（\mathrm{fv}(F)）。若缺少了这条限制，Frame规则将变得不正确。例如，我们分离与上的公式F为\forall x. x > v。很显然，变量v在F中自由出现，即v \in \mathrm{fv}(F)。假如在前置条件P中v = 0，但是代码片段c修改了变量v的值，使其变大为10。这样的话，F在前置/后置条件中的语义就会发生变化，即\forall x. x > 0变为\forall x. x > 10。从而导致F在后置条件中不一定成立。
小例子

我们使用一个小例子来演示分离逻辑推理规则的应用。如下的程序片段将指向内存区的两个不同指针变量x和y指向对方。我们使用带分离逻辑的霍尔三元组来描述这一功能。接下来我们来验证这段代码的功能正确性，即证明如下的霍尔三元组成立。
\{ x \mapsto - * y \mapsto -\} \\\mathtt{*x = y;} \\\mathtt{*y = x;} \\\{ x \mapsto y * y \mapsto x\}
应用规则证明过程如下：

• 应用指针写入规则可得：
  

\{ x \mapsto - \} \mathtt{*x = y} \{ x \mapsto y \}

• 应用Frame规则，分离与上公式\{ y \mapsto - \}，可得：
  

\{ x \mapsto - \underline{* y \mapsto - }\} \mathtt{*x = y} \{ x \mapsto y \underline{* y \mapsto - }\} \quad (2)

• 在应用指针写入规则可得：
  

\{ y \mapsto - \} \mathtt{*y = x} \{ y \mapsto x \}

• 再应用Frame规则，分离与上公式\{ x \mapsto y \}，可得：
  

\{ y \mapsto - \underline{* x \mapsto y} \} \mathtt{*y = x} \{ y \mapsto x \underline{* x \mapsto y} \} \quad (4)

• 应用顺序语句规则，将(2)和(4)两个霍尔三元组串起来。在进行这一步时，我们会应用额外的交换规则P * Q = Q * P进行谓词的位置调整。最后我们可以得到证明目标。
  

\{ x \mapsto - * y \mapsto - \} \mathtt{*x = y; *y = x} \{ x \mapsto y * y \mapsto x \}
从这个小例子可以看出，分离逻辑的推理规则也非常简洁，我们只需要在应用Frame规则时，选取合适的公式进行分离与操作即可。
验证案例

在这一小节中，我们将给出用分离逻辑验证一个释放销毁二叉树的函数的功能正确性的例子。我们会像之前分析验证案例一样，从属性描述到验证过程逐步进行。
案例程序

例子的代码如下，C语言实现的deletetree函数按后续遍历的方式，递归地释放销毁二叉树的左右子树，最后销毁当前访问的结点。
void deletetree(struct node *root)
{
  if (root != 0) {
    struct node *left = root->l, *right = root->r;
    deletetree(left);
    deletetree(right);
    free(root);
  }
}
证明目标

我们希望验证以上deletetree函数的功能正确性，还需要有对应的前置条件和后置条件。前置条件很简单，即要求函数的输入参数root是一棵二叉树的根结点。为了描述这一前置条件，我们使用一个辅助谓词tree(root)，来描述root是一颗二叉树的根结点。
tree(root) \triangleq \\ ite(root = 0, \mathbf{emp}, \exists x,y. root \mapsto (l: x, r: y) * tree(x) * tree(y))
其中，ite为一个数学函数，是if-then-else的缩写。tree(root)表达的意思是，如果root = 0，那么表示它是一个空指针，那我们直接要求堆为空，即返回谓词\mathbf{emp}。否则，root非空，我们要求它有左右子树x, y，且它们分别都是某颗二叉树的根结点。这里，我们使用分离与恰到好处地表示root, x, y指向的内存区不交叠，从而说明谓词tree(root)描述的是一颗二叉树，而非二叉图。
在谓词tree(root)的基础上，我们给出如下的霍尔三元组，来描述deletetree函数的功能正确性。该霍尔三元组描述了，输入一颗二叉树，执行函数销毁释放这颗二叉树，最后堆应该是空的。
\{tree(root)\} \mathtt{deletetree(root)} \{\mathbf{emp}\}
证明过程

接下来，我们应用分离逻辑推理规则来证明以上霍尔三元组成立。在证明的过程中，我们并不严格地按照推理规则来进行，而是按照自然演绎推理的方式，从前往后，一步一步给出推理结果。这一推理过程可以通过适当的转化，变成严格符合推理规则应用的证明过程。

• 首先展开前置条件中的谓词tree(root)：
  

ite(root = 0, \mathbf{emp}, \exists x,y. root \mapsto (l: x, r: y) * tree(x) * tree(y))

• 经过if (root != 0)语句。倘若root = 0，依据ite函数的语义，我们直接可以得到\mathbf{emp}。所以，我们还需考虑root \neq 0的情况。在这种情况下有：
  

\exists x,y. root \mapsto (l: x, r: y) * tree(x) * tree(y)

• 再经过*left=root->l, *right=root->r语句。我们做存在量词消去，并进行相应的变量替换，可得：
  

root \mapsto (l: left, r: right) * tree(left) * tree(right) \quad (3)

• 再分析经过deletetree(left)语句。这里我们可以对树的深度使用归纳法。对于归纳法的基本情况（Base Case），即树的深度为0的情况（root = 0），我们已经证明了霍尔三元组成立。而对于归纳法的归纳情况（Step Case），我们假定要证明的霍尔三元组对深度为k的子树根结点成立，从而证明霍尔三元组对深度为k + 1的父结点也成立。为证明归纳情况，我们首先对子树结点left使用归纳假设，即假定\{tree(left)\} \mathtt{deletetree(left)} \{\mathbf{emp}\}成立。接着，我们使用Frame规则，在归纳假设的前置/后置条件分离与上公式root \mapsto (l: left, r: right) * tree(right)，可以得到以下霍尔三元组成立：
  

\{tree(left) \underline{* root \mapsto (l: left, r: right) * tree(right)}\} \\\mathtt{deletetree(root)} \\\{\mathbf{emp} \underline{* root \mapsto (l: left, r: right) * tree(right)}\}

• 再将已经得到的式子(3)作为推理条件，通过以上霍尔三元组，我们可以推导出，经过deletetree(left)语句后，以下式子成立：
  

\mathbf{emp} * root \mapsto (l: left, r: right) * tree(right) \quad (5)

• 再分析经过deletetree(right)语句。我们再次使用归纳假设，如法炮制，假设\{tree(right)\} \mathtt{deletetree(right)} \{\mathbf{emp}\}成立。在使用Frame规则时，分离与上公式root \mapsto (l: left, r: right) * \mathbf{emp}，可得以下霍尔三元组成立：
  

\{tree(right) \underline{* root \mapsto (l: left, r: right) * \mathbf{emp}}\} \\\mathtt{deletetree(root)} \\\{\mathbf{emp} \underline{* root \mapsto (l: left, r: right) * \mathbf{emp}}\}

• 再将已经得到的式子(5)作为条件，通过以上霍尔三元组，我们可以推导出，经过deletetree(right)语句后，以下式子成立：
  

root \mapsto (l: left, r: right) * \mathbf{emp} * \mathbf{emp} \quad (7)

• 最后经过free(root)语句，依据指针释放规则我们直接有以下霍尔三元组成立：
  

\{root \mapsto (l: left, r: right)\} \mathtt{free(root)} \{\mathbf{emp}\}

• 再次使用Frame规则，在以上霍尔三元组中，前置/后置条件分别分离与上\mathbf{emp} * \mathbf{emp}，可得：
  

\{root \mapsto (l: left, r: right) \underline{* \mathbf{emp} * \mathbf{emp}}\} \\\mathtt{free(root)} \\ \{\mathbf{emp} \underline{* \mathbf{emp} * \mathbf{emp}}\}

• 将已经得到的式子(7)作为条件，通过以上霍尔三元组，我们可以推导出，经过ree(root)语句后，以下式子成立：
  

\mathbf{emp} * \mathbf{emp} * \mathbf{emp}

• 由于\mathbf{emp}是分离与操作的单位元，即A*\mathbf{emp}=A。因此以上式子等值于\mathbf{emp}。所以，我们证得了结论，原本的霍尔三元组成立。
  

小结

从本篇给出的验证例子中，我们发现分离逻辑对于具有验证复杂数据结构的动态内存程序似乎非常实用。事实上，在定理证明领域，分离逻辑的确使用得非常广泛。它在一定程度上解决了Frame问题，并且和递归数据结构以及递归函数都非常契合。但是，在自动化的程序验证领域，分离逻辑使用得非常少。这其中比较主要的原因是分离逻辑缺乏全自动的逻辑公式可满足性求解器（比如一阶逻辑理论的SMT求解器）。其次，自动化的程序验证主要针对低阶的安全属性，如数组越界，除0错误等等。而分离逻辑与高阶的功能属性比较契合，所以自动化的程序验证的分析对象不太需要使用分离逻辑来描述。
虽然如此，分离逻辑仍然魅力十足。它仅对霍尔逻辑进行了简单的扩展，就非常优雅地解决了Frame问题，并且实现了理论上的完备性。分离逻辑使得对复杂数据结构动态内存程序的验证变得更加简单。同时，分离逻辑在针对共享内存的并行程序的验证有着非常好的适性。我们可以使用如下的并行语句规则，来描述并行进程（Concurrent Process）的组合产生的影响。
\mathtt{Concurrency}\ \frac{\{P_1\} \mathtt{process1} \{Q_1\} \quad \{P_2\} \mathtt{process2} \{Q_2\}}{\{P_1 * P_2\} \mathtt{process1\ ||\ process2} \{Q_1 * Q_2\}}
在自动化求解方面，目前已经有了类似于SMT/SAT求解大赛（SMT-COMP，SAT-COMP）的分离逻辑求解大赛（SL-COMP），也涌现出了越来越多的分离逻辑求解器（SL Solver）。相信在不久的将来，随着分离逻辑求解器的发展，分离逻辑在自动化验证领域的应用也会越发广泛。
声明

注：题图截取自文章插图 O'Hearn P . Separation Logic[J]. Communications of the ACM, 2019, 62(2):86-95. （侵权删除）

专栏链接


参考

• ^O'Hearn P. Separation Logic[J]. Communications of the ACM, 2019, 62(2):86-95. https://dl.acm.org/doi/10.1145/3211968
  

原文地址：https://zhuanlan.zhihu.com/p/314605288