We propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using 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 FL.
翻译:我们提出了一个新颖的逻辑,称为框架逻辑(FL),它利用一个构思 Sp (.) 来扩展第一阶逻辑(带有递归定义),它能捕捉公式的隐含支持 -- -- 其含义所依赖的宇宙的精密子集。我们利用这种支持,制定证据规则,在基本模型发生变化时,为框架推理提供优雅的便利。我们通过捕捉若干数据结构来显示逻辑的表达方式,并展示从精确的分离逻辑碎片到逻辑框架的翻译。最后,我们设计了一个程序逻辑,根据框架逻辑进行推理,其程序能动态地更新堆积,便于本地的规格和框架推理。这个程序逻辑包括本地化的证明规则以及从FL中得出最薄弱的最严格先决条件的规则。