形式陈述

框架规则的典型形式为

$$ \frac{\{P\}\ C\ \{Q\}}{\{P*R\}\ C\ \{Q*R\}}, $$$$\frac{\{P\}C\{Q\}}{\{P\ast R\}C\{Q\ast R\}},$$

前提是命令 $C$$C$ 不修改 $R$$R$ 中自由出现且受保护的资源；具体旁条件依语言与语义而定。规则表达局部性：对一小块堆的证明可在任意不相干堆环境中复用。

直觉

程序若完全不碰某块资源，就可以把这块资源“装框”在证明外侧，执行前后保持不变。

例子与边界

已证明对 $x\mapsto a$$x\mapsto a$ 的更新，可附加独立的 $y\mapsto b$$y\mapsto b$。若 $C$$C$ 可能通过别名修改 $y$$y$，旁条件失败，不能套规则。框架规则不是任意把普通合取 $R$$R$ 加到前后条件；关键是分离所有权和命令的足迹。

推论与应用

框架规则使库函数规格、链表片段和并发资源证明可组合，是分离逻辑自动化的中心规则。

参考资料

• 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。