TY - GEN
T1 - Regional logic for local reasoning about global invariants
AU - Banerjee, Anindya
AU - Naumann, David A.
AU - Rosenberg, Stan
PY - 2008
Y1 - 2008
N2 - Shared mutable objects pose grave challenges in reasoning, especially for data abstraction and modularity. This paper presents a novel logic for error-avoiding 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.
AB - Shared mutable objects pose grave challenges in reasoning, especially for data abstraction and modularity. This paper presents a novel logic for error-avoiding 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.
UR - http://www.scopus.com/inward/record.url?scp=49049086746&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=49049086746&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-70592-5_17
DO - 10.1007/978-3-540-70592-5_17
M3 - Conference contribution
AN - SCOPUS:49049086746
SN - 3540705910
SN - 9783540705918
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 387
EP - 411
BT - ECOOP 2008 - Object-Oriented Programming - 22nd European Conference, Proceedings
T2 - 22nd European Conference on Object-Oriented Programming, ECOOP 2008
Y2 - 7 July 2008 through 11 July 2008
ER -