Universes: Lightweight Ownership for JML

Object-oriented programs with arbitrary object structures are difficult to understand, to maintain, and to reason about. Ownership has been applied successfully to structure the object store and to restrict how references can be passed and used. We describe how ownership relations can be expressed in the Java Modeling Language, JML. These ownership specifications can be checked by standard verification techniques, runtime assertion checking, ownership type systems, or combinations of these techniques. We show that the combination of the lightweight Universe type system and JML specifications is flexible enough to handle interesting implementations while keeping the annotation and checking overhead small. The Universe type system has been implemented in the JML compiler. This integration enables the application of ownership-based verification techniques to programs specified in JML.