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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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)
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)
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)
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)
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
Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Transactions on Software Engineering 21(10), 785–798 (1995)
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)
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
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)
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)
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)
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
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)
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
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)
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
Cheon, Y., Leavens, G.T.: The Larch/Smalltalk interface specification language. ACM Transactions on Software Engineering and Methodology 3(3), 221–253 (1994)
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)
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)
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)
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
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
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
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
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Inc., Englewood Cliffs (1976)
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)
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)
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)
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)
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)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–583 (1969)
Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1(4), 271–281 (1972)
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
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)
Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1990)
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)
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)
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)
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
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
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
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
Leavens, G.T., Weihl, W.E.: Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica 32(8), 705–778 (1995)
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
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
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
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
Leino, K.R.M.: Toward Reliable Modular Programs. PhD thesis, California Institute of Technology, Available as Technical Report Caltech-CS-TR-95-03 (1995)
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)
Leino, K.R.M., Manohar, R.: Joining specification statements. Theoretical Comput. Sci. 216(1-2), 375–394 (1999)
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)
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
Liskov, B.: Data abstraction and hierarchy. ACM SIGPLAN Notices 23(5), 17–34 (1988), Revised version of the keynote address given at OOPSLA 1987
Liskov, B., Guttag, J.: Program Development in Java. The MIT Press, Cambridge (2001)
Liskov, B., Wing, J.: A behavioral notion of subtyping. ACM Trans. Prog. Lang. Syst. 16(6), 1811–1841 (1994)
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)
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)
Meyer, B.: Eiffel: The Language. Object-Oriented Series. Prentice Hall, New York (1992)
Meyer, B.: Object-oriented Software Construction, 2nd edn. Prentice Hall, New York (1997)
Mitchell, R., McKim, J.: Design by Contract by Example. Addison-Wesley, Indianapolis (2002)
Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall International, Hempstead (1994)
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
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
Naumann, D.A.: Calculating sharp adaptation rules. Inf. Process. Lett. 77, 201–208 (2001)
Naumann, D.A., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state. Theoretical Comput. Sci (to appear, 2006)
Noble, J., Vitek, J., Potter, J.: Flexible alias protection. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, pp. 158–185. Springer, Heidelberg (1998)
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)
Olderog, E.: On the notion of expressiveness and the rule of adaptation. Theoretical Comput. Sci. 24, 337–347 (1983)
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
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
Poetzsch-Heffter, A.: Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich (January 1997), http://tinyurl.com/g7xgm
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
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
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)
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
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)
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)
Stepney, S., Barden, R., Cooper, D. (eds.): Object Orientation in Z. Workshops in Computing. Springer, Cambridge (1992)
Specification in Fresco. In: Stepney, et al., [78], ch. 11, pp. 127–135
Wing, J.M.: A two-tiered approach to specifying programs. Technical Report TR-299, Massachusetts Institute of Technology, Laboratory for Computer Science (1983)
Wing, J.M.: Writing Larch interface language specifications. ACM Trans. Prog. Lang. Syst. 9(1), 1–24 (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)