nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

JMCTest: Automatically Testing Inter-Method Contracts in Java

verfasst von : Paul Börding, Jan Haltermann, Marie-Christine Jakobs, Heike Wehrheim

Erschienen in: Testing Software and Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Over the years, Design by Contract (DbC) has evolved as a powerful concept for program documentation, testing, and verification. Contracts formally specify assertions on (mostly) object-oriented programs: pre- and postconditions of methods, class invariants, allowed call orders, etc. Missing in the long list of properties specifiable by contracts are, however, method correlations: DbC languages fall short on stating assertions relating methods.

In this paper, we propose the novel concept of inter-method contract, allowing precisely for expressing method correlations. We present JMC as a language for specifying and JMCTest as a tool for dynamically checking inter-method contracts on Java programs. JMCTest fully automatically generates objects on which the contracted methods are called and the validity of the contract is checked. Using JMCTest, we detected that large Java code bases (e.g. JBoss, Java RT) frequently violate standard inter-method contracts. In comparison to other verification tools inspecting (some) inter-method contracts, JMCTest can find bugs that remain undetected by those tools.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Security Testing for Chatbots

Nächstes Kapitel Testing Ambient Assisted Living Solutions with Simulations

An empty sequence is an abbreviation for the one-element sequence true, see contract (1) in Fig. 1.

The number \(n\) is user-configurable.

The ratio of PremiseFF to Runs is a metric indicating how many of the generated tests are relevant for contract checking.

Note that we could have used one parameterized JUnit test instead, but we think our solution simplifies the detection of the contract violating implementations.

Currently, all input variables under test must have the same object type.

http://www.jcheck.org/.

https://github.com/jqno/equalsverifier.

https://pmd.github.io/.

We tested all public classes which did not use Object.equals.

We compare RANDOOP and JMCTest only on the CPAchecker project because RANDOOP failed on Java rt.jar and got stuck on JBoss.

Ahrendt, W., et al.: The KeY platform for verification and analysis of Java programs. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 55–71. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12154-3_4CrossRef

Ayewah, N., Hovemeyer, D., Morgenthaler, J.D., Penix, J., Pugh, W.: Using static analysis to find bugs. IEEE 25(5), 22–29 (2008). https://doi.org/10.1109/MS.2008.130CrossRef

Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30569-9_3CrossRef

Bartetzko, D., Fischer, C., Möller, M., Wehrheim, H.: Jass - Java with assertions. Electr. Notes Theor. Comput. Sci. 55(2), 103–117 (2001). https://doi.org/10.1016/S1571-0661(04)00247-6CrossRef

Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_16CrossRef

Bouquet, F., Dadeau, F., Legeard, B.: Automated boundary test generation from JML specifications. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 428–443. Springer, Heidelberg (2006). https://doi.org/10.1007/11813040_29CrossRef

Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: ISSTA, pp. 123–133. ACM (2002). http://doi.acm.org/10.1145/566172.566191CrossRef

Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: advanced specification and verification with JML and ESC/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342–363. Springer, Heidelberg (2006). https://doi.org/10.1007/11804192_16CrossRef

Chalin, P., Rioux, F.: JML runtime assertion checking: improved error reporting and efficiency using strong validity. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 246–261. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68237-0_18CrossRef

10.

Chen, T.Y., Leung, H., Mak, I.K.: Adaptive random testing. In: Maher, M.J. (ed.) ASIAN 2004. LNCS, vol. 3321, pp. 320–329. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30502-6_23CrossRef

11.

Cheon, Y., Leavens, G.T.: A simple and practical approach to unit testing: the JML and JUnit way. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 231–255. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-47993-7_10CrossRef

12.

Cheon, Y.: Automated random testing to detect specification-code inconsistencies. In: Karras, D. (ed.) Conference on Software Engineering Theory and Practice, pp. 112–119. International Society for Research in Science and Technology (2007)

13.

Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java Modeling Language (JML). In: Conference on Software Engineering Research and Practice, pp. 322–328. CSREA Press (2002)

14.

Cheon, Y., Rubio-Medrano, C.E.: Random test data generation for Java classes annotated with JML specifications. In: Arabnia, H.R., Reza, H. (eds.) Conference on Software Engineering Research and Practice, pp. 385–391. CSREA Press (2007)

15.

Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: ICFP, pp. 268–279. ACM (2000). http://doi.acm.org/10.1145/351240.351266CrossRef

16.

Csallner, C., Smaragdakis, Y.: JCrasher: an automatic robustness tester for Java. Softw. Pract. Exper. 34(11), 1025–1050 (2004). https://doi.org/10.1002/spe.602CrossRef

17.

Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: VCC: contract-based modular verification of concurrent C. In: ICSE, pp. 429–430. IEEE (2009). https://doi.org/10.1109/ICSE-COMPANION.2009.5071046

18.

Enderlin, I., Dadeau, F., Giorgetti, A., Ben Othman, A.: Praspel: a specification language for contract-based testing in PHP. In: Wolff, B., Zaïdi, F. (eds.) ICTSS 2011. LNCS, vol. 7019, pp. 64–79. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24580-0_6CrossRef

19.

Fähndrich, M.: Static verification for code contracts. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 2–5. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15769-1_2CrossRef

20.

Fähndrich, M., Barnett, M., Logozzo, F.: Embedded contract languages. In: SAC, pp. 2103–2110. ACM (2010). http://doi.acm.org/10.1145/1774088.1774531

21.

Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica 10(1), 27–52 (1978). https://doi.org/10.1007/BF00260922MathSciNetCrossRefMATH

22.

Hovemeyer, D., Pugh, W.: Finding bugs is easy. SIGPLAN Not. 39(12), 92–106 (2004). http://doi.acm.org/10.1145/1052883.1052895CrossRef

23.

JUnit: Junit4 (2012–2017). http://junit.org/junit4/

24.

Karaorman, M., Hölzle, U., Bruno, J.: jContractor: a reflective java library to support design by contract. In: Cointe, P. (ed.) Reflection 1999. LNCS, vol. 1616, pp. 175–196. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48443-4_18CrossRef

25.

Keil, M., Thiemann, P.: TreatJS: higher-order contracts for JavaScripts. In: Boyland, J.T. (ed.) ECOOP. LIPIcs, vol. 37, pp. 28–51. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015). https://doi.org/10.4230/LIPIcs.ECOOP.2015.28

26.

Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT Softw. Eng. Notes 31(3), 1–38 (2006). http://doi.acm.org/10.1145/1127878.1127884CrossRef

27.

Lin, Y., Tang, X., Chen, Y., Zhao, J.: A divergence-oriented approach to adaptive random testing of Java programs. In: ASE, pp. 221–232. IEEE (2009). https://doi.org/10.1109/ASE.2009.13

28.

Meyer, B.: Design by contract: the Eiffel method. In: TOOLS, p. 446. IEEE (1998). https://doi.org/10.1109/TOOLS.1998.711043

29.

Oriat, C.: Jartege: a tool for random generation of unit tests for Java classes. In: Reussner, R., Mayer, J., Stafford, J.A., Overhage, S., Becker, S., Schroeder, P.J. (eds.) QoSA/SOQUA -2005. LNCS, vol. 3712, pp. 242–256. Springer, Heidelberg (2005). https://doi.org/10.1007/11558569_18CrossRef

30.

Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: ICSE, pp. 75–84. IEEE Computer Society (2007). http://doi.acm.org/10.1145/1297846.1297902

31.

Ploesch, R.: Design by contract for Python. In: APSEC, pp. 213–219. IEEE (1997). https://doi.org/10.1109/APSEC.1997.640178

32.

Pradel, M., Gross, T.R.: Automatic testing of sequential and concurrent substitutability. In: ICSE, pp. 282–291. IEEE (2013). https://doi.org/10.1109/ICSE.2013.6606574

33.

Tillmann, N., Schulte, W.: Parameterized unit tests. In: FSE, pp. 253–262. ACM (2005). http://doi.acm.org/10.1145/1081706.1081749CrossRef

34.

Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203–232 (2003). https://doi.org/10.1023/A:1022920129859CrossRef

35.

Wegner, P.: The Vienna definition language. ACM Comput. Surv. 4(1), 5–63 (1972). http://doi.acm.org/10.1145/356596.356598MathSciNetCrossRef

36.

Xu, G., Yang, Z.: JMLAutoTest: a novel automated testing framework based on JML and JUnit. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 70–85. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24617-6_6CrossRef

Titel: JMCTest: Automatically Testing Inter-Method Contracts in Java
verfasst von: Paul Börding
Jan Haltermann
Marie-Christine Jakobs
Heike Wehrheim
Verlag: Springer International Publishing
Buch: Testing Software and Systems
Print ISBN: 978-3-319-99926-5

Electronic ISBN: 978-3-319-99927-2

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-99927-2_4

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner