Regional Logic for Local Reasoning about Global Invariants

Shared mutable objects pose grave challenges in reasoning, especially for data abstraction and modularity. This paper presents a novel logic for erroravoiding partial correctness of programs featuring shared mutable objects. Using a first order assertion language, the logic provides heap-local reasoning about mutation and separation, via ghost fields and variables of type ‘region’ (finite sets of object references). A new form of modifies clause specifies write, read, and allocation effects using region expressions; this supports effect masking and a frame rule that allows a command to read state on which the framed predicate depends. Soundness is proved using a standard program semantics. The logic facilitates heap-local reasoning about object invariants: disciplines such as ownership are expressible but not hard-wired in the logic.

• Type: Conference
• Year: 2008
• Where: ECOOP
• Authors: Anindya Banerjee, David A. Naumann, Stan Rosenberg
• Keywords: ECOOP 2008, Heap-local Reasoning, Logic, Mutable Objects, Programming Languages