Safe initialization of objects

The inception of object-oriented programming introduces a category of bugs related to object construction: initialization errors. Every newly created object goes through several initialization states: starting from a state where all fields are uninitialized until all of them are assigned. Any operation on the object during its initialization process, which usually happens in the constructor via this, has to observe the initialization states of the object for correctness, i.e. only initialized fields may be used.

Checking safe usage of this statically, without manual annotation of initialization states in source code, is a challenge, due to aliasing and virtual method calls on this. Mainstream languages either do not check initialization errors, such as Java, C++, Scala, or they defend against them by not supporting useful initialization patterns, such as Swift. In parallel, past research has shown that safe initialization can be achieved for varying degrees of expressiveness but by sacrificing syntactic simplicity.

Based on formal reasoning about initialization, we advocate four design principles of initialization systems: monotonicity, authority, scopability and stackability. The principles enable local reasoning of initialization, which is the key enabler for efficient algorithms. They also enable sound strong updates in a flow-insensitive system, which is the key to support typestate polymorphism via subtyping. We put forward a type-based model for initialization, which consists of three abstractions, namely cold, warm and hot. The introduction of warm improves the expressiveness of existing models that classify objects either as initialized (i.e. hot) or non-initialized (i.e. cold).

Finally, we propose a novel type-and-effect inference system for a practical fragment of the type-based model, which significantly cuts down syntactic overhead of type-based solutions. The system scales to complex language features, such as functions, traits and inner classes, and it integrates well with compilers. The system introduces the concept of potentials to control aliasing in type-and-effect systems.

We implement an initialization system for Scala 3. The experiments on real-world projects show that our system significantly advances the state-of-the-art.