A Logical Analysis of Framing for Specifications with Pure Method Calls
A Logical Analysis of Framing for Specifications with Pure Method Calls
复制标题
纯方法调用规范框架的逻辑分析
DOI：
10.1145/3174801
复制
发表时间：
2018
影响因子：
1.3
通讯作者：
Nikouei, Mohammad
中科院分区：
文献类型：
--
作者：
Banerjee, Anindya;Naumann, David A.;Nikouei, Mohammad
对于基于对象的程序的指定和推理，使用对纯方法的调用来表达契约通常很有吸引力。对于纯方法来说，具有契约（包括读取效果）以支持基于帧条件的本地推理非常有用。这导致了诸如在自己的合约中使用纯方法之类的难题。这些想法已经与基于公理语义的验证工具结合起来进行了探索，以避免逻辑不一致的需要为指导，并专注于满足一阶自动证明者的编码。本文为区域逻辑添加了纯方法和读取效果，区域逻辑是一种一阶程序逻辑，具有基于框架的局部推理，并为端到端正确性提供模块化推理原理。模块化推理体现在用于将模块的方法实现与依赖于方法契约的客户端链接起来的证明规则中。可靠性是根据传统的操作语义来证明的，并使用阅读效果的外延（即关系）解释。通过对示例进行机器检查验证，证明了基于 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.
登录
查看更多内容
影响因子：
3.6
作者：
Alexander J. Summers;S. Drossopoulou
通讯作者：
S. Drossopoulou
动态框架：支持无限制的框架、依赖和共享
DOI：
--
发表时间：
2006
期刊：
World Congress on Formal Methods
影响因子：
--
作者：
Ioannis T. Kassios
通讯作者：
Ioannis T. Kassios
关于接口规范中方法调用的推理
DOI：
10.5381/jot.2006.5.5.a3
发表时间：
2006
期刊：
J. Object Technol.
影响因子：
--
作者：
Ádám Darvas;Peter Müller
通讯作者：
Peter Müller
DOI：
10.1145/1111037.1111046
发表时间：
2006-01
期刊：
--
影响因子：
--
作者：
Torben Amtoft;Sruthi Bandhakavi;A. Banerjee
通讯作者：
Torben Amtoft;Sruthi Bandhakavi;A. Banerjee
影响因子：
--
作者：
Benton, Nick;Hofmann, Martin;Nigam, Vivek
通讯作者：
Nigam, Vivek