Advertisement

How the Design of JML Accommodates Both Runtime Assertion Checking and Formal Verification

  • Gary T. Leavens
  • Yoonsik Cheon
  • Curtis Clifton
  • Clyde Ruby
  • David R. Cok
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2852)

Abstract

Specifications that are used in detailed design and in the documentation of existing code are primarily written and read by programmers. However, most formal specification languages either make heavy use of symbolic mathematical operators, which discourages use by programmers, or limit assertions to expressions of the underlying programming language, which makes it difficult to write complete specifications. Moreover, using assertions that are expressions in the underlying programming language can cause problems both in runtime assertion checking and in formal verification, because such expressions can potentially contain side effects. The Java Modeling Language, JML, avoids these problems. It uses a side-effect free subset of Java’s expressions to which are added a few mathematical operators (such as the quantifiers ∖forall and ∖exists). JML also hides mathematical abstractions, such as sets and sequences, within a library of Java classes. The goal is to allow JML to serve as a common notation for both formal verification and runtime assertion checking; this gives users the benefit of several tools without the cost of changing notations.

Keywords

Mathematical Notation Mathematical Concept Java Program Java Modeling Language Hash Code 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abraham-Mumm, E., de Boer, F.S., de Roever, W.P., Steffen, M.: A toolsupported proof system for mutlithreaded java. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 1–32. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  2. 2.
    America, P.: Inheritance and subtyping in a parallel object-oriented language. In: Bézivin, J., Hullot, J.-M., Lieberman, H., Cointe, P. (eds.) ECOOP 1987. LNCS, vol. 276, pp. 234–242. Springer, Heidelberg (1987)CrossRefGoogle Scholar
  3. 3.
    America, P.: Designing an object-oriented programming language with behavioural subtyping. In: de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1990. LNCS, vol. 489, pp. 60–90. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  4. 4.
    Barringer, H., Cheng, J.H., Jones, C.B.: A logic covering undefinedness in program proofs. Acta Informatica 21(3), 251–269 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Bartetzko, D., Fischer, C., Moller, M., Wehrheim, H.: Jass - Java with assertions. In: Havelund, K., Rosu, G. (eds.) Workshop on Runtime Verification held in conjunction with the 13th Conference on Computer Aided Verification, CAV 2001. Published in Electronic Notes in Theoretical Computer Science, vol. 55(2) (2001), Available from www.elsevier.nl
  6. 6.
    Bicarregui, J., Fitgerald, J.S., Lindsay, P.A., Moore, R., Ritchie, B.: Proof in VDM: A Practitioner’s Guide. Springer, New York (1994)Google Scholar
  7. 7.
    Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Object Technology Series. Addison Wesley, Reading (1999)Google Scholar
  8. 8.
    Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: Proceedings International Symposium on Software Testing and Analysis (ISSTA), July 2002, pp. 123–133. ACM, New York (2002)CrossRefGoogle Scholar
  9. 9.
    Chalin, P.: Back to basics: Language support and semantics of basic infinite integer types in JML and Larch. Technical Report CU-CS 2002-003.1, Computer Science Department, Concordia University (October 2002)Google Scholar
  10. 10.
    Chalin, P.: Improving JML: For a safer and more effective language. Technical Report 2003-001.1, Computer Science Department, Concordia University (March 2003)Google Scholar
  11. 11.
    Cheon, Y., Leavens, G.T.: The Larch/Smalltalk interface specification language. ACM Transactions on Software Engineering and Methodology 3(3), 221–253 (1994)CrossRefGoogle Scholar
  12. 12.
    Cheon, Y., Leavens, G.T.: A quick overview of Larch/C++. Journal of Object-Oriented Programming 7(6), 39–49 (1994)Google Scholar
  13. 13.
    Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java Modeling Language (JML). In: Arabnia, H.R., Mun, Y. (eds.) Proceedings of the International Conference on Software Engineering Research and Practice (SERP 2002), Las Vegas, Nevada, USA, June 24-27, pp. 322–328. CSREA Press (2002)Google Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    Clifton, C.: MultiJava: Design, implementation, and evaluation of a Javacompatible language supporting modular open classes and symmetric multiple dispatch. Technical Report 01-10, Department of Computer Science, Iowa State University, Ames, Iowa, 50011 (November 2001), Available from http://www.multijava.org
  16. 16.
    Clifton, C., Leavens, G.T., Chambers, C., Millstein, T.: MultiJava: Modular open classes and symmetric multiple dispatch for Java. In: OOPSLA 2000 Conference on Object-Oriented Programming, Systems, Languages, and Applications, October 2000. ACM SIGPLAN Notices, vol. 35(10), pp. 130–145. ACM, New York (2000)Google Scholar
  17. 17.
    Cohen, E.: Programming in the 1990s: An Introduction to the Calculation of Programs. Springer, New York (1990)zbMATHGoogle Scholar
  18. 18.
    Detlefs, D.L., Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: Extended static checking. SRC Research Report 159, Compaq Systems Research Center, 130 Lytton Ave., Palo Alto (December 1998)Google Scholar
  19. 19.
    Dhara, K.K., Leavens, G.T.: Forcing behavioral subtyping through specification inheritance. In: Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany, March 1996, pp. 258–267. IEEE Computer Society Press, Los Alamitos (1996); A corrected version is Iowa State University, Dept. of Computer Science TR #95-20cCrossRefGoogle Scholar
  20. 20.
    Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and program semantics. Springer, NY (1990)zbMATHGoogle Scholar
  21. 21.
    Duncan, A., Holzle, U.: Adding contracts to Java with Handshake. Technical Report TRCS98-32, Department of Computer Science, University of California, Santa Barbara, CA (December 1998)Google Scholar
  22. 22.
    Edwards, S.H., Heym, W.D., Long, T.J., Sitaraman, M., Weide, B.W.: Part II: Specifying components in RESOLVE. ACM SIGSOFT Software Engineering Notes 19(4), 29–39 (1994)CrossRefGoogle Scholar
  23. 23.
    Ernst, M., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering 27(2), 1–25 (2001)CrossRefGoogle Scholar
  24. 24.
    Findler, R.B., Felleisen, M.: Contract soundness for objectoriented languages. In: OOPSLA 2001 Conference Proceedings, Object-Oriented Programming, Systems, Languages, and Applications, Tampa Bay, Florida, USA, October 14-18, pp. 1–15 (2001)Google Scholar
  25. 25.
    Findler, R.B., Latendresse, M., Felleisen, M.: Behavioral contracts and behavioral subtyping. In: Proceedings of Joint 8th European Software Engineering Conference (ESEC) and 9th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE), Vienna, Austria, September 10-14 (2001)Google Scholar
  26. 26.
    Finney, K.: Mathematical notation in formal specification: Too difficult for the masses? IEEE Transactions on Software Engineering 22(2), 158–159 (1996)CrossRefGoogle Scholar
  27. 27.
    Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools in Software Development, Cambridge, UK (1998)Google Scholar
  28. 28.
    Flanagan, C., Rustan, K., Leino, M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Norris, C., Fenwick Jr., J.B. (eds.) Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), June 17-19. SIGPLAN, vol. 37(5), pp. 234–245. ACM Press, New York (2002)CrossRefGoogle Scholar
  29. 29.
    Friendly, L.: The design of distributed hyperlinked programming documentation. In: Fraïssè, S., Garzotto, F., Isakowitz, T., Nanard, J., Nanard, M. (eds.) Proceedings of the International Workshop on Hypermedia Design (IWHD 1995), Montpellier, France, June 1-2, pp. 151–173. Springer, Heidelberg (1995)Google Scholar
  30. 30.
    Gifford, D.K., Lucassen, J.M.: Integrating functional and imperative programming. In: ACM Conference on LISP and Functional Programming, August 1986, pp. 28–38. ACM, New York (1986)Google Scholar
  31. 31.
    Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer, New York (1994)Google Scholar
  32. 32.
    Gries, D., Schneider, F.B.: Avoiding the undefined by underspecification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 366–373. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  33. 33.
    Guttag, J.V., Horning, J.J., Garland, S.J., Jones, K.D., Modet, A., Wing, J.M.: Larch: Languages and Tools for Formal Specification. Springer, New York (1993)zbMATHGoogle Scholar
  34. 34.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–583 (1969)zbMATHCrossRefGoogle Scholar
  35. 35.
    Hoare, C.A.R.: Notes on data structuring. In: Dijkstra, E., Dahl, O.-J., Hoare, C.A.R. (eds.) Structured Programming, pp. 83–174. Academic Press, Inc., New York (1972)Google Scholar
  36. 36.
    Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1(4), 271–281 (1972)zbMATHCrossRefGoogle Scholar
  37. 37.
    Huisman, M.: Reasoning about Java Programs in higher order logic with PVS and Isabelle, February 2001. Ipa dissertation series 2001-03. University of Nijmegen, Holland (2001)Google Scholar
  38. 38.
    Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284–303. Springer, Heidelberg (2000); An earlier version is technical report CSI-R9912CrossRefGoogle Scholar
  39. 39.
    Jackson, D.: Alloy: A lightweight object modeling notation. ACM Transactions on Software Engineering and Methodology 11(2), 256–290 (2002)CrossRefGoogle Scholar
  40. 40.
    Jacobs, B., Kiniry, J., Warnier, M.: Java program verification challenges. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 202–219. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  41. 41.
    Jacobs, B., Poll, E.: A logic for the Java modeling language JML. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 284–299. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  42. 42.
    Jacobs, B., van den Berg, J., Huisman, M., van Berkum, M., Hensel, U., Tews, H.: Reasoning about Java classes (preliminary report). In: OOPSLA 1998 Conference Proceedings, October 1998. ACM SIGPLAN Notices, vol. 33(10), pp. 329–340. ACM, New York (1998)CrossRefGoogle Scholar
  43. 43.
    Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1990)zbMATHGoogle Scholar
  44. 44.
    Jonkers, H.B.M.: Upgrading the pre- and postcondition technique. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 551, pp. 428–456. Springer, Heidelberg (1991)Google Scholar
  45. 45.
    Karaorman, M., Holzle, 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)CrossRefGoogle Scholar
  46. 46.
    Khurshid, S., Marinov, D., Jackson, D.: An analyzable annotation language. In: Proceedings of OOPSLA 2002 Conference on Object-Oriented Programming, Languages, Systems, and Applications, November 2002. SIGPLAN Notices, vol. 37(11), pp. 231–245. ACM, New York (2002)Google Scholar
  47. 47.
    Kramer, R.: iContract – the Java design by contract tool. In: TOOLS 26: Technology of Object-Oriented Languages and Systems, Los Alamitos, California, pp. 295–307 (1998)Google Scholar
  48. 48.
    Lamport, L.: A simple approach to specifying concurrent systems. Communications of the ACM 32(1), 32–45 (1989)CrossRefMathSciNetGoogle Scholar
  49. 49.
    Larman, C.: Applying UML and Patterns: An Introduction to Object-Oriented Analysis and Design and the Unified Process, 2nd edn. Prentice Hall PTR, Upper Saddle River (2002)Google Scholar
  50. 50.
    Leavens, G.T.: An overview of Larch/C++: Behavioral specifications for C++ modules. In: Kilov, H., Harvey, W. (eds.) Specification of Behavioral Semantics in Object-Oriented Information Modeling. ch. 8, pp. 121–142. Kluwer Academic Publishers, Boston (1996); An extended version is TR #96-01d, Department of Computer Science, Iowa State University, Ames, Iowa, 50011CrossRefGoogle Scholar
  51. 51.
    Leavens, G.T.: Larch/C++ Reference Manual. Version 5.41, Available in ftp: http://www.ftp.cs.iastate.edu/pub/larchc++/lcpp.ps.gz or on the World Wide Web at the URL http://www.cs.iastate.edu/~leavens/larchc++.html (April 1999)
  52. 52.
    Leavens, G.T.: Larch frequently asked questions. Version 1.110 (May 2000), Available in http://www.cs.iastate.edu/~leavens/larch-faq.html
  53. 53.
    Leavens, G.T., Baker, A.L.: Enhancing the pre- and postcondition technique for more expressive specifications. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1087–1106. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  54. 54.
    Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175–188. Kluwer Academic Publishers, Boston (1999)Google Scholar
  55. 55.
    Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06v, Iowa State University, Department of Computer Science (May 2003), See http://www.jmlspecs.org
  56. 56.
    Leavens, G.T., Cheon, Y.: Preliminary design of Larch/C++. In: Martin, U., Wing, J. (eds.) Proceedings of the First International Workshop on Larch, July, 1992, Workshops in Computing, pp. 159–184. Springer, New York (1993)Google Scholar
  57. 57.
    Leavens, G.T., Dhara, K.K.: Concepts of behavioral subtyping and a sketch of their extension to component-based systems. In: Leavens, G.T., Sitaraman, M. (eds.) Foundations of Component-Based Systems. ch. 6, pp. 113–135. Cambridge University Press, Cambridge (2000)Google Scholar
  58. 58.
    Leavens, G.T., Leino, K.R.M., Poll, E., Ruby, C., Jacobs, B.: JML: notations and tools supporting detailed design in Java. In: OOPSLA 2000 Companion, Minneapolis, Minnesota, October 2000, pp. 105–106. ACM, New York (2000)Google Scholar
  59. 59.
    Leavens, G.T., Pigozzi, D.: A complete algebraic characterization of behavioral subtyping. Acta Informatica 36, 617–663 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  60. 60.
    Leavens, G.T., Weihl, W.E.: Reasoning about object-oriented programs that use subtypes (extended abstract). In: Meyrowitz, N. (ed.) OOPSLA ECOOP 1990 Proceedings, October 1990. ACM SIGPLAN Notices, vol. 25(10), pp. 212–223. ACM, New York (1990)Google Scholar
  61. 61.
    Leavens, G.T., Weihl, W.E.: Specification and verification of objectoriented programs using supertype abstraction. Acta Informatica 32(8), 705–778 (1995)zbMATHMathSciNetGoogle Scholar
  62. 62.
    Leavens, G.T., Wing, J.M.: Protective interface specifications. Formal Aspects of Computing 10, 59–75 (1998)zbMATHCrossRefGoogle Scholar
  63. 63.
    Leavens, G.T.: Verifying object-oriented programs that use subtypes. Technical Report 439, Massachusetts Institute of Technology, Laboratory for Computer Science, The author’s Ph.D. thesis (February 1989)Google Scholar
  64. 64.
    Rustan, K., Leino, M.: A myth in the modular specification of programs. Technical Report KRML 63, Digital Equipment Corporation, Systems Research Center, 130 Lytton Avenue Palo Alto, CA 94301, Obtain from the author at leino@microsoft.com (November 1995)Google Scholar
  65. 65.
    Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: ESC/Java user’s manual. Technical note, Compaq Systems Research Center (October 2000)Google Scholar
  66. 66.
    Rustan, K., Leino, M., Saxe, J.B., Stata, R.: Checking Java programs via guarded commands. Technical Note 1999-002, Compaq Systems Research Center, Palo Alto, CA (May 1999)Google Scholar
  67. 67.
    Lieberherr, K., Orleans, D., Ovlinger, J.: Aspect-oriented programming with adaptive methods. Communications of the ACM 44(10), 39–41 (2001)CrossRefGoogle Scholar
  68. 68.
    Liskov, B., Guttag, J.: Abstraction and Specification in Program Development. The MIT Press, Cambridge (1986)zbMATHGoogle Scholar
  69. 69.
    Liskov, B., Wing, J.: A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems 16(6), 1811–1841 (1994)CrossRefGoogle Scholar
  70. 70.
    Meyer, B.: Eiffel: The Language. Object-Oriented Series. Prentice Hall, New York (1992)zbMATHGoogle Scholar
  71. 71.
    Meyer, B.: Object-oriented Software Construction, 2nd edn. Prentice Hall, New York (1997)zbMATHGoogle Scholar
  72. 72.
    Nimmer, J.W., Ernst, M.D.: Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java. In: Proceedings of RV 2001, First Workshop on Runtime Verification. Elsevier, Amsterdam (July 2001); To appear in Electronic Notes in Theoretical Computer ScienceGoogle Scholar
  73. 73.
    Ogden, W.F., Sitaraman, M., Weide, B.W., Zweben, S.H.: Part I: The RESOLVE framework and discipline — a research synopsis. ACM SIGSOFT Software Engineering Notes 19(4), 23–28 (1994)CrossRefGoogle Scholar
  74. 74.
    International Standards Organization. Information technology – programming languages, their environments and system software interfaces – Vienna Development Method – specification language – part 1: Base language. ISO/IEC 13817-1 (December 1996)Google Scholar
  75. 75.
    Parasoft Corporation. Using design by contract TM to automate Java TM software and component testing, Available from http://www.parasoft.com/jsp/products/tech_papers.jsp?product=Jcontract (as of February 2003)
  76. 76.
    Raghavan, A.D., Leavens, G.T.: Desugaring JML method specifications. Technical Report 00-03c, Iowa State University, Department of Computer Science (August 2001)Google Scholar
  77. 77.
    Rosenblum, D.S.: Towards a method of programming with assertions. In: Proceedings of the 14th International Conference on Software Engineering, May 1992, pp. 92–104 (1992)Google Scholar
  78. 78.
    Ruby, C., Leavens, G.T.: Safely creating correct subclasses without seeing superclass code. In: OOPSLA 2000 Conference on Object-Oriented Programming, Systems, Languages, and Applications, Minneapolis, Minnesota, October 2000. ACM SIGPLAN Notices, vol. 35(10), pp. 208–228 (2000)Google Scholar
  79. 79.
    Spivey, J.: An introduction to Z and formal specifications. Software Engineering Journal (January 1989)Google Scholar
  80. 80.
    Spivey, J.M.: The Z Notation: A Reference Manual. International Series in Computer Science. Prentice-Hall, New York (1989) ISBN 013983768XzbMATHGoogle Scholar
  81. 81.
    Talpin, J.-P., Jouvelot, P.: The type and effect discipline. Information and Computation 111(2), 245–296 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  82. 82.
    Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modeling with UML. Addison Wesley, Reading (1999)Google Scholar
  83. 83.
    Warmer, J., Kleppe, A.: OCL: The constraint language of the UML. Journal of Object-Oriented Programming 12(1), 10–13, 28 (1999)Google Scholar
  84. 84.
    Wills, A.: Capsules and types in Fresco: Program validation in Smalltalk. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 59–76. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  85. 85.
    Wing, J.M.: Writing Larch interface language specifications. ACM Transactions on Programming Languages and Systems 9(1), 1–24 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  86. 86.
    Wing, J.M.: A two-tiered approach to specifying programs. Technical Report TR-299, Massachusetts Institute of Technology, Laboratory for Computer Science (1983)Google Scholar
  87. 87.
    Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Gary T. Leavens
    • 1
  • Yoonsik Cheon
    • 1
  • Curtis Clifton
    • 1
  • Clyde Ruby
    • 1
  • David R. Cok
    • 2
  1. 1.Department of Computer ScienceIowa State UniversityAmesUSA
  2. 2.Eastman Kodak Company Research & Development LaboratoriesRochesterUSA

Personalised recommendations