A logical analysis of framing for specifications with pure method calls

A. Banerjee, D. A. Naumann, M. Nikouei

Research output: Contribution to journalArticlepeer-review

5 Scopus citations

Abstract

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.

Original languageEnglish
Article number6
JournalACM Transactions on Programming Languages and Systems
Volume40
Issue number2
DOIs
StatePublished - 2018

Keywords

  • Framing
  • Local reasoning
  • Pure methods
  • Read effect
  • Specifications

Fingerprint

Dive into the research topics of 'A logical analysis of framing for specifications with pure method calls'. Together they form a unique fingerprint.

Cite this