Unbounded Allocation in Bounded Heaps - Fundamentals of Software Engineering
Conference Papers Year : 2013

Unbounded Allocation in Bounded Heaps

Abstract

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, assuming 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.
Fichier principal
Vignette du fichier
978-3-642-40213-5_1_Chapter.pdf (325.08 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

hal-01514664 , version 1 (26-04-2017)

Licence

Identifiers

Cite

Jurriaan Rot, Frank De Boer, Marcello Bonsangue. Unbounded Allocation in Bounded Heaps. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. pp.1-16, ⟨10.1007/978-3-642-40213-5_1⟩. ⟨hal-01514664⟩
93 View
66 Download

Altmetric

Share

More