Object Ownership

Object-oriented programs can create an entangled web of references between objects, making program understanding hard. Multiple references to the same object - so-called aliasing of objects - may result in unexpected state-changes of an object and makes it hard to build large object-oriented systems out of smaller components. This also leads to problems in several other areas of software engineering, for example, concurrent programming and modular verification of properties.

Object ownership was proposed as a possible solution to this problem. Instead of having an unstructured heap, some structure is enforced. Objects own other objects and thereby build a hierarchical structure.

Several different proposals of dynamic encodings of object ownership and of static ownership type systems exist today.

The Universe type system is an extended type system for object-oriented languages geared towards modular verification of programs. An object owns a set of representation objects, to which it has privileged access. The type system statically ensures that the heap will be well-structured and that only the owner of an object can initiate a modification.

I designed and formalized Generic Universe Types which combine type genericity with the Universe type system and allow one to statically check ownership structures that previously needed runtime checks. I rigorously proved the soundness of Generic Universe Types to gain detailed understanding of the properties of the type system.

I implemented Generic Universe Types in the Java Modeling Language (JML) tools and, together with students, I also implemented features like bytecode support, runtime checks, and support for the Eclipse IDE. More recently, I implemented a GUT type checker using the Checker Framework.

Also see the Checker Inference project for a tool that helps in annotating programs with Generic Universe Types.

As part of my PhD thesis I generated a formalization of GUT using Ott. Have a look at the Ott output (.pdf and the Ott inputs (.tar.bz2.

The GUT type checker contains a type checker and a type inference component. See file README for installation instructions.

The ECOOP 2011 version of the type checker is available for archival purposes.

See my previous page at ETH Zurich for information about the different tools. Also, see my publications page.