Regional logic for local reasoning about global invariants

Anindya Banerjee, David A. Naumann, Stan Rosenberg

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

59 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationECOOP 2008 - Object-Oriented Programming - 22nd European Conference, Proceedings
Pages387-411
Number of pages25
DOIs
StatePublished - 2008
Event22nd European Conference on Object-Oriented Programming, ECOOP 2008 - Paphos, Cyprus
Duration: 7 Jul 200811 Jul 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5142 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference22nd European Conference on Object-Oriented Programming, ECOOP 2008
Country/TerritoryCyprus
CityPaphos
Period7/07/0811/07/08

Fingerprint

Dive into the research topics of 'Regional logic for local reasoning about global invariants'. Together they form a unique fingerprint.

Cite this