Thumbnail
Access Restriction
Subscribed

Author Banerjee, Anindya ♦ Naumann, David A. ♦ Rosenberg, Stan
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2013
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Modularity ♦ Data abstraction ♦ Data invariants ♦ Heap separation ♦ Information hiding ♦ Resource protection
Abstract Dedicated to the memory of Stephen L. Bloom (1940--2010). Shared mutable objects pose grave challenges in reasoning, especially for information hiding and modularity. This article presents a novel technique for reasoning about error-avoiding partial correctness of programs featuring shared mutable objects, and investigates the technique by formalizing a logic. 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 frame condition specifies write, read, and allocation effects using region expressions; this supports 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, as shown here by examples. Part II of this article extends the logic with second-order framing which formalizes the hiding of data invariants.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2013-06-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 60
Issue Number 3
Page Count 56
Starting Page 1
Ending Page 56


Open content in new tab

   Open content in new tab
Source: ACM Digital Library