Semantics of fractional permissions with nesting

Abstract

Permissions specify mutable state that can be accessed by a program. Fractions distinguish write access (1) from read access (any smaller fraction). Nesting can model object invariants and ownership. Fractional permissions provides a foundation the meaning of many of access-based annotations: uniqueness, read-only, immutability, method effects, guarded state, etc. The semantics of fractional permissions with nesting is given in terms of "fractional heaps." We show that the fraction law π = 1/2π + 1/2π permits sound reasoning and that nesting can be carried out safely using only local reasoning. © 2010 ACM.