Article

Non-null references by default in the Java modeling language

Authors:

Patrice Chalin,

Frédéric RiouxAuthors Info & Claims

SAVCBS '05: Proceedings of the 2005 conference on Specification and verification of component-based systems

Pages 9 - es

https://doi.org/10.1145/1123058.1123068

Published: 05 September 2005 Publication History

Abstract

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.

References

[1]

M. Barnett, K. R. M. Leino, and W. Schulte, "The Spec# Programming System: An Overview." In Proceedings of the International Workshop on the Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS 2004), Marseille, France, LNCS, vol. 3362, 2004.]]

[2]

D. Bonniot. The Nice programming language, http://nice.sourceforge.net/, June 2005.]]

[3]

D. Bonniot. Type safety in Nice: Why programs written in Nice have less bugs, http://nice.sourceforge.net/safety.html, June 2005.]]

[4]

L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll, "An overview of JML tools and applications," International Journal on Software Tools for Technology Transfer (STTT), 2004.]]

[5]

P. Chalin and F. Rioux, Non-null References by Default in the Java Modeling Language, Dependable Software Research Group, Concordia University, ENCS-CSE TR 2005--004. June, 2005.]]

[6]

D. Evans and D. Larochelle, "Improving security using extensible lightweight static analysis," IEEE Software, vol. 19, no. 1, pp. 42--51, Jan.-Feb., 2002.]]

Digital Library

[7]

M. Fähndrich and K. R. M. Leino, "Declaring and checking non-null types in an object-oriented language," in Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications. OOPSLA'03: ACM Press, 2003, pp. 302--312.]]

Digital Library

[8]

C. Flanagan and K. R. M. Leino, "Houdini, an Annotation Assistant for ESC/Java." In Proceedings of the International Symposium of Formal Methods Europe, Berlin, Germany, vol. 2021, pp. 500--517, 2001.]]

Digital Library

[9]

M. Fowler, Refactoring: Improving the Design of Existing Code. Object Technology Series. Addison-Wesley, 1999.]]

Digital Library

[10]

J. V. Guttag and J. J. Horning, Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer-Verlag, 1993.]]

Digital Library

[11]

G. T. Leavens, A. L. Baker, and C. Ruby, "JML: A Notation for Detailed Design," in Behavioral Specifications of Businesses and Systems, B. R. Haim Kilov, Ian Simmonds, Ed.: Kluwer, 1999, pp. 175--188.]]

[12]

G. T. Leavens, K. R. M. Leino, E. Poll, C. Ruby, and B. Jacobs, "JML: notations and tools supporting detailed design in Java," in OOPSLA 2000 Companion, Minneapolis, Minnesota, 2000, pp. 105--106.]]

Digital Library

[13]

G. T. Leavens, A. L. Baker, and C. Ruby, Preliminary Design of JML: A Behavioral Interface Specification Language for Java, Department of Computer Science, Iowa State University TR #98-06-rev27. April, 2005.]]

[14]

G. T. Leavens, Y. Cheon, C. Clifton, C. Ruby, and D. R. Cok, "How the design of JML accommodates both runtime assertion checking and formal verification," Science of Computer Programming, vol. 55, no. 1--3, pp. 185--208, 2005.]]

Digital Library

[15]

B. Meyer, Eiffel: The Language. Object-Oriented Series. New York. Prentice-Hall, 1991.]]

Digital Library

[16]

B. Meyer, Eiffel: The Language, Draft of future edition, revision 5.00 (June 2005) ed. Unpublished, 2005.]]

Digital Library

[17]

A. D. Raghavan and G. T. Leavens, Desugaring JML Method Specifications, Department of Computer Science, Iowa State University TR #00-03e. May, 2005.]]

[18]

F. Rioux and P. Chalin, "Improving the Quality of Web-based Enterprise Applications with Extended Static Checking: A Case Study." In Proceedings of the 1st International Workshop on Automated Specification and Verification of Web Sites, Valencia, Spain, Electronic Notes in Theoretical Computer Science, March 14--15, 2005 (to appear).]]

Cited By

Schiller TDonohue KCoward FErnst MJalote PBriand LHoek A(2014)Case studies and tools for contract specificationsProceedings of the 36th International Conference on Software Engineering10.1145/2568225.2568285(596-607)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2568225.2568285
Brucker AKrieger MWolff B(2009)Extending OCL with null-referencesProceedings of the 2009 international conference on Models in Software Engineering10.1007/978-3-642-12261-3_25(261-275)Online publication date: 4-Oct-2009
https://dl.acm.org/doi/10.1007/978-3-642-12261-3_25
Chalin PJames P(2007)Non-null references by default in javaProceedings of the 21st European conference on Object-Oriented Programming10.5555/2394758.2394776(227-247)Online publication date: 30-Jul-2007
https://dl.acm.org/doi/10.5555/2394758.2394776
Show More Cited By

Index Terms

Non-null references by default in the Java modeling language

Recommendations

Non-null references by default in the Java modeling language

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 ...
JML and OpenJML for Java 16
FTfJP '21: Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs

As the Java language evolves, the Java Modeling Language (JML) and the OpenJML deductive verification tool must evolve with it. Changes in Java since Java 8 bring language and organizational changes which affect the semantics of JML and the ...
Non-null references by default in java: alleviating the nullity annotation burden
ECOOP'07: Proceedings of the 21st European conference on Object-Oriented Programming

With Java 5 annotations, we note a marked increase in tools that statically detect potential null dereferences. To be effective such tools require that developers annotate declarations with nullity modifiers and have annotated API libraries. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SAVCBS '05: Proceedings of the 2005 conference on Specification and verification of component-based systems

September 2005

95 pages

ISBN:1595933719

DOI:10.1145/1123058

Program Chair:
Gary T. Leavens
Iowa State

ACM SIGSOFT Software Engineering Notes Volume 31, Issue 2
March 2006
193 pages
ISSN:0163-5948
DOI:10.1145/1118537
Issue’s Table of Contents

Copyright © 2005 Authors.

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 September 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Acceptance Rates

SAVCBS '05 Paper Acceptance Rate 15 of 15 submissions, 100%;

Overall Acceptance Rate 37 of 46 submissions, 80%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
227
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Schiller TDonohue KCoward FErnst MJalote PBriand LHoek A(2014)Case studies and tools for contract specificationsProceedings of the 36th International Conference on Software Engineering10.1145/2568225.2568285(596-607)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2568225.2568285
Brucker AKrieger MWolff B(2009)Extending OCL with null-referencesProceedings of the 2009 international conference on Models in Software Engineering10.1007/978-3-642-12261-3_25(261-275)Online publication date: 4-Oct-2009
https://dl.acm.org/doi/10.1007/978-3-642-12261-3_25
Chalin PJames P(2007)Non-null references by default in javaProceedings of the 21st European conference on Object-Oriented Programming10.5555/2394758.2394776(227-247)Online publication date: 30-Jul-2007
https://dl.acm.org/doi/10.5555/2394758.2394776
Shaner SLeavens GNaumann D(2007)Modular verification of higher-order methods with mandatory calls specified by model programsACM SIGPLAN Notices10.1145/1297105.129705342:10(351-368)Online publication date: 21-Oct-2007
https://dl.acm.org/doi/10.1145/1297105.1297053
Shaner SLeavens GNaumann DGabriel RBacon DLopes CSteele G(2007)Modular verification of higher-order methods with mandatory calls specified by model programsProceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems, languages and applications10.1145/1297027.1297053(351-368)Online publication date: 21-Oct-2007
https://dl.acm.org/doi/10.1145/1297027.1297053
Kiniry JMorkan ACochran DFairmichael FChalin POostdijk MHubbers E(2007)The KOA Remote Voting System: A Summary of Work to DateTrustworthy Global Computing10.1007/978-3-540-75336-0_16(244-262)Online publication date: 2007
https://doi.org/10.1007/978-3-540-75336-0_16
Chalin P(2006)Are practitioners writing contracts?Rigorous Development of Complex Fault-Tolerant Systems10.5555/2167981.2167987(100-113)Online publication date: 1-Jan-2006
https://dl.acm.org/doi/10.5555/2167981.2167987
Kiniry JMorkan ACochran DFairmichael FChalin POostdijk MHubbers E(2006)The KOA remote voting systemProceedings of the 2nd international conference on Trustworthy global computing10.5555/1776656.1776678(244-262)Online publication date: 7-Nov-2006
https://dl.acm.org/doi/10.5555/1776656.1776678
Kulczycki GVasudeo J(2006)Simplifying reasoning about objects with TakoProceedings of the 2006 conference on Specification and verification of component-based systems10.1145/1181195.1181207(57-64)Online publication date: 10-Nov-2006
https://dl.acm.org/doi/10.1145/1181195.1181207
Leavens GCok DNilizadeh A(2022)Further Lessons from the JML ProjectThe Logic of Software. A Tasting Menu of Formal Methods10.1007/978-3-031-08166-8_15(313-349)Online publication date: 4-Jul-2022
https://doi.org/10.1007/978-3-031-08166-8_15

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents