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 pageMultiJava compiler and the external pageJML 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 pageWerner 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 pageMultiJava compiler and the external pageJML Tools. Special mention is due to external pageGary Leavens and external pageSophia Drossopoulou.