分离逻辑

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

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

验证；若另有 $y\mapsto m$，应用框架规则理路框架规则Frame rule若命令不修改额外资源，则可把该资源同时附加到前置和后置断言。可在前后条件中同时保留它。

要隔离“值矛盾”和“资源重叠”，更好的对照是 $(x\mapsto 1)\wedge (x\mapsto 1)$ 与 $(x\mapsto 1)\ast (x\mapsto 1)$。前者在单元堆上成立，后者即使两边值相同也不可满足，因为同一地址不能分给两个不交子堆。原来的 $(x\mapsto 1)\ast (x\mapsto 2)$ 当然也不可满足。

变量侧条件有独立作用：若 $R$ 为 $y\mapsto 2$，命令只是把栈变量 $y$ 改成另一个地址，即使没有写入原来的堆单元，$R$ 也未必仍成立。反之，链表断言 $(x\mapsto y)\ast (y\mapsto 0)$ 可以满足：第一个单元的值指向第二个单元，但两个被拥有的地址仍不同。“数据有引用关系”不等于“堆域重叠”。

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

它广泛用于内存安全、指针程序、并发算法与程序验证工具；分离逻辑自动化理路分离逻辑自动化Separation logic automation以 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 与生命周期静态限制程序，两者可以互相验证，却不是同一套规则或术语替换。