Non-null references by default in the Java modeling language. - Chalin, Patrice
Based on our experiences and those of our peers, we hypothesized that in Java code, the majority of declarations that are of reference types are meant to be non-null. Unfortunately, the Java Modeling Language (JML), like most interface specification and object-oriented programming languages, assumes that such declarations are possibly-null by default. As a consequence, developers need to write specifications that are more verbose than necessary in order to accurately document their module interfaces. In practice, this results in module interfaces being left incompletely and inaccurately specified. In this paper we present the results of a study that confirms our hypothesis. Hence, we propose an adaptation to JML that preserves its language design goals and that allows developers to specify that declarations of reference types are to be interpreted as non-null by default. We explain how this default is safer and results in less writing on the part of specifiers than null-by-default. The paper also reports on an implementation of the proposal in some of the JML tools.
Keywords: Software; Software Engineering; Software / Program Verification; Programming by contract; Programming languages; Language constructs and features; Theory of Computation; Logics and meanings of programs; Specifying and verifying and reasoning about programs; Design; Documentation; Languages; Theory; Verification; JML; Contracts; Java modeling language; Non-null references; Reference types