Combining traits with boxes and ownership types in a Java-like setting

The box model is a lightweight component model for the object-oriented paradigm, which structures the flat object-heap 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 provide 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.

► We integrate traits into an ownership type system for boxes.
► This combination supports code sharing between standard and box classes.
► An ownership type system and the corresponding soundness proofs are presented.