Combining Traits with Boxes and Ownership Types in a Java-like Setting

The box model is a light-weight component model for the object-oriented paradigm, which structures the flat objectheap into hierarchical runtime components called boxes. Boxes have clear runtime boundaries that divide the objects of a box into objects that can be used to interact with the box (the boundary objects) and objects that are encapsulated and represent the state of the box (the local objects). The distinction into local and boundary objects is statically achieved by an ownership type system for boxes that uses domain annotations to classify objects into local and boundary objects and that guarantees that local objects can never be directly accessed by the context of a box. A trait is a set of methods divorced from any class hierarchy. Traits are units of fine-grained reuse that can be composed together to form classes or other traits. This paper integrates traits into an ownership type system for boxes. This combination is fruitful in two ways: it can statically guarantee encapsulation of objects and still provides fine-grained reuse among classes that goes beyond the possibilities of standard inheritance. It also solves a specific problem of the box ownership type system: namely that box classes cannot inherit from standard classes (and vice versa) and thus code sharing between these two kinds of classes was not possible in this setting so far. We present an ownership type system and the corresponding soundness proofs that guarantee encapsulation of objects in an object-oriented language with traits.