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.

Cite as:

Werner Dietl, Peter Müller, “Universes: Lightweight Ownership for JML”, Journal of Object Technology, Volume 4, no. 8 (October 2005), pp. 5-32, doi:10.5381/jot.2005.4.8.a1.

PDF | HTML | DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn

The JOT Journal   |   ISSN 1660-1769   |   DOI 10.5381/jot   |   AITO   |   Open Access