A Syntactic Model of Mutation and Aliasing

Paola Giannini
(DiSIT, Universita' del Piemonte Orientale)
Marco Servetto
(School of Engineering and Computer Science,Victoria University of Wellington)
Elena Zucca
(DIBRIS, Universita' di Genova)

Traditionally, semantic models of imperative languages use an auxiliary structure which mimics memory. In this way, ownership and other encapsulation properties need to be reconstructed from the graph structure of such global memory. We present an alternative "syntactic" model where memory is encoded as part of the program rather than as a separate resource. This means that execution can be modelled by just rewriting source code terms, as in semantic models for functional programs. Formally, this is achieved by the block construct, introducing local variable declarations, which play the role of memory when their initializing expressions have been evaluated. In this way, we obtain a language semantics which directly represents at the syntactic level constraints on aliasing, allowing simpler reasoning about related properties. To illustrate this advantage, we consider the issue, widely studied in the literature, of characterizing an isolated portion of memory, which cannot be reached through external references. In the syntactic model, closed block values, called "capsules", provide a simple representation of isolated portions of memory, and capsules can be safely moved to another location in the memory, without introducing sharing, by means of "affine' variables. We prove that the syntactic model can be encoded in the conventional one, hence efficiently implemented.

In Michele Pagani and Sandra Alves: Proceedings Twelfth Workshop on Developments in Computational Models and Ninth Workshop on Intersection Types and Related Systems (DCM 2018 and ITRS 2018 ), Oxford, UK, 8th July 2018, Electronic Proceedings in Theoretical Computer Science 293, pp. 39–55.
Published: 23rd April 2019.

ArXived at: http://dx.doi.org/10.4204/EPTCS.293.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org