TY - JOUR
T1 - A logical analysis of framing for specifications with pure method calls
AU - Banerjee, A.
AU - Naumann, D. A.
AU - Nikouei, M.
N1 - Publisher Copyright:
© 2018 ACM.
PY - 2018
Y1 - 2018
N2 - 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.
AB - 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.
KW - Framing
KW - Local reasoning
KW - Pure methods
KW - Read effect
KW - Specifications
UR - http://www.scopus.com/inward/record.url?scp=85056840127&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85056840127&partnerID=8YFLogxK
U2 - 10.1145/3174801
DO - 10.1145/3174801
M3 - Article
AN - SCOPUS:85056840127
SN - 0164-0925
VL - 40
JO - ACM Transactions on Programming Languages and Systems
JF - ACM Transactions on Programming Languages and Systems
IS - 2
M1 - 6
ER -