A Type-and-Effect System for Object Initialization

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, like Java, C++, Scala, or they defend against them by not supporting useful initialization patterns, like Swift. In parallel, past research has shown that safe initialization can be achieved for varying degrees of expressiveness but by sacrificing syntactic simplicity. We approach the problem by upholding two fundamental principles for reasoning about the initialization of objects: stackability and monotonicity. On this basis, we propose a novel type-and-effect system that can effectively ensure initialization safety while allowing flexible initialization patterns with almost zero annotation burden. The experiments on several real-world projects show that our system advances the state-of-the-art.

Jan 09 2020

 Record created 2020-01-09, last modified 2020-01-13

Rate this document:

Rate this document:
(Not yet reviewed)