Summers, Alexander J.
Rights / licenseIn Copyright - Non-Commercial Use Permitted
Null pointer dereferences are the most common runtime error in languages such as Java and C#. To alleviate this problem, Fähndrich and Leino proposed a non-null type system, in which reference types can be annotated with non-nullity expectations that are statically enforced. The main challenge for the static checking of non-nullity is object initialisation; since fields of new objects get first initialised with null, a non-null type system needs to determine when an object is fully initialised and, thus, its non-null fields actually contain non-null values. Several proposed solutions exist for tackling this problem, but each fail on one of the three criteria of soundness, flexibility and simplicity. In this paper we present a solution which satisfies all three criteria, making it suitable for mainstream use. We provide a formalisation of the core type system and prove soundness for a small language. We also show informally how the core type system can be extended to support a realistic language Show more
Journal / seriesTechnical Report
PublisherETH Zurich, Department of Computer Science
Organisational unit03653 - Müller, Peter
02150 - Departement Informatik / Department of Computer Science
MoreShow all metadata