Semantics of fractional permissions with nesting

Fractional permissions use fractions to distinguish write access (1) from read access (any smaller fraction). Nesting (an extension of adoption) can be used to model object invariants and ownership. Indeed nesting extends both in a form of “monotonically increasing invariants.” Fractional permissions thus provides a foundation for defining the meaning of a large variety of access-based annotations: uniqueness, read-only, immutability, method effects, lock protected state etc. In this paper we give a semantics of fractional permissions with nesting (adoption), in terms of “fractional heaps” indicating the mutable state that can be accessed using each permission. We show that fractions are sound and that the system satisfies separation properties. Department of Electrical Engineering and Computer Science Technical Report CS-07-01 Work supported in part by the National Science Foundation (CCF-0702635). The opinions expressed here are not necessarily those of the National Scien...

• Type: Journal
• Year: 2010
• Where: TOPLAS
• Authors: John Tang Boyland
• Keywords: Fractional Permissions, National Science Foundation, Science Technical Report, TOPLAS 2010