Candidate: Lian Sun
Title: An Immutability Type System for Classes and Objects: Improvements, Experiments, and Comparisons
Date: April 6, 2021
Time: 4:00 PM
Place: Remote
Supervisor(s): Dietl, Werner
Abstract:
Mutability is frequently cited as the source of software problems. If the immutability status is enforced correctly, the program will benefit from various aspects, such as a guaranteed immutable state in a multi-thread environment, or a key in a hash map that is guaranteed to never alternate. This thesis explores the use of static analysis with pluggable type systems for immutability analysis of classes and objects. A properly implemented pluggable type system can analysis the mutability property of an object before the program executes. This thesis presents (1) the analysis of the previous solutions, (2) improvements made on a immutability pluggable type system, PICO, to enhance the soundness of the formalization or improve user experience, and (3) experiments of the enhanced PICO with real projects, and comparisons with the previous solutions.
PICO is an immutability type system that enforces and analyses the mutability property of an object to prevent the accidental mutating of a immutable object. Although many modern programming language provide a way to provide immutability to classes, PICO provides a more easy, flexible and foolproof way to declare the mutability property of a class.
While PICO is a novel work exploring the possibility of utilizing the receiver and assignment context to improve the flexibility of itself, it oversights certain unsoundness in some part of the formalization of immutable rules. Such unsoundness would introduce the risk of allowing the mutation of a immutable object, known as false negatives. To solve the unsoundness, this thesis provides more sound formalization to fix the false negative.
In addition to the unsoundness, PICO also contains counterintuitive logic, such as an unsafe defaulting. To solve the counterintuitive logic, this thesis presents a new defaulting scheme to PICO, and various minor changes to improve the user-friendliness during the type checking process.
This thesis conducts experiments on small code snippets and large real-world projects. This thesis also compares the new PICO with previous works on the immutability to find more potential problems and illustrate the flexibility and usability of PICO compared with other projects, such as Glacier.