Semantics of Fractional Permissions with Nesting

by John Boyland

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.

BibTeX Style Reference

@article(boyland:10frac-nesting,
  author =      {John Boyland}
  title =       {Semantics of Fractional Permissions with Nesting},
  journal = toplas,
  volume = 32
  number = 6,
  pages = {Article~22},
  month = aug,
  year = 2010)

How to Get a Copy

The article is available from the ACM digital library. An earlier technical report is available in PDF (but the article was extensively revised). The electronic appendix (machine-checked proofs) is also available.

Last Modified: April 11, 2011