一句话：将纯方法与读效应引入区域逻辑，为模块化框架推理建立可靠证明规则并机器检验示例。
本文研究面向对象程序规约中如何用纯方法调用表达契约，并处理由此产生的逻辑难题，例如纯方法出现在自身契约中。已有工作多基于公理语义验证工具，为避免不一致并适配一阶自动证明器而设计编码。作者将纯方法与读效应加入区域逻辑（region logic）：一种支持框架式局部推理的一阶程序逻辑，并给出一阶模块化推理原则。核心是一条链接模块方法实现与依赖方法契约的客户端的证明规则，从而支持端到端正确性。作者相对传统操作语义证明可靠性，读效应采用外延（关系）解释。最后通过机器检验的实例展示其对基于 SMT 求解器工具的适用性，并为模块化验证器实现链接及研究观测纯方法、封装提供基础。
For specifying and reasoning about object-based programs, it is often attractive for contracts to be expressed using calls to pure methods. It is useful for pure methods to have contracts, including read effects, to support local reasoning based on frame conditions. This leads to puzzles such as the use of a pure method in its own contract. These ideas have been explored in connection with verification tools based on axiomatic semantics, guided by the need to avoid logical inconsistency, and focusing on encodings that cater for first-order automated provers. This article adds pure methods and read effects to region logic, a first-order program logic that features frame-based local reasoning and provides modular reasoning principles for end-to-end correctness. Modular reasoning is embodied in a proof rule for linking a module’s method implementations with a client that relies on the method contracts. Soundness is proved with respect to conventional operational semantics and uses an extensional (i.e, relational) interpretation of read effects. Applicability to tools based on SMT solvers is demonstrated through machine-checked verification of examples. The developments in this article can guide the implementations of linking as used in modular verifiers and serve as a basis for studying observationally pure methods and encapsulation.
@article{paperbot323,
title = {A Logical Analysis of Framing for Specifications with Pure Method Calls},
author = {Anindya Banerjee and David A. Naumann and Mohammad Nikouei},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {40},
number = {2},
year = {2018},
doi = {10.1145/3174801}
}