框架规则

框架规则把“这段代码没有碰其余内存”从每个证明中的重复劳动提升为一条通用推理原则。先在最小堆片段上验证命令，再把无关资源同时附加到前后条件；星号保证两部分互不重叠，局部性保证命令不会越界触碰框外。它像在照片上给不相关区域加一个固定边框，但前提是被验证的操作真的只作用于自己的区域。若存在隐藏别名，所谓“框外”其实可能被命令访问，规则便不能应用。

由

可推出

这里分离合取保证 $x\ne y$，所以对 $x$ 的写入不影响 $y$。

边界是把 $R$ 取成另一个关于同一位置的断言，或命令通过别名实际能访问 $R$ 的资源；此时前置条件可能不可满足，或局部性假设被破坏。命令若修改普通变量 z，也不能框入依赖 z 旧值的断言而不检查侧条件。

框架规则是分离逻辑公理库分离逻辑Separation logic以分离合取表达互不重叠资源并局部推理堆内存的程序逻辑。相对传统公理语义公理库公理语义Axiomatic semantics用逻辑断言和推理规则描述程序状态变换性质的语义方法。的关键增益：函数规格只需写触及的资源，调用点可自动保留更大上下文。它使链表库、内存分配器和模块化数据结构证明能够组合。

并发分离逻辑把同一思想扩展为线程资源拆分与共享不变量；分离逻辑自动化公理库分离逻辑自动化Separation logic automation · Symbolic heap entailment · Bi-abduction以 symbolic heap、entailment、frame inference 与 bi-abduction 自动推理堆形状和局部内存契约。则通过 entailment、frame inference 或 bi-abduction 推断调用前后未显式写出的剩余堆。语义框架规则说明何种资源可可靠保留，推断算法负责寻找具体的 frame；算法返回候选并不免除别名、局部性和侧条件检查。