Declaring and checking non-null types in an object-oriented language

ABSTRACT

Distinguishing non-null references from possibly-null references at the type level can detect null-related errors in object-oriented programs at compile-time. This paper gives a proposal for retrofitting a language such as C# or Java with non-null types. It addresses the central complications that arise in constructors, where declared non-null fields may not yet have been initialized, but the partially constructed object is already accessible. The paper reports experience with an implementation for annotating and checking null-related properties in C# programs.

REFERENCES

• 1: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, ACM SIGPLAN Notices, v.36 n.5, p.59-69, May 2001
• 2: ECMA. Standard ECMA-334: C# Language Specification, December 2002. Available on the web as http://www.ecma-international.org/publications/files/ecma-st/Ecma-334.pdf.
• 3: David Evans , John Guttag , James Horning , Yang Meng Tan, LCLint: a tool for using specifications to check code, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.87-96, December 06-09, 1994, New Orleans, Louisiana, United States
• 4: Manuel Fähndrich and K. Rustan M. Leino. Heap monotonic typestates. In Proceedings of the 1st International Workshop on Aliasing, Confinement and Ownership, July 2003.
• 5: Kathleen Fisher , John Reppy, The design of a class mechanism for Moby, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.37-49, May 01-04, 1999, Atlanta, Georgia, United States
• 6: Robert Fitzgerald , Todd B. Knoblock , Erik Ruf , Bjarne Steensgaard , David Tarditi, Marmot: an optimizing compiler for Java, Software—Practice & Experience, v.30 n.3, p.199-232, Mar.1.2000 [doi>10.1002/(SICI)1097-024X(200003)30:3<199::AID-SPE296>3.0.CO;2-2]
• 7: Cormac Flanagan , Matthew Flatt , Shriram Krishnamurthi , Stephanie Weirich , Matthias Felleisen, Catching bugs in the web of program invariants, ACM SIGPLAN Notices, v.31 n.5, p.23-32, May 1996
• 8: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 9: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 10: Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
• 11: Barbara Liskov, Dorothy Curtis, Mark Day, Sanjay Ghemawat, Robert Gruber, Paul Johnson, and Andrew C. Myers. Theta reference manual, preliminary version. Memo~88, Programming Methodology Group, MIT Laboratory for Computer Science, February 1995. Available on the web at http://www.pmg.lcs.mit.edu/Theta.html.
• 12: Barbara Liskov , John Guttag, Abstraction and specification in program development, MIT Press, Cambridge, MA, 1986
• 13: Robin Milner , Mads Tofte , Robert Harper, The Definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 14: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 15: George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
• 16: Simon Peyton Jones, John Hughes, Lennart Augustsson, Dave Barton, Brian Boutel, Warren Burton, Joseph Fasel, Kevin Hammond, Ralf Hinze, Paul Hudak, Thomas Johnsson, Mark Jones, John Launchbury, Erik Meijer, John Peterson, Alastair Reid, Colin Runciman, and Philip Wadler. Haskell 98 report, February 1999. Available on the web as http://haskell.org/onlinereport.
• 17: Chris Smith. Java pointifications: Nullability constraints, June 2001. Available on the web as http://cdsmith.twu.net/professional/java/pontifications/nonnull.html.
• 18: Frederick Smith , David Walker , J. Gregory Morrisett, Alias Types, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.366-381, April 02, 2000
• 19: Raymie Stata. Improving the safety of Java, December 1995. Available on the web as http://larch-www.lcs.mit.edu:8001/\homedirraymie/Java/javachangessafety.html.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Reliability, Verification

Keywords:
Java, c#, non-null types, null references, type system