Semantics of fractional permissions with nesting

8 years 7 months ago
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...
John Tang Boyland
Added 31 Jan 2011
Updated 31 Jan 2011
Type Journal
Year 2010
Authors John Tang Boyland
Comments (0)