Universe Types: Topology, encapsulation, genericity, and tools
Werner Dietl · Repository for Publications and Research Data (ETH Zurich) · 2009
We present Generic Universe Types, a sound, lightweight ownership type system for type-generic object-oriented programming languages, which cleanly separates the ownership topology from the owner-as-modifier encapsulation discipline and is supported by a comprehensive set of tools.Mutable references give object-oriented programming languages the power to build complex object structures and to efficiently modify them.However, this power comes at the cost of aliasing: two or more references to the same object can exist, and the modifications performed through one reference are visible through all other references.In main-stream object-oriented languages, like Java and C , objects and references build a complicated mesh and there is no support to structure the heap.Visibility modifiers (such as private and protected in Java) only deal with information hiding, for example, ensuring that a field is only accessible from within its declaring class.However, the object referenced by that field might still be aliased and modified by other objects at runtime.There is no support to encapsulate object structures and to ensure that objects at runtime are only accessed in a controlled fashion.Aliasing and the unstructured nature of the heap lead to problems with, for example, understanding the behavior of a program, adapting a consistent locking discipline to ensure correct concurrent behavior, exchanging the implementation of an interface, and the formal verification of properties.The concept of object ownership has been proposed as a mechanism to structure the heap hierarchically and to provide encapsulation of object structures.Each object is assigned at most one other object as its owning object, and restrictions are enforced on the references.Ownership type systems provide static type annotations to enforce an ownership topology and encapsulation.For maintaining invariants, the existence of aliases is no problem, as long as these aliases are not used to modify the internal representation of a different object.We call this encapsulation system the owner-as-modifier discipline, because it guarantees that the owner object is always in control of modifications.The Universe type system is a lightweight ownership type system that enforces the owner-as-modifier discipline and supports the modular verification of object-oriented programs.We define Generic Universe Types (GUT), a combination of type genericity with Universe types.GUT subsumes the previous non-generic Universe type system and cleanly separates the topology from the encapsulation system.We give a complete formalization of the GUT system and prove it sound.Usually, ownership type systems entangle the enforcement of the ownership topology with the enforcement of an encapsulation system; that is, the structuring of the heap and the restrictions on the use of references are enforced together.In this thesis, we cleanly separate the ownership topology from the encapsulation system, giving a cleaner formalization and allowing the separate reuse.