Aliasing control with view-based typestate

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

17 Citations (Scopus)


Tracking the state of an object (in the sense of how a File can be in an Open or Closed state) is difficult not just because of the problem of managing state transitions but also due to the complexity introduced by aliasing. Unchecked duplication of object references makes local reasoning impossible by allowing situations where transitions can be triggered unexpectedly (for instance, passing aliased parameters to a method that expects unaliased parameters, or calling a method that has a side effect through an alias deeply nested in a data structure). We propose a generalization ofaccess permissionsthat goes beyond a fixed set of permissions to an object. In this paper we present a new aliasing control mechanism that uses a small set of permissions as building block for the creation of views that capture a projection of an object with specific access constraints to its fields and/or methods. This makes permission tracking more fine grained while also making the designer's intent more explicit. We present a few meaningful examples of how theseviewshandle situations such as: separating different sections of an object for safe initialization; and access with either an unbounded number of readers or a single writer (multiple readers or unique writer). Finally, we show a type system for checking correctness of state use in the presence of this kind of controlled aliasing.
Original languageUnknown
Title of host publicationAssociation for Computing Machinery Digital Library
Publication statusPublished - 1 Jan 2010
EventFormal Techniques for Java-Like Programs (FTfJP) -
Duration: 1 Jan 2010 → …


ConferenceFormal Techniques for Java-Like Programs (FTfJP)
Period1/01/10 → …

Cite this