Expressive type systems for object-oriented languages

Expressive type-systems for object-oriented languages can help improve programmer productivity and system performance. This thesis describes type-based solutions for problems that are commonly addressed using flow-analysis. Specifically, this thesis introduces two extensions to standard object-oriented type systems that enable the programmer to concisely specify additional common and useful invariants. A concise specification is facilitated in both cases by using problem-specific constraint systems in the type rules.;The first extension enables programmers to control aliasing of objects and thereby strengthens the encapsulation paradigm in object-oriented languages. Existing object-oriented languages provide little support for encapsulating objects. Reference semantics allow objects to escape their defining scope, and the pervasive aliasing that ensues remains a major source of software defects. Chapter 2 introduces a type system that can guarantee confinement ---the property that all instances of a given type are encapsulated in their defining package Chapter 2 presents Kacheck/J, a tool for inferring confined types for large Java programs. Our goal is to develop practical tools to assist software engineers, thus we focus on simple and scalable techniques. Confinement can be used to identify accidental leaks of sensitive objects, as well as for compiler optimizations. We report on the analysis of a large body of code and discuss language support and refactoring for confinement.;The second extension focuses on memory safety, specifically for accesses to distributed arrays. A fundamental concept for programming with these arrays is the use of regions. A region is a set of points, and enables the programmer to give high-level specifications for the shape of arrays and for iterations over sets of indices. Arrays over regions were introduced in ZPL in the late 1990s and later adopted in Titanium and X10 as a means of simplifying the programming of high-performance software. While convenient, regions do not eliminate the risk of memory safety violations in the form of accesses outside of the bounds of arrays. Until now, language implementations have resorted to checking array accesses dynamically or to warning the programmer that bounds violations lead to undefined behavior. Chapter 3 shows that a type system for a language with arrays over regions can guarantee that array bounds violations cannot occur. Our type system uses dependent types and enables safety without dynamic bounds checks. We have developed a core language and a type system, proven type soundness and settled the complexity of the key decision problems.;A prototype implementation which embodies the ideas of our core language has been developed for X10, a new language for high performance computing. We have implemented a type checker for our variant of X10 and experimented with a variety of benchmark programs. Some of the internals of the implementation of both type system extensions are covered in Appendix A.