分离逻辑（Separation Logic）

分离逻辑是一种为操纵指针与堆内存的程序提供严格推理能力的形式化逻辑，它在霍尔逻辑的断言语言中加入了描述内存布局的新算子，使得对链表、树等动态数据结构的验证变得可行且模块化。

概述

分离逻辑由约翰·雷诺兹（John Reynolds）、彼得·奥赫恩（Peter O'Hearn）等人在二十世纪末至二十一世纪初提出。传统霍尔逻辑在处理别名问题时非常笨重，因为两个指针可能指向同一块内存，而分离逻辑通过显式表达内存的分割优雅地解决了这一难题。

核心原理

• 分离合取：断言把堆分成两个不相交的部分，各自满足一个子断言，从而表达内存区域互不重叠。
• 指向断言：描述某个地址存放某个值，是刻画堆内容的基本单元。
• 框架规则：这是模块化推理的关键，允许在局部证明基础上安全地附加与之无关的内存部分。
• 局部推理：只需关注程序实际访问的那部分内存，无需描述整个堆状态。

应用场景

分离逻辑广泛用于验证操作系统内核、指针密集的库、并发数据结构等对内存安全要求极高的软件。它是多个大型验证项目的理论基础，也催生了并发分离逻辑用于推理共享内存并发程序。工业界的一些内存安全静态分析工具也借鉴了它的思想。

常见问题

问：分离逻辑相比霍尔逻辑最大的优势是什么？答：它能通过分离合取显式表达不同内存区域互不重叠，从根本上化解指针别名带来的推理困难，并借助框架规则实现真正的局部化与模块化证明。

问：框架规则为什么重要？答：框架规则允许在只考虑局部内存的证明外，自动保留程序未触碰的其余堆内存不变，使得证明可以复用和组合，这正是大规模验证得以扩展的核心。