UniverseTypeSystemExplanation

Object-oriented programs with arbitrary object structures are difficult to understand, to maintain, and to reason about since, in theory, all objects can interact with each other and methods might access any object in the heap memory via reference chains.

To support modular verification, especially of invariants, we developed a new programming model and type system for a subset of Java. This type system allows one to structure the heap memory into so-called universes and provides rigor, statically checkable control of references across universe boundaries. To make the universe type system available to a wider community and as a basis for case studies, we currently implement it as a part of the Java Modeling Language JML.

We are working on the static and dynamic inference of ownership properties in order to ease the transition from current Java programs to programs that use the Universe type system. To support modular inference of annotations we evaluate different possible extensions to the Universe type system. The introduction of type variables could allow partial inference of annotations.

Publications

• W. Dietl and P. Müller: Universes: Lightweight Ownership for JML. Journal of Object Technology (JOT), 2005. PDF, BIB
• D. Cunningham and W. Dietl and S. Drossopoulou and A. Francalanza and P. Müller and A. J. Summers: Universe Types for Topology and Encapsulation. Formal Methods for Components and Objects (FMCO), 2008. To appear. PDF BIB
• W. Dietl and S. Drossopoulou and P. Müller: Generic Universe Types. European Conference on Object-Oriented Programming (ECOOP), 2007. PDF BIB Springer-Online
• P. Müller and A. Rudich: Ownership Transfer in Universe Types. Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2007. PDF BIB

See the homepage for a complete list.

Version: 3 Time: Tue Oct 7 21:09:17 2008 Author: wdietl (None) IP: 129.132.105.183