Research Project Description: 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 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.
We integrated the Universe type system into the
MultiJava compiler
and the
JML Tools.
We have a separate description of
our tools.
Publications:
- W. Dietl and P. Müller:
Ownership Type Systems and Dependent Classes
Foundations of Object-Oriented Languages (FOOL),
2008.
[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
- W. Dietl and P. Müller:
Runtime Universe Type Inference
International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO),
2007.
[PDF]
[BIB]
- W. Dietl and P. Müller:
2007 State of the Universe Address
International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO),
2007.
[PDF]
[BIB]
- W. Dietl and S. Drossopoulou and P. Müller:
Generic Universe Types
Foundations and Developments of Object-Oriented Languages (FOOL/WOOD '07), 2007.
[PDF]
[BIB]
- W. Dietl and S. Drossopoulou and P. Müller:
Formalization of Generic Universe Types
Technical Report, ETH Zurich, 2006.
[PDF]
[BIB]
- W. Dietl and P. Müller:
Universes: Lightweight Ownership for JML
Journal of Object Technology (JOT), 2005.
[PDF]
[BIB]
- W. Dietl, P. Müller, and A. Poetzsch-Heffter:
A Type System for Checking Applet Isolation in Java Card
Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS), 2004.
[PDF]
[BIB]
- W. Dietl and P. Müller:
Exceptions in Ownership Type Systems
Formal Techniques for Java-like Programs, 2004.
[PDF]
[BIB]
We collaborate with the developers of the
MultiJava compiler
and the
JML Tools.
Special mention is due to
Gary Leavens
and
Sophia Drossopoulou.
Werner M. Dietl
E-mail: Werner.Dietl@inf.ethz.ch
Homepage: http://pm.inf.ethz.ch/people/dietl/
|
