Universe Type System
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 also worked 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.
We integrated the Universe type system into the external page MultiJava compiler and the external page JML Tools.
Key Publications
- W. Dietl, S. Drossopoulou, and P. Müller: Separating ownership topology and encapsulation with generic universe types
ACM Trans. Program. Lang. Syst., 2011. [PDF] [BIB] - W. Dietl, M. Ernst, and P. Müller: Tunable Static Inference for Generic Universe Types
European Conference on Object-Oriented Programming (ECOOP), 2011. [PDF] [BIB] - P. Müller and A. Rudich: Ownership Transfer in Universe Types
Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2007. [PDF] [BIB] - W. Dietl, S. Drossopoulou, and P. Müller: Generic Universe Types
European Conference on Object-Oriented Programming (ECOOP), 2007. [PDF] [BIB] - P. Müller, A. Poetzsch-Heffter, and G.T. Leavens: Modular Invariants for Layered Object Structures
Science of Computer Programming, 2006. [PDF] [BIB] - W. Dietl and P. Müller: Universes: Lightweight Ownership for JML
Journal of Object Technology (JOT), 2005. [BIB] JOT-Online
Acknowledgments
The work on Universe Types was a collaboration with external page Werner Dietl, University of Waterloo, who developed Generic Universe Types and the tool support during his time at ETH. We collaborated with the developers of the external page MultiJava compiler and the external page JML Tools. Special mention is due to external page Gary Leavens and external page Sophia Drossopoulou.