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.