Many languages and language extensions include annotations on pointer variables suchas “read-only,” “unique,” and “borrowed”;
many more annotations have been proposed but not implemented. Unfortunately, all these annotations are described individually
and formalised independently — assuming they are formalised at all. In this paper, we show how these annotations can be subsumed
into a general capability system for pointers. This system separates mechanism (defining the semantics of sharing and exclusion)
from policy (defining the invariants that are intended to be preserved). The capability system has a welldefined semantics
which can be used as a reference for the correctness of various extended type systems using annotations. Furthermore, it supports
researchin new less-restrictive type systems that permit a wider range of idioms to be statically checked.
Work supported in part by the National Science Foundation (CCR-9984681) and the Defense Advanced Research Projects Agency
and Rome Laboratory, Air Force Materiel Command, USAF under contract F30602-99-2-0522. The views and conclusions contained
herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements,
either expressed or implied, of the National Science Foundation, Defense Advanced Research Projects Agency, Rome Laboratory,
or the U.S. Government.