一句话：提出 Frame Logic，扩展一阶逻辑与递归定义，用支持集实现 frame reasoning，并用于堆程序局部规范。
Frame Logic (FL) 旨在解决底层模型或堆发生变化时，如何刻画公式意义所依赖的精确支持集并进行 frame reasoning 的问题。它扩展一阶逻辑与递归定义，引入 Sp(·) 构造来捕获公式的隐式支持，即其真值依赖的全域子集。基于支持，作者给出证明规则，使模型变化下的 frame 推理更优雅。文中还展示 FL 能表达多种数据结构，并给出从分离逻辑精确片段到 FL 的翻译；随后设计基于 FL 的程序逻辑，用于动态更新堆的程序，支持局部规范和 frame reasoning，包含局部化证明规则及推导最弱最紧前置条件的规则。
We propose a novel logic, Frame Logic (FL), that extends first-order logic and recursive definitions with a construct Sp (·) that captures the implicit supports of formulas—the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in frame logic.
@article{paperbot2134,
title = {A First-order Logic with Frames},
author = {Adithya Murali and Lucas Peña and Christof Löding and P. Madhusudan},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {45},
number = {2},
year = {2023},
doi = {10.1145/3583057}
}