Advertisement

Practical Void Safety

  • Alexander KogtenkovEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10712)

Abstract

Null pointer dereferencing remains one of the major issues in modern object-oriented languages. An obvious addition of keywords to distinguish between never null and possibly null references appears to be insufficient during object initialization when some fields declared as never null may be temporary null before the initialization completes. Unlike all previous publications on the subject, this work avoids explicit encoding of these intermediate states in programs in favor of statically checked validity rules that do not depend on special conditionally non-null types. I review all object initialization examples proposed earlier and I suggest new ones to compare applicability of different approaches. I demonstrate the usability of the proposed scheme on open-source libraries with a million lines of code that were converted to satisfy the rules.

Keywords

Null pointer dereferencing Null safety Void safety Object initialization Static analysis Library-level modularity 

References

  1. 1.
    Arnout, K., Meyer, B.: Finding implicit contracts in .NET components. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 285–318. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-39656-7_12. ISBN: 978-3-540-39656-7CrossRefGoogle Scholar
  2. 2.
    Barnett, M., Fähndrich, M., Leino, K.R.M., Müller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Commun. ACM 54(6), 81–91 (2011)CrossRefGoogle Scholar
  3. 3.
    Bray, T., Paoli, J., Sperberg-McQueen, C.M., Maler, E., Yergeau, F.: Extensible Markup Language (XML) 1.0 (Fifth Edition). Fifth Edition of a Recommendation. W3C (2008). http://www.w3.org/TR/2008/REC-xml-20081126/
  4. 4.
    Fähndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: Proceedings of the 18th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2003, Anaheim, California, USA, pp. 302–312. ACM (2003)Google Scholar
  5. 5.
    Fähndrich, M., Xia, S.: Establishing object invariants with delayed types. In: Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems and Applications, OOPSLA 2007, Montreal, Quebec, Canada, pp. 337–350. ACM (2007)Google Scholar
  6. 6.
    Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, PLDI 2002, Berlin, Germany, pp. 234–245. ACM (2002)Google Scholar
  7. 7.
    Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-oriented Software. Addison-Wesley Longman Publishing Co., Inc., Boston (1995)zbMATHGoogle Scholar
  8. 8.
    Hoare, T.: Null references: the billion dollar mistake. Presentation at QCon London (2009)Google Scholar
  9. 9.
    ISO: ISO/IEC 25436:2006(E): Information technology — Eiffel: Analysis, Design and Programming Language. ISO (International Organization for Standardization) and IEC (International Electrotechnical Commission), Geneva, Switzerland (2006)Google Scholar
  10. 10.
    JetBrains: Kotlin Language Specification (2017). https://jetbrains.github.io/kotlin-spec/kotlin-spec.pdf. Accessed 31 Jan 2017
  11. 11.
    Kogtenkov, A.: Mechanically proved practical local null safety. Proc. Inst. Syst. Program. RAS 28(5), 27–54 (2016)CrossRefGoogle Scholar
  12. 12.
    Leino, K.R.M.: Data groups: specifying the modification of extended state. In: Proceedings of the 13th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA 1998, Vancouver, British Columbia, Canada, pp. 144–153. ACM (1998)Google Scholar
  13. 13.
    Mediator pattern (2016). https://en.wikipedia.org/wiki/Mediator_pattern. Accessed 23 Dec 2016
  14. 14.
    Meyer, B.: Targeted expressions: safe object creation with void safety (2012). http://se.ethz.ch/~meyer/publications/online/targeted.pdf. Accessed 8 May 2017
  15. 15.
    Pearce, D.J.: On flow-sensitive types in whiley (2010). http://whiley.org/2010/09/22/on-flow-sensitive-types-in-whiley/. Accessed 7 May 2017
  16. 16.
    Qi, X., Myers, A.C.: Masked types for sound object initialization. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, pp. 53–65. ACM (2009)Google Scholar
  17. 17.
    Spoto, F.: Precise null-pointer analysis. Softw. Syst. Model. 10(2), 219–252 (2011)CrossRefGoogle Scholar
  18. 18.
    Stata, R.: ESCJ 2: improving the safety of Java (1995). http://kindsoftware.com/products/opensource/ESCJava2/ESCTools/docs/design-notes/escj02.html. Accessed 27 Apr 2017
  19. 19.
    Summers, A.J., Müller, P.: Freedom before commitment. Simple flexible initialisation for non-full types. Technical report 716, Zurich, Switzerland: ETH Zurich, Department of Computer Science (2010)Google Scholar
  20. 20.
    Summers, A.J., Müller, P.: Freedom before commitment: a lightweight type system for object initialisation. In: Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2011, Portland, Oregon, USA, pp. 1013–1032. ACM (2011)Google Scholar
  21. 21.
    Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2–3), 167–187 (1996)CrossRefGoogle Scholar
  22. 22.
    Wu, J., Hu, G., Tang, Y., Yang, J.: Effective dynamic detection of alias analysis errors. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2013, Saint Petersburg, Russia, pp. 279–289. ACM (2013)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Independent scientistPodolskRussia

Personalised recommendations