Sciweavers

ECOOP
2008
Springer

Regional Logic for Local Reasoning about Global Invariants

13 years 4 months ago
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.
Anindya Banerjee, David A. Naumann, Stan Rosenberg
Added 09 Nov 2010
Updated 09 Nov 2010
Type Conference
Year 2008
Where ECOOP
Authors Anindya Banerjee, David A. Naumann, Stan Rosenberg
Comments (0)