Universes: Lightweight Ownership for JML

Abstract

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.