Skip to main content
SpringerLink
Log in

JML’s Rich, Inherited Specifications for Behavioral Subtypes

  • Conference paper
Formal Methods and Software Engineering (ICFEM 2006)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4260))

Included in the following conference series:

Abstract

The Java Modeling Language (JML) is used to specify detailed designs for Java classes and interfaces. It has a particularly rich set of features for specifying methods. This paper describes those features, with particular emphasis on the features related to specification inheritance. It shows how specification inheritance in JML forces behavioral subtyping, through a discussion of semantics and examples. It also describes a notion of modular reasoning based on static type information, supertype abstraction, which is made valid in JML by methodological restrictions on invariants, history constraints, and initially clauses and by behavioral subtyping.

This work was supported by NSF grant CCF-0429567.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Software and System Modeling 4, 32–54 (2005)

    Article  Google Scholar 

  2. Alagic, S., Kouznetsova, S.: Behavioral compatibility of self-typed theories. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 585–608. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004), http://tinyurl.com/m2a8j

    Article  Google Scholar 

  6. Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Transactions on Software Engineering 21(10), 785–798 (1995)

    Article  Google Scholar 

  7. Bruce, K., Cardelli, L., Castagna, G., Group, T.H.O., Leavens, G.T., Pierce, B.: On binary methods. Theory and Practice of Object Systems 1(3), 221–242 (1995)

    Google Scholar 

  8. Büchi, M., Weck, W.: The greybox approach: When blackbox specifications hide too much. Technical Report 297, Turku Center for Computer Science (August 1999), http://www.abo.fi/~mbuechi/publications/TR297.html

  9. Burdy, L., Requet, A., Lanet, J.-L.: Java applet correctness: a developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 422–439. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  10. Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT) 7(3), 212–232 (2005)

    Google Scholar 

  11. Cataño, N., Huisman, M.: Formal specification of Gemplus’s electronic purse case study. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 272–289. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  12. 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), http://tinyurl.com/o4nxa

    Chapter  Google Scholar 

  13. Chen, Y., Cheng, B.H.C.: A semantic foundation for specification matching. In: Leavens, G.T., Sitaraman, M. (eds.) Foundations of Component-Based Systems, pp. 91–109. Cambridge University Press, New York (2000)

    Google Scholar 

  14. Cheon, Y.: A runtime assertion checker for the Java Modeling Language. Technical Report 03-09, Department of Computer Science, Iowa State University, Ames, IA, The author’s Ph.D. dissertation (April 2003), ftp://ftp.cs.iastate.edu/pub/techreports/TR03-09/TR.pdf

  15. 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)

    Chapter  Google Scholar 

  16. 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), ftp://ftp.cs.iastate.edu/pub/techreports/TR02-05/TR.pdf

  17. Cheon, Y., Leavens, G.T.: The Larch/Smalltalk interface specification language. ACM Transactions on Software Engineering and Methodology 3(3), 221–253 (1994)

    Article  Google Scholar 

  18. Cheon, Y., Leavens, G.T., Sitaraman, M., Edwards, S.: Model variables: Cleanly supporting abstraction in design by contract. Software—Practice and Experience 35(6), 583–599 (2005)

    Article  Google Scholar 

  19. Cook, W.R.: Interfaces and specifications for the Smalltalk-80 collection classes. ACM SIGPLAN Notices, 27(10), 1–15 (1992); Paepcke, A. (ed.) OOPSLA 1992 Proceedings (1992)

    Google Scholar 

  20. Dhara, K.K.: Behavioral subtyping in object-oriented languages. Technical Report TR97-09, Department of Computer Science, Iowa State University, 226 Atanasoff Hall, Ames IA 50011-1040. The author’s Ph.D. dissertation (May 1997)

    Google Scholar 

  21. Dhara, K.K., Leavens, G.T.: Preventing cross-type aliasing for more practical reasoning. Technical Report 01-02a, Department of Computer Science, Iowa State University, Ames, Iowa, 50011 (November 2001), available from archives.cs.iastate.edu , ftp://ftp.cs.iastate.edu/pub/techreports/TR01-02/TR.pdf

  22. Dhara, K.K., Leavens, G.T.: Weak behavioral subtyping for types with mutable objects. In: Brookes, S., Main, M., Melton, A., Mislove, M. (eds.) Mathematical Foundations of Programming Semantics, Eleventh Annual Conference. Electronic Notes in Theoretical Computer Science, vol. 1. Elsevier, Amsterdam (1995), available from: http://www.sciencedirect.com/science/journal/15710661

    Google Scholar 

  23. Dhara, K.K., Leavens, G.T.: Forcing behavioral subtyping through specification inheritance. In: Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany, pp. 258–267. IEEE Computer Society Press, Los Alamitos (March 1996), A corrected version is ISU CS TR #95-20c, http://tinyurl.com/s2krg

    Chapter  Google Scholar 

  24. Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology (JOT) 4(8), 5–32 (2005), http://www.jot.fm/issues/issue_2005_10/article1.pdf

    Article  Google Scholar 

  25. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Inc., Englewood Cliffs (1976)

    MATH  Google Scholar 

  26. 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)

    Article  Google Scholar 

  27. 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), 99–123 (2001)

    Article  Google Scholar 

  28. Findler, R.B., Felleisen, M.: Contract soundness for object-oriented 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 

  29. 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), June  17–19. SIGPLAN, vol. 37(5), pp. 234–245. ACM Press, New York (2002)

    Chapter  Google Scholar 

  30. Guttag, J.V., Horning, J.J., Garland, S., Jones, K., Modet, A., Wing, J.: Larch: Languages and Tools for Formal Specification. Springer, New York (1993)

    MATH  Google Scholar 

  31. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–583 (1969)

    Article  MATH  Google Scholar 

  32. Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1(4), 271–281 (1972)

    Article  MATH  Google Scholar 

  33. Jacobs, B., Poll, E.: Java program verification at Nijmegen: Developments and perspective. Technical Report NIII-R0318, Computing Science Institute, University of Nijmegen (2003), http://www.cs.kun.nl/research/reports/full/NIII-R0318.ps.gz

  34. 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. ACM SIGPLAN Notices, vol. 33(10), pp. 329–340. ACM, New York (1998)

    Chapter  Google Scholar 

  35. Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1990)

    MATH  Google Scholar 

  36. Kiniry, J.R., Cok, D.R.: ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2, including a case study involving the use of the tool to verify portions of an Internet voting tally system. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108–128. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  37. LaLonde, W.R., Thomas, D.A., Pugh, J.R.: An exemplar based Smalltalk. ACM SIGPLAN Notices 21(11), 322–330 (1986); In: Meyrowitz, N. (ed.) OOPSLA 1986 Conference Proceedings, Portland, Oregon (September 1986)

    Google Scholar 

  38. 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 

  39. 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, 50011

    Chapter  Google Scholar 

  40. Leavens, G.T., Baker, A.L.: Enhancing the pre- and post condition 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), http://tinyurl.com/qv84o

    Chapter  Google Scholar 

  41. 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), http://www.cs.iastate.edu/~leavens/FoCBS-book/06-leavens-dhara.pdf

    Google Scholar 

  42. Leavens, G.T., Naumann, D.A.: Behavioral subtyping, specification inheritance, and modular reasoning. Technical Report 06-20a, Department of Computer Science, Iowa State University, Ames, Iowa, 50011 (August 2006), ftp://ftp.cs.iastate.edu/pub/techreports/TR06-20/TR.pdf

  43. Leavens, G.T., Weihl, W.E.: Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica 32(8), 705–778 (1995)

    MATH  MathSciNet  Google Scholar 

  44. Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming 55(1-3), 185–208 (2005), http://dx.doi.org/10.1016/j.scico.2004.05.015

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  Google Scholar 

  46. Leavens, G.T., Leino, K.R.M., Müller, P.: Specification and verification challenges for sequential object-oriented programs. Technical Report 06-14, Department of Computer Science, Iowa State University, Ames, Iowa (May 2006), ftp://ftp.cs.iastate.edu/pub/techreports/TR06-14/TR.pdf

  47. Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., Müller, P., Kiniry, J., Chalin, P.: JML reference manual. Department of Computer Science, Iowa State University (January 2006), available from: http://www.jmlspecs.org

  48. Leino, K.R.M.: Toward Reliable Modular Programs. PhD thesis, California Institute of Technology, Available as Technical Report Caltech-CS-TR-95-03 (1995)

    Google Scholar 

  49. Leino, K.R.M.: Data groups: Specifying the modification of extended state. In: OOPSLA 1998 Conference Proceedings. ACM SIGPLAN Notices, vol. 33(10), pp. 144–153. ACM, New York (1998)

    Chapter  Google Scholar 

  50. Leino, K.R.M., Manohar, R.: Joining specification statements. Theoretical Comput. Sci. 216(1-2), 375–394 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  51. Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–515. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  52. Leino, K.R.M., Müller, P.: A verification methodology for model fields. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 115–130. Springer, Heidelberg (2006), http://tinyurl.com/pzll8

    Chapter  Google Scholar 

  53. Liskov, B.: Data abstraction and hierarchy. ACM SIGPLAN Notices 23(5), 17–34 (1988), Revised version of the keynote address given at OOPSLA 1987

    Article  Google Scholar 

  54. Liskov, B., Guttag, J.: Program Development in Java. The MIT Press, Cambridge (2001)

    Google Scholar 

  55. Liskov, B., Wing, J.: A behavioral notion of subtyping. ACM Trans. Prog. Lang. Syst. 16(6), 1811–1841 (1994)

    Article  Google Scholar 

  56. Liskov, B., Wing, J.M.: Specifications and their use in defining subtypes. ACM SIGPLAN Notices 28(10), 16–28 (1993); Paepcke, A. (ed.) OOPSLA 1993 Proceedings (1993)

    Article  Google Scholar 

  57. Marché, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML. Journal of Logic and Algebraic Programming 58(1-2), 89–106 (2004)

    Article  MATH  Google Scholar 

  58. Meyer, B.: Eiffel: The Language. Object-Oriented Series. Prentice Hall, New York (1992)

    MATH  Google Scholar 

  59. Meyer, B.: Object-oriented Software Construction, 2nd edn. Prentice Hall, New York (1997)

    MATH  Google Scholar 

  60. Mitchell, R., McKim, J.: Design by Contract by Example. Addison-Wesley, Indianapolis (2002)

    Google Scholar 

  61. Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall International, Hempstead (1994)

    MATH  Google Scholar 

  62. Müller, P.: Modular Specification and Verification of Object-Oriented Programs. In: Müller, P. (ed.) Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002), http://tinyurl.com/jtwot

    Chapter  Google Scholar 

  63. Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Sci. Comput. Programming 62(3), 253–286 (2006), http://dx.doi.org/10.1016/j.scico.2006.03.001

    Article  MATH  MathSciNet  Google Scholar 

  64. Naumann, D.A.: Calculating sharp adaptation rules. Inf. Process. Lett. 77, 201–208 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  65. Naumann, D.A., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state. Theoretical Comput. Sci (to appear, 2006)

    Google Scholar 

  66. Noble, J., Vitek, J., Potter, J.: Flexible alias protection. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, pp. 158–185. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  67. 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)

    Article  Google Scholar 

  68. Olderog, E.: On the notion of expressiveness and the rule of adaptation. Theoretical Comput. Sci. 24, 337–347 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  69. Parkinson, M.J.: Local reasoning for Java. Technical Report 654, University of Cambridge Computer Laboratory, (November 2005), The author’s Ph.D. dissertation, http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-654.pdf

  70. Pierik, C.: Validation Techniques for Object-Oriented Proof Outlines. PhD thesis, Universiteit Utrecht (2006), http://igitur-archive.library.uu.nl/dissertations/2006-0502-200341/index.htm

  71. Poetzsch-Heffter, A.: Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich (January 1997), http://tinyurl.com/g7xgm

  72. Poetzsch-Heffter, A., Müller, P.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 162–176. Springer, Heidelberg (1999), http://tinyurl.com/krjle

    Chapter  Google Scholar 

  73. Poetzsch-Heffter, A., Müller, P., Schäfer, J.: The Jive tool (April 2006) (Checked August 2), http://softech.informatik.uni-kl.de/twiki/bin/view/Homepage/Jive

  74. Poll, E.: A coalgebraic semantics of subtyping. In: Reichel, H. (ed.) Coalgebraic Methods in Computer Science (CMCS). Electronic Notes in Theoretical Computer Science. vol. 33. Elsevier, Amsterdam (2000)

    Google Scholar 

  75. Raghavan, A.D., Leavens, G.T.: Desugaring JML method specifications. Technical Report 00-03e, Iowa State University, Department of Computer Science (May 2005), ftp://ftp.cs.iastate.edu/pub/techreports/TR00-03/TR.pdf

  76. Robby, E.R., Dwyer, M.B., Hatcliff, J.: Bogor: An extensible and highly-modular model checking framework. In: Proceedings of the 9th European Software Engineering Conference held jointly with the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering. SIGSOFT Softw. Eng. Notes, vol. 28(5), pp. 267–276. ACM, New York (2003)

    Google Scholar 

  77. Robby, E.R., Dwyer, M., Hatcliff, J.: Checking strong specifications using an extensible software model checking framework. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 404–420. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  78. Stepney, S., Barden, R., Cooper, D. (eds.): Object Orientation in Z. Workshops in Computing. Springer, Cambridge (1992)

    Google Scholar 

  79. Specification in Fresco. In: Stepney, et al., [78], ch. 11, pp. 127–135

    Google Scholar 

  80. 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 

  81. Wing, J.M.: Writing Larch interface language specifications. ACM Trans. Prog. Lang. Syst. 9(1), 1–24 (1987)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Iowa State University, 229 Atanasoff Hall, Ames, IA, 50011-1041, USA

    Gary T. Leavens

Authors
  1. Gary T. Leavens
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. International Institute of Software Technology, United Nations University, Macau, China

    Zhiming Liu

  2. Software Engineering Institute, East China Normal University, 200062, Shanghai, China

    Jifeng He

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Leavens, G.T. (2006). JML’s Rich, Inherited Specifications for Behavioral Subtypes. In: Liu, Z., He, J. (eds) Formal Methods and Software Engineering. ICFEM 2006. Lecture Notes in Computer Science, vol 4260. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901433_2

Download citation

  • DOI: https://doi.org/10.1007/11901433_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-47460-9

  • Online ISBN: 978-3-540-47462-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation