形式陈述

分离逻辑在 Hoare 逻辑上加入分离合取 $P*Q$$P\ast Q$，表示堆可分成互不相交的两部分，分别满足 $P$$P$ 与 $Q$$Q$；空堆断言记为 $emp$$emp$，点指断言 $x\mapsto v$$x\mapsto v$ 描述单元所有权。语义通常基于部分交换幺半群或堆分割。局部推理要求命令只访问其拥有的资源。

直觉

传统断言描述整个内存，分离逻辑把内存拆成可独立拥有的片段，使程序只证明自己实际触碰的部分。

例子与边界

$x\mapsto1*y\mapsto2$$x\mapsto 1\ast y\mapsto 2$ 蕴含 $x$$x$ 与 $y$$y$ 指向不同单元。链表段可递归定义并用于验证插入和释放。若两个断言可能指向同一地址，就不能用 $*$$\ast$ 合并。并发分离逻辑还需权限、共享不变量等机制，基础堆语义并不自动解决数据竞争。

推论与应用

分离逻辑用于指针程序、内存安全、并发验证和自动静态分析，核心优势是模块化地扩展未修改堆。

参考资料

• John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, LICS 2002，pp. 55–74。
• Peter W. O'Hearn, Separation Logic, Communications of the ACM 62(2), 2019，pp. 86–95。