Document Open Access Logo

Contracts in the Wild: A Study of Java Programs

Authors Jens Dietrich, David J. Pearce, Kamil Jezek, Premek Brada

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2017.9.pdf
  • Filesize: 0.6 MB
  • 29 pages

Document Identifiers

Author Details

Jens Dietrich
David J. Pearce
Kamil Jezek
Premek Brada

Cite AsGet BibTex

Jens Dietrich, David J. Pearce, Kamil Jezek, and Premek Brada. Contracts in the Wild: A Study of Java Programs. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 9:1-9:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ECOOP.2017.9

Abstract

The use of formal contracts has long been advocated as an approach to develop programs that are provably correct. However, the reality is that adoption of contracts has been slow in practice. Despite this, the adoption of lightweight contracts — typically utilising runtime checking — has progressed. In the case of Java, built-in features of the language (e.g. assertions and exceptions) can be used for this. Furthermore, a number of libraries which facilitate contract checking have arisen. In this paper, we catalogue 25 techniques and tools for lightweight contract checking in Java, and present the results of an empirical study looking at a dataset extracted from the 200 most popular projects found on Maven Central, constituting roughly 351,034 KLOC. We examine (1) the extent to which contracts are used and (2) what kind of contracts are used. We then investigate how contracts are used to safeguard code, and study problems in the context of two types of substitutability that can be guarded by contracts: (3) unsafe evolution of APIs that may break client programs and (4) violations of Liskovs Substitution Principle (LSP) when methods are overridden. We find that: (1) a wide range of techniques and constructs are used to represent contracts, and often the same program uses different techniques at the same time; (2) overall, contracts are used less than expected, with significant differences between programs; (3) projects that use contracts continue to do so, and expand the use of contracts as they grow and evolve; and, (4) there are cases where the use of contracts points to unsafe subtyping (violations of Liskov's Substitution Principle) and unsafe evolution.
Keywords
  • verification
  • design-by-contract
  • assertions
  • preconditions
  • postconditions
  • runtime checking
  • java
  • input validation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Apache commons lang. Accessed 12 August 2016. URL: https://commons.apache.org.
  2. C4J - DBC for Java. Accessed 12 August 2016. URL: https://sourceforge.net/projects/c4j/.
  3. chex4j. Accessed 12 August 2016. URL: https://sourceforge.net/projects/chex4j/.
  4. cofoja. Accessed 12 August 2016. URL: https://github.com/nhatminhle/cofoja.
  5. Design by contract. Accessed 12 August 2016. URL: http://c2.com/cgi/wiki?DesignByContract.
  6. Google core libraries for java 6+. Accessed 12 August 2016. URL: https://github.com/google/guava.
  7. Hamcrest. Accessed 12 August 2016. URL: http://hamcrest.org/.
  8. Hibernate validator. Accessed 12 August 2016. URL: http://hibernate.org/validator/.
  9. Java parser. Accessed 12 August 2016. URL: http://javaparser.org/.
  10. javadbc. Accessed 12 August 2016. URL: https://www.openhub.net/p/javadbc.
  11. Oval - object validation framework for java. Accessed 12 August 2016. URL: http://oval.sourceforge.net/.
  12. Spring framework. Accessed 12 August 2016. URL: http://spring.io/.
  13. Valid4j. Accessed 12 August 2016. URL: http://www.valid4j.org/.
  14. Code contracts, 2008. URL: https://www.microsoft.com/en-us/research/project/code-contracts/.
  15. Wladimir Araujo, Lionel C. Briand, and Yvan Labiche. On the effectiveness of contracts as test oracles in the detection and diagnosis of functional faults in concurrent object-oriented software. IEEE Transactions on Software Engineering, 40(10):971-992, 2014. Google Scholar
  16. Karine Arnout and Bertrand Meyer. Finding implicit contracts in.NET components. In Proceedings of the Formal Methods for Components and Objects (FMCO), volume 2852 of LNCS, pages 285-318. Springer-Verlag, 2002. Google Scholar
  17. J. Barnes. High Integrity Ada: The SPARK Approach. Addison Wesley Longman, Inc., 1997. Google Scholar
  18. M. Barnett, M. Fähndrich, K. R. M. Leino, P. Müller, W. Schulte, and H. Venter. Specification and verification: the Spec# experience. Communications of the ACM, 54(6):81-91, 2011. Google Scholar
  19. Mike Barnett, Robert De ine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 3(6):27-56, 2004. Google Scholar
  20. Detlef Bartetzko, Clemens Fischer, Michael Möller, and Heike Wehrheim. Jass—Java with assertions. Electronic Notes in Theoretical Computer Science, 55(2):103-117, 2001. Google Scholar
  21. Jaroslav Bauml and Premek Brada. Automated Versioning in OSGi: a Mechanism for Component Software Consistency Guarantee. In Proceedings of the Conference on Software Engineering and Advanced Applications (SEAA), pages 428-435, 2009. Google Scholar
  22. Emmanual Bernard. Jsr 349: Bean validation 1.1, 2013. URL: http://beanvalidation.org/1.1/.
  23. Emmanuel Bernard and Steve Peterson. Jsr 303: Bean validation, 2009. URL: http://beanvalidation.org/1.0/.
  24. Antoine Beugnard, Jean-Marc Jézéquel, Noël Plouzeau, and Damien Watkins. Making Components Contract Aware. Computer, 32(7):38-45, 1999. Google Scholar
  25. Stephen M Blackburn, Robin Garner, Chris Hoffmann, Asjad M Khang, Kathryn S McKinley, Rotem Bentzur, Amer Diwan, Daniel Feinberg, Daniel Frampton, Samuel Z Guyer, et al. The DaCapo benchmarks: Java benchmarking development and analysis. In Proceedings of the ACM conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), number 10, pages 169-190. ACM, 2006. Google Scholar
  26. Joshua Bloch. Effective Java. Pearson Education, 2008. Google Scholar
  27. J. Bowen and M. Hinchey. Ten commandments of Formal Methods... ten years later. IEEE Computer, 39(1):40-48, 2006. Google Scholar
  28. Carl Brandon and Peter Chapin. A SPARK/Ada CubeSat control program. In Proceedings of the Conference on Reliable Software Technologies (RST), pages 51-64, 2013. Google Scholar
  29. Eric Bruneton, Thierry Coupaye, Matthieu Leclercq, Vivien Quéma, and Jean Stefani. The fractal component model and its support in Java. Software: Practice and Experience, 36:1257-1284, 2006. Google Scholar
  30. Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overview of JML tools and applications. Electronic Notes in Computer Science, 80:75-91, 2003. Google Scholar
  31. Casey Casalnuovo, Premkumar T. Devanbu, Vladimir Filkov, and Baishakhi Ray. Replication of assert use in github projects. Technical report, 2015. Google Scholar
  32. Casey Casalnuovo, Premkumar T. Devanbu, Abilio Oliveira, Vladimir Filkov, and Baishakhi Ray. Assert use in github projects. In Proceedings of the International Conference of Software Engineering (ICSE), pages 755-766. IEEE Computer Society Press, 2015. Google Scholar
  33. Néstor Cataño and Marieke Huisman. Formal specification and static checking of Gemplus' electronic purse using ESC/Java. In Proceedings of the Symposium on Formal Methods Europe (FME), volume 2391 of LNCS, pages 272-289. Springer-Verlag, 2002. Google Scholar
  34. Patrice Chalin. Are practitioners writing contracts? In Rigorous Development of Complex Fault-Tolerant Systems [FP6 IST-511599 RODIN project], pages 100-113, 2006. Google Scholar
  35. Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll. Beyond assertions: Advanced specification and verification with JML and ESC/Java2. In Symposium on Formal Methods for Components and Objects (FMCO), pages 342-363, 2005. Google Scholar
  36. Patrice Chalin and Frédéric Rioux. JML runtime assertion checking: Improved error reporting and efficiency using strong validity. In Proceedings of the Symposium on Formal Methods (FM), volume 5014 of LNCS, pages 246-261. Springer-Verlag, 2008. Google Scholar
  37. Roderick Chapman and Florian Schanda. Are we there yet? 20 years of industrial theorem proving with SPARK. In Proceedings of the Conference on Interactive Theorem Proving (ITP), pages 17-26, 2014. Google Scholar
  38. Y. Cheon and G. T. Leavens. A simple and practical approach to unit testing: The JML and JUnit way. In Proceedings of the European Confereince on Object-Oriented Programming (ECOOP), pages 231-255, 2002. Google Scholar
  39. L. A. Clarke and D. S. Rosenblum. A historical perspective on runtime assertion checking in software development. ACM Software Engineering Notes, 31(3):25-37, 2006. Google Scholar
  40. David R. Cok. OpenJML: JML for Java 7 by extending OpenJDK. In Proceedings of the NASA Formal Methods Symposium (NFM), volume 6617 of LNCS, pages 472-479. Springer-Verlag, 2011. Google Scholar
  41. David R. Cok. OpenJML: Software verification for Java 7 using JML, OpenJDK, and eclipse. In Proceedings of the Workshop on Formal Integrated Development Environment (F-IDE), volume 149, pages 79-92, 2014. Google Scholar
  42. David R. Cok and Joseph Kiniry. ESC/Java2: Uniting ESC/Java and JML. In Proceedings of the Conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS), volume 3362 of LNCS, pages 108-128. Springer-Verlag, 2005. Google Scholar
  43. P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-C: A Software Analysis Perspective. In Proceedings of the Conference on Software Engineering and Formal Methods (SEFM), pages 233-247. 2012. Google Scholar
  44. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Proceedings of the conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 337-340, 2008. Google Scholar
  45. David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. SRC Research Report 159, Compaq Systems Research Center, 1998. Google Scholar
  46. L. Peter Deutsch. An interactive program verifier. Ph.D., 1973. Google Scholar
  47. Jens Dietrich and Graham Jenson. Components, contracts and vocabularies-making dynamic component assemblies more predictable. Journal of Object Technology, 8(7):131-148, 2009. Google Scholar
  48. Jens Dietrich, Kamil Jezek, and Premek Brada. Broken promises: An empirical study into evolution problems in Java programs caused by library upgrades. In Proceedings of the Conference on Software Maintenance, Reengineering and Reverse Engineering (CSMR-WCRE), pages 64-73. IEEE Computer Society Press, 2014. Google Scholar
  49. Jens Dietrich and Lucia Stewart. Component contracts in Eclipse - A case study. In Proceedings of the Symposium on Component-Based Software Engineering (CBSE), volume 6092, pages 150-165, 2010. Google Scholar
  50. C. Dross, P. Efstathopoulos, D. Lesens, D. Mentre, and Y. Moy. Rail, space, security: Three case studies for SPARK 2014. In Proceedings of the Embedded Real Time Software And Systems (ERTS), 2014. Google Scholar
  51. Oliver Enseling. icontract: Design by contract in Java. Accessed 12 August 2016. URL: http://www.javaworld.com/article/2074956/learn-java/icontract--design-by-contract-in-java.html.
  52. Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz, and Chen Xiao. The Daikon system for dynamic detection of likely invariants. Science of Computer Programming, 69(1-3):35-45, 2007. Google Scholar
  53. H.-Christian Estler, Carlo A. Furia, Martin Nordio, Marco Piccioni, and Bertrand Meyer. Contracts in practice. In Proceedings of the Symposium on Formal Methods (FM), volume 8442 of LNCS, pages 230-246. Springer-Verlag, 2014. Google Scholar
  54. H.-Christian Estler, Marco Piccioni, Carlo A. Furia, Martin Nordio, and Bertrand Meyer. How specifications change and why you should care. Computing Research Repository (CoRR), abs/1211.4775, 2012. Google Scholar
  55. Manuel Fähndrich, Michael Barnett, and Francesco Logozzo. Embedded contract languages. In Proceedings of the Symposium on Applied Computing (SAC), pages 2103-2110. ACM, 2010. Google Scholar
  56. J. Filliâtre and A. Paskevich. Why3 - where programs meet provers. In Proceedings of the European Symposium on Programming (ESOP), pages 125-128, 2013. Google Scholar
  57. C. Flanagan, K. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In Proceedings of the ACM conference on Programming Language Design and Implementation (PLDI), pages 234-245, 2002. Google Scholar
  58. R. W. Floyd. Assigning meaning to programs. In Proceedings of Symposia in Applied Mathematics, volume 19, pages 19-31. American Mathematical Society, 1967. Google Scholar
  59. Erich Gamma and Kent Beck. Contributing to Eclipse: principles, patterns, and plug-ins. Addison-Wesley Professional, 2004. Google Scholar
  60. Olga Goloshchapova and Markus Lumpe. On the application of inequality indices in comparative software analysis. In Proceedings of the Australasian Software Engineering Conference (ASWEC), pages 117-126. IEEE, 2013. Google Scholar
  61. D. I. Good. Mechanical proofs about computer programs. In Mathematical logic and programming languages, pages 55-75, 1985. Google Scholar
  62. Alwyn E. Goodloe, César Muñoz, Florent Kirchner, and Loïc Correnson. Verification of numerical programs: From real numbers to floating point numbers. In Proceedings of the NASA Formal Methods Symposium (NFM), pages 441-446, 2013. Google Scholar
  63. C. A. R. Hoare. Assertions: A personal perspective. IEEE Annals of the History of Computing, 25(2):14-25, 2003. Google Scholar
  64. C.A.R. Hoare. The verifying compiler: A grand challenge for computing research. Journal of the ACM, 50(1):63-69, 2003. Google Scholar
  65. Charles Antony Richard Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580, 1969. Google Scholar
  66. Ashlie B. Hocking, John C. Knight, M. Anthony Aiello, and Shinichi Shiraishi. Arguing software compliance with ISO 26262. In Proceedings of the Symposium on Software Reliability Engineering (ISSRE), pages 226-231. IEEE Computer Society, 2014. Google Scholar
  67. Richard C. Holt, Philip A. Matthews, J. Alan Rosselet, and James R. Cordy. The Turing Programming Language. Design and Definition. Prentice Hall, 1988. Google Scholar
  68. B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens. Verifast: A powerful, sound, predictable, fast verifier for C and Java. In Proceedings of the NASA Formal Methods Symposium (NFM), pages 41-55, 2011. Google Scholar
  69. B. Jacobs, J. Smans, and F. Piessens. A quick tour of the verifast program verifier. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS), pages 304-311, 2010. Google Scholar
  70. T. J. Jennings and B. A. Carré. A subset of Ada for formal verification (SPARK). Ada User, 9(Supplement):121-126, 1989. Google Scholar
  71. Murat Karaorman, Urs Hölzle, and John Bruno. jContractor: A reflective Java library to support design by contract. In Proc. REFLECTION, pages 175-196, 1999. Google Scholar
  72. Gregor Kiczales, John Lamping, Anurag Mendhekar, Chris Maeda, Cristina Lopes, Jean-Marc Loingtier, and John Irwin. Aspect-oriented programming. In Proceedings of the European Confereince on Object-Oriented Programming (ECOOP), pages 220-242, 1997. Google Scholar
  73. Michael Kimberlin. Reducing boilerplate code with project lombok. URL: http://jnb.ociweb.com/jnb/jnbJan2010.html.
  74. S. King. A Program Verifier. PhD thesis, Carnegie-Mellon University, 1969. Google Scholar
  75. 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, 55(1-3):185-208, March 2005. Google Scholar
  76. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Proceedings of the Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), volume 6355 of LNCS, pages 348-370. Springer-Verlag, 2010. Google Scholar
  77. K. Rustan M. Leino. Developing verified programs with Dafny. In Proceedings of the Conference on Verified Software: Theories, Tools, Experiments (VSTTE), volume 7152 of LNCS, pages 82-82. Springer-Verlag, 2012. Google Scholar
  78. D. Luckham, SM German, F. von Henke, R. Karp, P. Milne, D. Oppen, W. Polak, and W. Scherlis. Stanford Pascal Verifier user manual. Technical Report CS-TR-79-731, Stanford University, Department of Computer Science, 1979. Google Scholar
  79. B. Meyer. Eiffel: A language and environment for software engineering. Journal of Systems and Software, 8(3):199-246, 1988. Google Scholar
  80. B. Meyer. Applying 'design by contract'. Computer, 25(10):40-51, 1992. Google Scholar
  81. Emerson Murphy-Hill and Dan Grossman. How programming languages will co-evolve with software engineering: a bright decade ahead. In Proceedings of the on Future of Software Engineering (FOSE). ACM, 2014. Google Scholar
  82. Peter Naur. Proof of algorithms by general snapshots. BIT Numerical Mathematics, 6, 1966. Google Scholar
  83. Matthew M Papi, Mahmood Ali, Telmo Luis Correa Jr, Jeff H Perkins, and Michael D Ernst. Practical pluggable types for Java. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), pages 201-212, 2008. Google Scholar
  84. D. J. Pearce and L. Groves. Whiley: a platform for research in software verification. In Proceedings of the Conference on Software Language Engineering (SLE), pages 238-248, 2013. Google Scholar
  85. D. J. Pearce and L. Groves. Designing a verifying compiler: Lessons learned from developing whiley. Science of Computer Programming, 113(2):191-220, 2015. Google Scholar
  86. Yu Pei, Carlo A. Furia, Martin Nordio, Yi Wei, Bertrand Meyer, and Andreas Zeller. Automated fixing of programs with contracts. IEEE Transactions on Software Engineering, 40(5):427-449, 2014. Google Scholar
  87. Frantisek Plasil and Stanislav Visnovsky. Behavior protocols for software components. IEEE transactions on Software Engineering, 28(11):1056-1076, 2002. Google Scholar
  88. N. Polikarpova, C. Furia, Y. Pei, Y. Wei, and B. Meyer. What good are strong specifications? In Proceedings of the International Conference of Software Engineering (ICSE), pages 262-271, 2013. Google Scholar
  89. Tom Preston-Werner. Semantic versioning 2.0.0. Accessed 12 August 2016. URL: http://semver.org/.
  90. William Pugh. Jsr305: Annotations for software defect detection, 2013. URL: https://jcp.org/en/jsr/detail?id=305.
  91. S. Raemaekers, A. van Deursen, and J. Visser. Semantic versioning versus breaking changes: A study of the Maven repository. In Proceedings of the Working Conference on Source Code Analysis &Manipulation, pages 215-224. IEEE Computer Society Press, 2014. Google Scholar
  92. David S. Rosenblum. A practical approach to programming with assertions. IEEE Transactions on Software Engineering, 21(1):19-31, 1995. Google Scholar
  93. José Sánchez and Gary T. Leavens. Static verification of PtolemyRely programs using OpenJML. In Proceedings of the Workshop on Foundations of Aspect-Oriented Languages (FOAL), pages 13-18. ACM Press, 2014. Google Scholar
  94. Todd W. Schiller, Kellen Donohue, Forrest Coward, and Michael D. Ernst. Case studies and tools for contract specifications. In Proceedings of the International Conference of Software Engineering (ICSE), pages 596-607, 2014. Google Scholar
  95. Kavir Shrestha and Matthew J. Rutherford. An empirical evaluation of assertions as oracles. In ICST, pages 110-119. IEEE Computer Society Press, 2011. Google Scholar
  96. Clemens Szyperski. Component Software, Second Edition. ACM Press, Addison-Wesley, 2002. Google Scholar
  97. Ewan Tempero, Craig Anslow, Jens Dietrich, Ted Han, Jing Li, Markus Lumpe, Hayden Melton, and James Noble. The Qualitas Corpus: A curated collection of Java code for empirical studies. In Asia Pacific Software Engineering Conference (APSEC), pages 336-345. IEEE, 2010. Google Scholar
  98. The OSGi Alliance. OSGi service platform, 2012. Release 4.3. Google Scholar
  99. Jeffrey M. Voas and Keith W. Miller. Putting assertions in their place. In Proceedings of the Symposium on Software Reliability Engineering (ISSRE), pages 152-157, 1994. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact