基于分离逻辑的规约

如果程序只涉及栈上局部标量变量（例如 intint），用霍尔逻辑就很容易处理：断言是关于变量取值的一阶公式，借助赋值公理和循环不变式就能完成大多数证明。但验证 C 程序时，难点主要在于堆与指针，尤其是链表、树、图这些共享可变数据结构（Shared Mutable Data Structures），而非栈上的标量。本节先通过一个例子说明：一旦程序开始操作堆，经典霍尔逻辑中的规约就会迅速膨胀，证明也随之复杂起来；随后介绍分离逻辑（Separation Logic）如何用一个新的逻辑连接词解决这个问题。本节使用形式化数学记号，暂不涉及 C* 的具体规约语法。

考虑下面的 C 函数，它递归地释放一棵二叉树的全部节点：

#include <stdlib.h>
struct tree {
  struct tree *l;
  struct tree *r;
};
void free_tree(struct tree *p)
{
  if (p != NULL) {
    struct tree *i = p->l;
    struct tree *j = p->r;
    free_tree(i);
    free_tree(j);
    free(p);
  }
}

#include <stdlib.h>
struct tree {
  struct tree *l;
  struct tree *r;
};
void free_tree(struct tree *p)
{
  if (p != NULL) {
    struct tree *i = p->l;
    struct tree *j = p->r;
    free_tree(i);
    free_tree(j);
    free(p);
  }
}

我们想说明它是正确的：调用结束后，树上的节点都被释放了。一条看似合理的霍尔式规约如下：

其中 表示 指向一棵合法的二叉树（节点互不共享、无环）； 表示从 出发可以到达节点 ； 表示 处于已分配状态； 是任取的辅助变量。整条规约的含义是：“若 是树 上的任一节点，则 free_tree(p)free_tree(p) 执行后， 不再处于已分配状态。”

沿着递归结构验证函数体时，我们先考虑第一次递归调用 free_tree(i)free_tree(i)。将规约中的参数实例化为 ，得到：

后置条件只说明“ 子树上的节点被释放了”，完全没有提及其余内存。特别地，它没有排除 free_tree(i)free_tree(i) 同时改写子树 的可能性。单看这条规约，调用返回后， 可能已经不再是一棵树。这样就无法建立第二次调用 free_tree(j)free_tree(j) 的前置条件，证明也无法继续。只要规约允许这种行为，证明就必须考虑这种可能。

一种补救办法是添加框架公理（Frame Axioms），把“什么没有变”也写进前置条件和后置条件。例如：

仅仅为了说明“树外的任意节点 及其字段都没有改变，未分配的 仍未分配”，规约就引入了许多与函数本身无关的元变量 、、，其中 表示任意字段（例如 ll 和 rr）。程序每增加一种可能引用的资源，每条函数规约就要相应增加一组框架公理。随着程序规模增大，这样的规约难以维持，也完全不符合程序员的直觉：编写 free_treefree_tree 时，程序员清楚地知道，函数只操作了这一棵树。

分离逻辑由 Reynolds、O’Hearn 等人在 2000 年前后提出，用来应对这两个困难：让断言默认只描述“一块”内存，并将“互不重叠”纳入逻辑连接词的含义，从而减少需要显式写出的条件。

分离逻辑扩展了霍尔逻辑，并未取代它：三元组 的形式不变，改变的是程序状态模型和断言语言。

存储映射对应 C 的局部变量，可以理解为栈；堆对应动态分配的内存。注意堆是一个部分函数，可以只包含两三个地址，因此断言也就可以只描述一小块内存。

断言语言在一阶逻辑之上增加三个构造，统称空间断言（Spatial Assertions）：

• ：空堆断言，即我们在第一个 C* 程序中看到的 empemp；
• ：指向谓词（Points-to），地址 处恰好存储着值 ，即我们在第一个 C* 程序中看到的 data_at data_at （地址 处恰好存储着值 ）；
• ：分离合取（Separating Conjunction），堆可拆分为互不相交的两块，分别满足 与 ，即我们在第一个 C* 程序中看到的 **** 连接词。

满足关系记为 ，表示“状态 满足断言 ”。变量间的算术断言（如 ）只依赖存储映射，语义与霍尔逻辑一致。逻辑常量与连接词逐点提升到状态 上，再加上三个新构造，就得到了下面的语义。

注意 中“恰好”的含义：堆中有且只有 这一个位置。要表达“堆中至少有 这一位置”，应写 。这个看似严格的设计正是局部性的来源：每个 都精确刻画一个内存位置， 再将这些断言组合起来，要求它们描述的内存互不重叠。

下图是一个经典例子：三个内存位置相互指向。断言中的每个 恰好描述一个位置， 将三个各含一个内存位置的小堆组合成整个堆。

我们逐行验证这些断言：

• 第一行， 要求整个堆恰好由从 开始的两个单元组成，A 的堆有四个单元，故不成立；
• 第二行， 对任何堆都成立，于是 把“恰好”放松为“至少”——只要能拆出从 开始的两个单元，其余部分满足 即可，A、B 都满足；
• 第三行，A 的堆恰能拆分为互不相交的两块，各自满足一个合取项，而 B 的堆无法拆出两块不相交的 ；
• 第四行则相反， 要求两个合取项在同一个堆上成立，这也就要求 ；
• 第五行，两个合取项都只要求堆中至少包含各自描述的两个单元：A 中可以分别拆出这两块内存，B 中两个合取项描述的是同一块内存，所以该断言在两种状态下都成立。这是第三、四行的共同弱化，不再区分 、 是否互为别名。

换言之， 内建了“互不重叠”，而 内建了“同一块”。由此还有一个初看有些意外的推论： 是可满足的（取 ，任何非空堆都满足 ）。正如 O’Hearn 所说：“理解分离逻辑断言时，始终要从局部考虑。”

分离逻辑的局部性不仅体现在描述堆的断言中，也体现在推理规则中，因此证明本身也能利用这种局部性。先看堆操作语句的公理。在数学记号中，我们采用极简指令集： 写入地址 （对应 C 的 *e = f*e = f）， 分配 个连续单元并将其初始化（对应 mallocmalloc）， 释放地址 （对应 freefree）。这些操作的公理具有很好的局部性，因此也称为小公理（Small Axioms）：

（allocation 的附加条件： 不在 中自由出现。）每条公理的前置条件只刻画操作涉及的几个内存单元：写入一个单元，就只描述这一个单元；释放一个单元后，它从堆中消失，得到 。这些小公理之所以足以支持推理，是因为分离逻辑还有一条最重要的规则：

这条规则可以这样理解：若 在满足 的“小”状态上正确运行，我们就可以在 描述的内存之外增加一块不相交、满足 的内存。在这样得到的任何“大”状态上，程序仍能正确运行，且 所描述的内存保持不变。“什么没有变”从此不必写入每条规约，需要时用框架规则一步引入即可。这就是局部推理（Local Reasoning）：规约只描述程序实际访问的内存（称为它的足迹，footprint），其余内存由框架规则处理。

回到开头的 free_treefree_tree 例子。首先， 谓词本身可以用空间断言归纳定义：

保证根节点与左右子树两两不相交，因此“节点互不共享、无环”可以直接由定义得出，无须额外公理。整条规约也相应简化为：

后置条件 表示：函数返回时，前置条件刻画的那块内存（整棵树）已经全部归还。注意规约完全没有提树以外的空间。验证递归调用时，按 的定义把堆拆分为三块 ；对 free_tree(i)free_tree(i) 应用规约（作用于 这一块），框架规则保证其余两块保持不变：

此前“ 子树可能被改动”的问题也就解决了：它属于框架 ，框架规则保证它保持不变。三条小公理加一条框架规则，替代了繁琐的框架公理。

这里还有一点需要说明：分离逻辑赋予三元组的含义比部分正确性更强。

这一语义加强了正确性要求，同时也是框架规则成立的条件。反过来说，如果允许出错的执行，那么 将是一条有效规约（它对结果状态毫无要求）；用框架规则加上 ：

这条结论无法成立，因为它声称向 写入 之后， 中仍存储着 。问题在于 原本就不应成立： 没有刻画 对应的内存单元，写入就可能出错。于是分离逻辑强制要求：前置条件必须刻画程序访问的所有内存。因此，凡是通过分离逻辑验证的程序，都能自动排除野指针写入、悬垂指针解引用、双重释放等问题，内存安全是程序验证的自然结果。

将小公理、框架规则与霍尔逻辑原有的规则结合起来，我们就可以逐句推演一段实际操作指针的程序。下面的程序分配两块各含两个单元的内存，让它们相互引用，然后释放其中一个单元，再通过指针读取。目标规约是：

推演采用证明大纲（Proof Outline）的记号：在语句之间插入断言，每一步都有一条公理或规则作为依据（ 表示 在赋值前的旧值，隐式地由存在量词约束）。