Establishing Object Invariants with Delayed Types

Establishing Object Invariants with Delayed Types. Manuel Fähndrich, Songtao Xia.

Mainstream object-oriented languages such as C# and Java provide an initializationmodel for objects that does not guarantee programmer controlled initialization of fields. Instead, all fields are initialized to default values (0 for scalars and null for non-scalars) on allocation. This is in stark contrast to functional languages, where all parts of an allocation are initialized to programmer-provided values. These choices have a direct impact on two main issues: 1) the prevalence of null in object oriented languages (and its general absence in functional languages), and 2) the ability to initialize circular data structures. This paper explores connections between these differing approaches and proposes a fresh look at initialization. Delayed types are introduced to express and formalize prevalent initialization patterns in object-oriented languages.

It's interesting to note that in Ada type definitions can contain initializers (i.e., initialization expressions), partly because constructors were introduced into the language only in the second revision of the language (Ada95).