FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
A syntactic model of mutation and aliasing

Authors: Paola Giannini, Marco Servetto and Elena Zucca

Paper Information

Title:A syntactic model of mutation and aliasing
Authors:Paola Giannini, Marco Servetto and Elena Zucca
Proceedings:DCM DCM Pre-proceedingsd
Editor: Sandra Alves
Keywords:imperative calculi, sharing, syntactic models
Abstract:

ABSTRACT. Traditionally, semantic models of imperative languages use an auxiliary structure which mimics memory. In this way, ownerships 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 is more abstract, and directly represents at the syntactic level constraints on aliasing, allowing simpler reasoning about related properties. We illustrate this advantage by expressing in the calculus the "capsule" property, characterizing an isolated portion of memory, which cannot be reached through external references. Capsules can be safely moved to another location in the memory, without introducing sharing. We state that the syntactic model can be encoded in the conventional one, hence efficiently implemented, and outline the proof that the dynamic semantics are equivalent.

Pages:9
Talk:Jul 08 11:00 (Session 38C)
Paper: