An Immutability Type System for Classes and Objects: Improvements, Experiments, and Comparisons

Abstract

Mutability, the ability for an object to change, is frequently cited as one of the sources of software problems. Ensuring the immutability of objects opens opportunities for optimizations, e.g., removing the need for locks in a concurrent environment for an immutable object. This thesis explores an approach to analyze immutability of classes and objects by using static analysis with pluggable type systems. A properly implemented pluggable type system can statically analyze the mutability property of an object without execution. This thesis presents (1) the analysis of some previous work, including Javari, ReIm, and Glacier, (2) improvements to a pluggable type system, PICO, to enhance the soundness of the formalization and to improve the user experience, and (3) experiments with the enhanced PICO with real projects, and comparisons with the results of the previous work.

PICO is an immutability type system that analyzes and enforces the mutability property of an object so that a mutation on an immutable object can be statically detected. Although many modern programming languages have various means of declaring this property, PICO provides an easier, more flexible, and foolproof way to declare the mutability property of a class by automating the check of immutability.

While PICO is a novel work in improving the flexibility of the immutability type system, it has certain bad designs for defaulting in parts of the immutability rules. Such bad designs would lead to the risk of allowing the mutation of an immutable object, known as the false negative. To solve this problem, this thesis provides more sound formalization to fix the false negative.

Also, PICO contains counterintuitive logic, such as unsafe defaulting. To solve the counterintuitive logic, this thesis presents a new defaulting scheme for PICO, and reports various minor changes made to improve the user-friendliness during the type checking process.

This thesis conducts experiments on small code snippets and large real-world projects, and also compares the new PICO with previous works on immutability to find more potential problems and demonstrates the flexibility and usability of PICO compared with previous projects, e.g., Glacier.