A Logical Analysis of Framing for Specifications with Pure Method Calls

摘要: For specifying and reasoning about object-based programs it is often attractive for contracts to be expressed using calls pure methods. It useful methods have contracts, including read effects support local based on frame conditions. This leads puzzles such as the use of a method in its own contract. These ideas been explored connection with verification tools axiomatic semantics, guided by need avoid logical inconsistency, focusing encodings that cater first order automated provers. paper adds region logic, first-order program logic features frame-based proof rule linking clients modules achieve end-to-end correctness modular reasoning. Soundness proved respect conventional operational semantics extensional (i.e., relational) interpretation effects.