Your browser does not support JavaScript!
http://iet.metastore.ingenta.com
1887

Reducing the use of nullable types through non-null by default and monotonic non-null

Reducing the use of nullable types through non-null by default and monotonic non-null

For access to this article, please select a purchase option:

Buy article PDF
£12.50
(plus tax if applicable)
Buy Knowledge Pack
10 articles for £75.00
(plus taxes if applicable)

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Name:*
Email:*
Your details
Name:*
Email:*
Department:*
Why are you recommending this title?
Select reason:
 
 
 
 
 
IET Software — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

With Java 5 annotations, the authors note a marked increase in tools that can statically detect potential null dereferences. To be effective, such tools require that developers annotate declarations with nullity modifiers and have annotated API libraries. Unfortunately, in the experience of the authors, specifying moderately large code bases, the use of non-null annotations is more labour intensive than it should be. Motivated by this experience, the authors conducted an empirical study of five open source projects totalling 700K lines-of-code, which confirms that, on average, 75% of reference declarations are meant to be non-null, by design. Guided by these results, the authors propose the adoption of non-null-by-default semantics. This new default has advantages of better matching general practice, lightening developer annotation burden and being safer. The authors also describe the Eclipse Java Modelling Language (JML) Java Development Tooling (JDT), a tool supporting the new semantics, including the ability to read the extensive API library specifications written in the JML. Issues of backwards compatibility are addressed. In a second phase of the empirical study, the authors analysed the uses of null and noted that over half of the nullable field references are only assigned non-null values. For this category of reference, the authors introduce the concept of monotonic non-null type and illustrate the benefits of its use.

References

    1. 1)
      • Evans, D.: `Static detection of dynamic memory errors', Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, 1996, Philadelphia, PA.
    2. 2)
      • E. Gamma , R. Helm , R. Johnson , J.M. Vlissides . (1994) Design patterns: elements of reusable object-oriented software.
    3. 3)
      • Palsberg, J., Schwartzbach, M.I.: `Type substitution for object-oriented programming', Proc. European Conf. Object-Oriented Programming on Object-Oriented Programming Systems, Languages, and Applications, 1990, Ottawa, Canada, ACM.
    4. 4)
      • D. Bonniot . Using kinds to type partially-polymorphic methods. Electron. Notes Theor. Comput. Sci. , 1 - 20
    5. 5)
      • L.C. Paulson . (1996) ML for the working programmer.
    6. 6)
      • Ernst M., Coward D.: ‘Annotations on Java types’. JCP.org, JSR 308, 17 October 2006.
    7. 7)
    8. 8)
      • D. Flanagan . (1996) Java in a nutshell: a desktop quick reference.
    9. 9)
    10. 10)
      • Bierman, G., Meijer, E., Schulte, W.: `The essence of data access in Cω', Proc. European Conf. Object-Oriented Programming (ECOOP), 2005, Glasgow.
    11. 11)
      • JetBrains: ‘Nullable How-To’. IntelliJ IDEA 5.x Developer Documentation: JetBrains, 2006.
    12. 12)
      • Meyer, B.: `Attached types and their application to three open problems of object-oriented programming', Proc. European Conf. Object-Oriented Programming (ECOOP), 25–29 July 2005, Glasgow, p. 1–32, (LNCS, 3586).
    13. 13)
      • Evans D.: ‘Using specifications to check source code’. MIT, MIT/LCS/TR 628, June 1994.
    14. 14)
      • Erik, M., Brian, B., Gavin, B.: `LINQ: reconciling object, relations and xml in the .net framework', Proc. ACM SIGMOD Int. Conf. Management of Data, 2006, Chicago, IL, ACM.
    15. 15)
      • Pugh W.: ‘Annotations for software defect detection’. JCP.org, JSR 305, 2006.
    16. 16)
      • Leavens G.T., Cheon Y.: ‘Design by contract with JML’, Draft paper, 2005.
    17. 17)
      • INRIA, ‘Pointers in Caml’. Caml Documentation, Specific Guides, http://caml.inria.fr/resources/doc/, 2006.
    18. 18)
      • J.E. Freund . (1962) Mathematical statistics.
    19. 19)
      • Cielecki, M., Fulara, J., Jakubczyk, K., Jancewicz, L.: `Propagation of JML non-null annotations in Java programs', Proc. Int. Conf. Principles and Practices of Programming in Java (PPPJ), 2006, Mannheim, Germany.
    20. 20)
      • Stallman R.: ‘Using the GNU compiler collection (GCC): GCC Version 4.1.0’. Free Software Foundation, 2005.
    21. 21)
      • Microsoft Developer Network, ‘C run-time library: SAL annotations’. MSDN Library, Visual Studio 2008, Visual C++ Reference, 2008.
    22. 22)
      • Chalin, P.: `Towards support for non-null types and non-null-by-default in Java', Proc. 8th Workshop on Formal Techniques for Java-like Programs (FTfJP), July 2006, Nantes, France.
    23. 23)
      • Engelen, A.F.M.: `Nullness analysis of Java source code', 2006, Master's, Nijmegen Institute for Computing and Information Sciences, Radboud University Nijmegen, The Netherlands.
    24. 24)
      • D. Grossman , M. Hicks , T. Jim , G. Morrisett . Cyclone: a type-safe dialect of C. C/C++ Users J. , 1 , 275 - 288
    25. 25)
      • Kiniry, J.R.: ‘ESC/Java2'. http://secure.ucd.ie/products/opensource/ESCJava2, 2005.
    26. 26)
      • Evans D.: ‘Annotation-assisted lightweight static checking’. First Int. Workshop on Automated Program Analysis, Testing and Verification, February 2000.
    27. 27)
      • Barnett, M., DeLine, R., Jacobs, B.: `The Spec# programming system: challenges and directions', Int. Conf. Verified Software: Theories, Tools, Experiments (VSTTE), 2005, Zürich, Switzerland.
    28. 28)
      • Jim, T., Morrisett, G., Grossman, D., Hicks, M., Cheney, J., Wang, Y.: `Cyclone: a safe dialect of C', Proc. USENIX Annual Technical Conf., June 2002, Monterey, CA, p. 275–288.
    29. 29)
      • Bonniot D.: ‘Type safety in nice: why programs written in nice have less bugs’, 2005.
    30. 30)
      • Cok, D.R., Kiniry, J.R.: `ESC/Java2: Uniting ESC/Java and JML', ‘Proc. Int. Workshop on the Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS’04)', 10–14 March 2004, Marseille, France, p. 108–128, (LNCS, 3362).
    31. 31)
      • Fähndrich, M., Xia, S.: `Establishing object invariants with delayed types', Proc. ACM Conf. Object-Oriented Programming, Systems, and Applications, 2007, Montreal.
    32. 32)
      • M. Williams . (2002) Microsoft Visual C# .NET.
    33. 33)
      • B. Liskov , E. Moss , A. Snyder . (1984) CLU reference manual.
    34. 34)
      • M. Fowler . (1999) Refactoring: improving the design of existing code.
    35. 35)
      • M. Fowler . (2003) Patterns of enterprise application architecture.
    36. 36)
      • Bonniot D.: ‘The nice programming language’. http://nice.sourceforge.net2005.
    37. 37)
      • D. Hovemeyer , J. Spacco , W. Pugh . Evaluating and tuning a static analysis to find null pointer bugs. SIGSOFT Softw. Eng. Notes , 1 , 13 - 19
    38. 38)
      • Ekman, T.: `Extensible compiler construction', 2006, PhD, CS Deparment, Lund University.
    39. 39)
      • Chalin, P., James, P.R.: `Non-null references by default in Java: Alleviating the nullity annotation burden', Proc 21st European Conf. Object-Oriented Programming (ECOOP), July–August 2007, Berlin, Germany, p. 227–247, (LNCS, 4609).
    40. 40)
      • Park R.: ‘Software size measurement: a framework for counting source statements’. CMU, Software Engineering Institute, Pittsburgh CMU/SEI-92-TR-20, 1992.
    41. 41)
      • Fähndrich, M., Leino, K.R.M.: `Declaring and checking non-null types in an object-oriented language', Proc. 18th annual ACM SIGPLAN Conf. Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA'03, 2003, p. 302–312.
    42. 42)
      • DeLine, R., Leino, K.R.M.: `BoogiePL: a typed procedural language for checking object-oriented programs', Microsoft Research, Technical Report, 2005.
    43. 43)
      • Leavens G.T., Poll E., Clifton C., et al.: ‘JML reference manual’. http://www.jmlspecs.org, 2008.
    44. 44)
      • Evans D.: ‘Splint user manual’. Secure Programming Group, University of Virginia, 5 June 2003.
    45. 45)
      • Fähndrich, M., Leino, K.R.M.: `Non-null types in an object-oriented language', Proc. Workshop on Formal Techniques for Java-like Languages, 2002, Malaga, Spain.
    46. 46)
      • J. Bloch . (2001) Effective Java programming language guide.
    47. 47)
      • Flanagan, C., Leino, K.R.M.: `Houdini, an annotation assistant for ESC/Java', Proc. Int. Symp. Formal Methods Europe, 2001, Berlin, Germany, 2021, p. 500–517.
    48. 48)
    49. 49)
      • ECMA International, ‘Eiffel analysis, design and programming language’, ECMA-367, June 2005.
    50. 50)
      • L. Burdy , Y. Cheon , D.R. Cok . An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. (STTT) , 3 , 212 - 232
    51. 51)
      • Ekman, T., Hedin, G.: `Pluggable non-null types for Java', In Proceeding of TOOLS Europe, 2007, To be Published.
    52. 52)
      • Kiniry, J.R., Morkan, A.E., Fairmichael, F.: `The KOA remote voting system: A summary of work to-date', Proc. Symposium on Trustworthy Global Computing (TGC), 7–9 November 2006, Lucca, Italy, p. 244–262.
    53. 53)
      • Barnett, M., Leino, K.R.M., Schulte, W.: `The Spec# programming system: an overview', ‘Proc. Int. Workshop on the Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS)’, 10–14 March 2004, Marseille, France, (LNCS, 3362).
    54. 54)
      • D. Hovemeyer , W. Pugh . Finding bugs is easy. ACM SIGPLAN Not. , 12 , 92 - 106
    55. 55)
      • Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: `Extended static checking', Compaq Systems Research Center, Research Report 159, 1998.
    56. 56)
      • Chalin, P., James, P.R., Karabotsos, G.: `JML4: towards an industrial grade IVE for java and next generation research platform for JML', Proc. Conf. Verified Software: Theories, Tools, Experiments (VSTTE), 6–9 October 2008, Toronto, Canada.
    57. 57)
      • Lea K.: ‘Nully’. https://nully.dev.java.net, 2005.
    58. 58)
      • J.V. Guttag , J.J. Horning . (1993) Larch: languages and tools for formal specification.
    59. 59)
      • Pugh W.: ‘How do you fix an obvious bug?’, http://findbugs.blogspot.com, 2006.
    60. 60)
      • Leavens G.T.: ‘The Java Modeling Language (JML)’. http://www.jmlspecs.org, 2008.
    61. 61)
    62. 62)
      • Chalin, P., James, P.R., Karabotsos, G.: `An integrated verification environment for JML: architecture and early results', Proc. 6th Int. Workshop on Specification and Verification of Component-Based Systems (SAVCBS), 3–4 September 2007, Cavtat, Croatia, p. 47–53.
    63. 63)
      • J. Gosling , B. Joy , G. Steele , G. Bracha . (2005) The Java Language Specification.
    64. 64)
      • F. Rioux , P. Chalin . Improving the quality of web-based enterprise applications with extended static checking: A case study. Electron. Notes Theor. Comput. Sci. , 2 , 119 - 132
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-sen_20080010
Loading

Related content

content/journals/10.1049/iet-sen_20080010
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading
This is a required field
Please enter a valid email address