Universes: Lightweight Ownership for JML
By: Werner Dietl, Peter Müller
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. This paper describes 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.