分离逻辑

普通逻辑的 $P\wedge Q$ 只说两件事同时成立，可能都谈论同一个内存单元；$P\ast Q$ 额外承诺它们拥有的堆片段互不重叠。这个所有权分割让函数规格只描述自己会触及的“小脚印”，调用者的其余堆可自动框住。别名不再靠全局猜测，而由能否把堆拆成不交部分显式控制。类比物理资源很有用，但现代分离逻辑也能用分数权限等方式表达共享，不必把所有权理解成永远独占。

断言 $(x\mapsto 1)\ast (y\mapsto 2)$ 表示 $x,y$ 是不同位置，堆可拆为两个单元。命令 [x]:=[x]+1 可由局部规格

验证；若另有 $y\mapsto m$，框架规则自动保留它。

边界是 $(x\mapsto 1)\ast (x\mapsto 2)$：普通合取可能只显得两个断言冲突，而分离合取明确要求两个不交单元，却又使用同一地址，因此不可满足。另一方面，链表节点可能通过指针连接，但拥有的堆单元仍可不交；“数据有引用关系”不等于“堆域重叠”。

分离逻辑扩展可变状态语义公理库可变状态语义Semantics of mutable state · Store semantics把位置到值的存储纳入配置并随求值更新的语义。与Hoare 三元组公理库Hoare 三元组Hoare triple断言若前置条件成立且程序终止，则后置条件成立的 {P}C{Q} 形式。，框架规则公理库框架规则Frame rule若命令不修改额外资源，则可把该资源同时附加到前置和后置断言。是其局部性原则的集中表达。递归谓词可描述链表、树和图的堆布局。

它广泛用于内存安全、指针程序、并发算法与程序验证工具；分离逻辑自动化公理库分离逻辑自动化Separation logic automation · Symbolic heap entailment · Bi-abduction以 symbolic heap、entailment、frame inference 与 bi-abduction 自动推理堆形状和局部内存契约。把 symbolic heap entailment、frame inference 与 bi-abduction 组织成可执行过程，尝试补出缺失的前置资源或调用后剩余的堆。逻辑给出资源语义和可靠规则，自动化只负责在受支持片段内搜索证明，不能把工具可解片段当成分离逻辑的全部表达力。

并发分离逻辑以资源不变量和权限控制线程间共享，支撑对数据竞争公理库数据竞争Data race · 数据竞态不同线程对同一内存位置的冲突访问既未按模型同步排序、也未通过原子操作协调的情形。自由和线性化点的模块化证明。这里的“所有权”是断言对资源份额的语义解释；语言所有权系统公理库所有权与借用Ownership and borrowing · Ownership type system · Borrow checking以所有者、移动、共享或独占借用及生命周期约束静态组织资源责任与别名访问。则以 move、loan 与生命周期静态限制程序，两者可以互相验证，却不是同一套规则或术语替换。