Résumé: 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 ?gfractional heaps.?h We show that the fraction law  ?? 12  + 12  permits sound reasoning and that nesting can be carried out safely using only local reasoning.

Langue: Anglais