基于分离逻辑的规约

霍尔逻辑处理只涉及栈上局部标量变量（例如 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 年前后提出，正面回应这两个困难： 让断言默认只谈“一块”内存，并把“互不重叠”融入逻辑连接词本身，从而减轻显式描述的负担。

分离逻辑不是替换霍尔逻辑，而是扩展它：三元组 的形态不变， 变化发生在程序状态的模型与断言语言上。

store 对应 C 的局部变量，可以理解为栈；heap 对应动态分配的内存，可以理解为堆。 注意 heap 是部分函数：一个 heap 可以只含两三个地址——这为“断言只描述一小块内存”预留了空间。

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

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

满足关系写作 ，表示“状态 满足断言 ”。 变量间的算术断言（如 ）只依赖 store，语义与霍尔逻辑一致；逻辑常量与连接词逐点提升到状态 上；连同三个新构造，语义如下。

注意 的语义是“恰好”：堆里有且只有 这一个位置。 要表达“堆里至少有 这一位置”，应写 。 这个看似严苛的设计正是局部性的来源：每个 都精确刻画一个内存位置， 再把互不重叠的刻画组合起来。

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

逐行验证一遍：

• 第一行， 要求整个堆恰好是 起的两个单元，A 的堆有四个单元，故不成立；
• 第二行， 对任何堆都成立，于是 把“恰好”放松为“至少”——只要能拆出 起的两个单元、余下归 即可，A、B 都满足；
• 第三行，A 的堆恰能拆分为互不相交的两块，各自满足一个合取项，而 B 的堆无法拆出两块不相交的 ；
• 第四行则相反， 要求两个合取项在同一个堆上成立，这恰恰断定了 ；
• 第五行，两个合取项都只要求“至少有自己那两个单元”：A 中两块各自可拆出，B 中同一块被两个合取项共用，故两者都成立——它是第三、四行的共同弱化，不再区分 、 是否别名。

换言之， 内建了“互不重叠”，而 内建了“同一块”。 一个乍看惊人的推论： 是可满足的（取 ，任何非空堆都满足 ）。 正如 O’Hearn 所说：“理解分离逻辑断言，永远要局部地想（think locally）。”

分离逻辑不仅能够让我们用具有局部性的断言刻画堆的性质，它的推理规则也能让证明本身受益于局部性。 先看堆操作语句的公理。在数学记号中，我们采用极简指令集： 写入地址 （对应 C 的 *e = f*e = f）， 分配连续 个单元并初始化（对应 mallocmalloc）， 释放地址 （对应 freefree）。 它们的公理具有非常好的局部性，故而也称为小公理（Small Axioms）：

（allocation 的附加条件： 不在 中自由出现。） 每条公理的前置条件只刻画被触碰的那几单元内存：写入一个单元，就只谈那一单元；释放后它从堆中消失，剩下 。 这样的小公理之所以够用，是因为有分离逻辑中最重要的一条规则在背后作为支撑：

解读：若 在满足 的“小”状态上正确运行，那么它在“ 外加一块不相交内存 ”的任何“大”状态上同样正确，且 原封不动。 “什么没有变”从此不必写入每条规约——需要时用框架规则一步引入。 这就是局部推理（Local Reasoning）：规约只描述程序真正触碰的内存（称为它的足迹，footprint），其余交给框架规则。

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

保证根节点与左右子树两两不相交——“节点互不共享、无环”不再需要额外公理，而是定义的直接后果。 整条规约随之收缩为：

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

上一节“ 的子树可能被改动”的疑难就此消失：它在框架 里，规则保证它纹丝不动。 三条小公理加一条框架规则，替代了繁琐的框架公理。

还有一点值得说明。分离逻辑对三元组的解读比部分正确性更强：

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

结论是不成立的：向 写入 之后， 中仍存储着 。 注意到，这里的问题在于 本就不该成立： 没有刻画 那一单元内存，写入就可能出错。 于是分离逻辑强制要求：前置条件必须刻画程序触碰的所有内存。 这带来的好处是：凡通过分离逻辑验证的程序，自动排除野指针写入、悬垂指针解引用、双重释放等问题——内存安全是程序验证的自然结果。

把小公理、框架规则与霍尔逻辑原有的规则串联起来，可以逐句推演一段真实操纵指针的程序。 下面的程序分配两个双单元块、让它们相互引用，然后释放其一、再穿过指针读取。目标规约是：

推演采用证明大纲（Proof Outline）的记号：在语句之间插入断言，每一步由一条公理或规则支撑 （ 表示 在赋值前的旧值，隐式存在量化）。