文章基本信息

标题：A Syntactic Model of Mutation and Aliasing
本地全文：下载
作者：Paola Giannini ; Marco Servetto ; Elena Zucca 等
期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2019
卷号：293
页码：39-55
DOI：10.4204/EPTCS.293.4
语种：English
出版社：Open Publishing Association
摘要：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.