Paper Info
Title
It is pointless to point in bounded heaps
Abstract
We model a program with recursive procedure, local variables dynamic allocation and deallocation.We give an abstraction of the memory model that is precise and finitary.we show that adding pointer fields does not add any expressiveness if heaps are bounded. In this paper we introduce a new symbolic semantics for a class of recursive programs which feature dynamic creation and unbounded allocation of objects. We use a symbolic representation of the program state in terms of equations to model the semantics of a program as a pushdown system with a finite set of control states and a finite stack alphabet. Our main technical result is a rigorous proof of the equivalence between the concrete and the symbolic semantics.Adding pointer fields gives rise to a Turing complete language. However, under the assumption that the number of reachable objects in the visible heap is bounded in all the computations of a program with pointers, we show how to construct a program without pointers that simulates it. Consequently, in the context of bounded visible heaps, programs with pointers are no more expressive than programs without them.We conclude by extending programs with a dynamic deallocation statement, an operation that affects all aliases of a deallocated object. We show how to extend the concrete and the symbolic semantics so to retain the previous equivalence result.
Year
DOI
Venue
2015
10.1016/j.scico.2015.06.007
Science of Computer Programming
Keywords
Field
DocType
Heap structures,Pushdown system,Object-oriented program semantics
Pointer (computer programming),Programming language,Turing completeness,Computer science,Theoretical computer science,Heap (data structure),Equivalence (measure theory),Memory model,Recursion,Local variable,Bounded function
Journal
Volume
Issue
ISSN
112
P1
0167-6423
Citations 
PageRank 
References 
0
0.34
15
Authors
3
Name
Order
Citations
PageRank
Frank S. de Boer12013159.02
Marcello M. Bonsangue282466.34
Jurriaan Rot310418.53