Gary T. Leavens
Albert L. Baker
Skip Abstract Section
Abstract
JML is a behavioral interface specification language tailored to Java(TM). Besides pre- and postconditions, it also allows assertions to be intermixed with Java code; these aid verification and debugging. JML is designed to be used by working software engineers; to do this it follows Eiffel in using Java expressions in assertions. JML combines this idea from Eiffel with the model-based approach to specifications, typified by VDM and Larch, which results in greater expressiveness. Other expressiveness advantages over Eiffel include quantifiers, specification-only variables, and frame conditions.This paper discusses the goals of JML, the overall approach, and describes the basic features of the language through examples. It is intended for readers who have some familiarity with both Java and behavioral specification using pre- and postconditions.
- {AGH00} Ken Arnold, James Gosling, and David Holmes. The Java Programming Language Third Edition. Addison-Wesley, Reading, MA, 2000.]]Google Scholar
Digital Library
- {Ame87} Pierre America. Inheritance and subtyping in a parallel object-oriented language. In Jean Bezivin et al., editors, ECOOP '87, European Conference on Object-Oriented Programming, Paris, France, pages 234--242, New York, NY, June 1987. Springer-Verlag. Lecture Notes in Computer Science, volume 276.]] Google ScholarDigital Library
- {Ame91} Pierre America. Designing an object-oriented programming language with behavioural subtyping. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Foundations of Object-Oriented Languages, REX School/Workshop, Noordwijkerhout, The Netherlands, May/June 1990, volume 489 of Lecture Notes in Computer Science, pages 60--90. Springer-Verlag, New York, NY, 1991.]] Google ScholarDigital Library
- {Bac88} R. J. R. Back. A calculus of refinements for program derivations. Acta Informatica, 25(6):593--624, August 1988.]] Google ScholarDigital Library
- {BG98} Kent Beck and Erich Gamma. Test infected: Programmers love writing tests. Java Report, 3(7):37--50, 1998.]]Google Scholar
- {BMR95} Alex Borgida, John Mylopoulos, and Raymond Reiter. On the frame problem in procedure specifications. IEEE Transactions on Software Engineering, 21(10): 785--798, October 1995.]] Google ScholarDigital Library
- {BMvW98} Ralph Back, Anna Mikhajlova, and Joakim von Wright. Modeling component environments and interactive programs using iterative choice. Technical Report 200, Turku Centre for Computer Science, September 1998. http://www.tucs.abo.fi/publications/techreports/TR200.html.]] Google ScholarDigital Library
- {BvW98} Ralph-Johan Back and Joakim von Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer-Verlag, 1998.]] Google ScholarDigital Library
- {BW00} Martin Büchi and Wolfgang Weck. Generic wrappers. In Elisa Bertino, editor, ECOOP 2000 --- Object-Oriented Programming 14th European Conference, volume 1850 of Lecture Notes in Computer Science, pages 201--225, 2000.]] Google ScholarDigital Library
- {Cha02} Patrice Chalin. 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
- {Cha04} Patrice Chalin. JML support for primitive arbitrary precision numeric types: Definition and semantics. Journal of Object Technology, 3(6):57--79, June 2004.]]Google ScholarCross Ref
- {Che03} Yoonsik Cheon. A runtime assertion checker for the Java Modeling Language. Technical Report 03-09, Department of Computer Science, Iowa State University, Ames, IA, April 2003. The author's Ph.D. dissertation.]]Google ScholarCross Ref
- {CL02a} Yoonsik Cheon and Gary T. Leavens. A run-time assertion checker for the Java Modeling Language (JML). In Hamid R. Arabnia and Youngsong Mun, editors, Proceedings of the International Conference on Software Engineering Research and Practice (SERP '02), Las Vegas, Nevada, USA, June 24-27, 2002, pages 322--328. CSREA Press, June 2002.]]Google Scholar
- {CL02b} Yoonsik Cheon and Gary T. Leavens. A simple and practical approach to unit testing: The JML and JUnit way. In Boris Magnusson, editor, ECOOP 2002 --- Object-Oriented Programming, 16th European Conference, Máalaga, Spain, Proceedings, volume 2374 of Lecture Notes in Computer Science, pages 231--255, Berlin, June 2002. Springer-Verlag.]] Google ScholarDigital Library
- {CL05} Yoonsik Cheon and Gary T. Leavens. A contextual interpretation of undefinedness for runtime assertion checking. In AADEBUG 2005, Proceedings of the Sixth International Symposium on Automated and Analysis-Driven Debugging, Monterey, California, September 19--21, 2005, pages 149--157. ACM Press, September 2005.]] Google ScholarDigital Library
- {Coh90} Edward Cohen. Programming in the 1990s: An Introduction to the Calculation of Programs. Springer-Verlag, New York, NY, 1990.]] Google ScholarDigital Library
- {DL96} Krishna Kishore Dhara and Gary T. Leavens. Forcing behavioral subtyping through specification inheritance. In Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany, pages 258--267. IEEE Computer Society Press, March 1996. A corrected version is Iowa State University, Dept. of Computer Science TR #95-20c.]] Google ScholarDigital Library
- {ECGN01} Michael Ernst, Jake Cockrell, William G. Gris-wold, and David Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering, 27(2):99--123, February 2001.]] Google ScholarDigital Library
- {Fin96} Kate Finney. Mathematical notation in formal specification: Too difficult for the masses? IEEE Transactions on Software Engineering, 22(2):158--159, February 1996.]] Google ScholarDigital Library
- {FL98} John Fitzgerald and Peter Gorm Larsen. Modelling Systems: Practical Tools in Software Development. Cambridge, Cambridge, UK, 1998.]]Google Scholar
- {GHG+93} John V. Guttag, James J. Horning, S. J. Garland, K. D. Jones, A. Modet, and J. M. Wing. Larch: Languages and Tools for Formal Specification. Springer-Verlag, New York, NY, 1993.]] Google ScholarDigital Library
- {GJSB00} James Gosling, Bill Joy, Guy Steele, and Gilad Bracha. The Java Language Specification Second Edition. The Java Series. Addison-Wesley, Boston, Mass., 2000.]] Google ScholarDigital Library
- {GL86} David K. Gifford and John M. Lucassen. Integrating functional and imperative programming. In ACM Conference on LISP and Functional Programming, pages 28--38. ACM, August 1986.]] Google ScholarDigital Library
- {GS95} David Gries and Fred B. Schneider. Avoiding the undefined by underspecification. In Jan van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, number 1000 in Lecture Notes in Computer Science, pages 366--373. Springer-Verlag, New York, NY, 1995.]]Google Scholar
- {Hay93} I. Hayes, editor. Specification Case Studies. International Series in Computer Science. Prentice-Hall, Inc., second edition, 1993.]] Google ScholarDigital Library
- {Hoa69} C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576--583, October 1969.]] Google ScholarDigital Library
- {Hoa72} C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271--281, 1972.]]Google ScholarDigital Library
- {Hui01} Marieke Huisman. Reasoning about Java Programs in higher order logic with PVS and Isabelle. Ipa dissertation series, 2001-03, University of Nijmegen, Holland, February 2001.]]Google Scholar
- {Jon90} Cliff B. Jones. Systematic Software Development Using VDM. International Series in Computer Science. Prentice Hall, Englewood Cliffs, N.J., second edition, 1990.]] Google ScholarDigital Library
- {Jon91} H. B. M. Jonkers. Upgrading the pre- and postcondition technique. In S. Prehn and W. J. Toetenel, editors, VDM '91 Formal Software Development Methods 4th International Symposium of VDM Europe Noordwijkerhout, The Netherlands, Volume 1: Conference Contributions, volume 551 of Lecture Notes in Computer Science, pages 428--456. Springer-Verlag, New York, NY, October 1991.]] Google ScholarDigital Library
- {JvdBH+98} Bart Jacobs, Joachim van den Berg, Marieke Huisman, Martijn van Berkum, Ulrich Hensel, and Hendrik Tews. Reasoning about Java classes (preliminary report). In OOPSLA '98 Conference Proceedings, volume 33(10) of ACM SIGPLAN Notices, pages 329--340. ACM, October 1998.]] Google ScholarDigital Library
- {LB99} Gary T. Leavens and Albert L. Baker. Enhancing the pre- and postcondition technique for more expressive specifications. In Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors, FM'99 --- Formal Methods: World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 1999, Proceedings, volume 1709 of Lecture Notes in Computer Science, pages 1087--1106. Springer-Verlag, 1999.]] Google ScholarDigital Library
- {LBR99} Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A notation for detailed design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds, editors, Behavioral Specifications of Businesses and Systems, pages 175--188. Kluwer Academic Publishers, Boston, 1999.]]Google ScholarCross Ref
- {Lea96} Gary T. Leavens. An overview of Larch/C++: Behavioral specifications for C++ modules. In Haim Kilov and William Harvey, editors, Specification of Behavioral Semantics in Object-Oriented Information Modeling, chapter 8, pages 121--142. Kluwer Academic Publishers, Boston, 1996. An extended version is TR #96-01d, Department of Computer Science, Iowa State University, Ames, Iowa, 50011.]]Google Scholar
- {Lea97} Gary T. Leavens. Larch/C++ Reference Manual. Version 5.14. Available in ftp://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, October 1997.]]Google Scholar
- {Lea00} Gary T. Leavens. Larch frequently asked questions. Version 1.110. Available in http://www.cs.iastate.edu/~leavens/larch-faq.html, May 2000.]]Google Scholar
- {Lei95a} K. Rustan M. Leino. 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, November 1995. Obtain from the author, at [email protected].]]Google Scholar
- {Lei95b} K. Rustan M. Leino. Toward Reliable Modular Programs. PhD thesis, California Institute of Technology, 1995. Available as Technical Report Caltech-CS-TR-95-03.]] Google ScholarDigital Library
- {Lei98} K. Rustan M. Leino. Data groups: Specifying the modification of extended state. In OOPSLA '98 Conference Proceedings, volume 33(10) of ACM SIGPLAN Notices, pages 144--153. ACM, October 1998.]] Google ScholarDigital Library
- {LG88} John M. Lucassen and David K. Gifford. Polymorphic effect systems. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, Calif., pages 47--57. ACM, January 1988.]] Google ScholarDigital Library
- {LH94} K. Lano and H. Haughton, editors. Object-Oriented Specification Case Studies. The Object-Oriented Series. Prentice Hall, New York, NY, 1994.]] Google ScholarDigital Library
- {LNS00} K. Rustan M. Leino, Greg Nelson, and James B. Saxe. ESC/Java user's manual. Technical note, Compaq Systems Research Center, October 2000.]]Google Scholar
- {LPC+05} Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David R. Cok, Peter Müller, and Joseph Kiniry. JML reference manual. Department of Computer Science, Iowa State University. Available from http://www.jmlspecs.org, July 2005.]]Google Scholar
- {LPHZ02} K. Rustan M. Leino, Arnd Poetzsch-Heffter, and Yunhong Zhou. Using data groups to specify and check side effects. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI'02), volume 37, 5 of SIGPLAN, pages 246--257, New York, June 17--19 2002. ACM Press.]] Google ScholarDigital Library
- {Luc87} John M. Lucassen. Types and effects: Towards the integration of functional and imperative programming. Technical Report TR-408, Massachusetts Institute of Technology, Laboratory for Computer Science, August 1987.]]Google Scholar
- {LvH85} David Luckham and Friedrich W. von Henke. An overview of anna - a specification language for Ada. IEEE Software, 2(2):9--23, March 1985.]]Google ScholarDigital Library
- {LvHKBO87} David Luckham, Friedrich W. von Henke, Bernd Krieg-Brückner, and Olaf Owe. ANNA - A Language for Annotating Ada Programs, volume 260 of Lecture Notes in Computer Science. Springer-Verlag, New York, NY, 1987.]] Google ScholarDigital Library
- {LW94} Barbara Liskov and Jeannette Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6):1811--1841, November 1994.]] Google ScholarDigital Library
- {LW95} Gary T. Leavens and William E. Weihl. Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica, 32(8):705--778, November 1995.]]Google ScholarDigital Library
- {LW97} Gary T. Leavens and Jeannette M. Wing. Protective interface specifications. In Michel Bidoit and Max Dauchet, editors, TAPSOFT '97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lille, France, volume 1214 of Lecture Notes in Computer Science, pages 520--534. Springer-Verlag, New York, NY, 1997.]] Google ScholarDigital Library
- {Mey92a} Bertrand Meyer. Applying "design by contract". Computer, 25(10): 40--51, October 1992.]] Google ScholarDigital Library
- {Mey92b} Bertrand Meyer. Eiffel: The Language. Object-Oriented Series. Prentice Hall, New York, NY, 1992.]] Google ScholarDigital Library
- {Mey97} Bertrand Meyer. Object-oriented Software Construction. Prentice Hall, New York, NY, second edition, 1997.]] Google ScholarDigital Library
- {Mor94} Carroll Morgan. Programming from Specifications: Second Edition. Prentice Hall International, Hempstead, UK, 1994.]] Google ScholarDigital Library
- {Mül02} Peter Müller. Modular Specification and Verification of Object-Oriented Programs, volume 2262 of Lecture Notes in Computer Science. Springer-Verlag, 2002. The author's Ph.D. Thesis. Available from http://www.informatik.fernuni-hagen. de/import/pi5/publications.html.]]Google Scholar
- {MV94} Carroll Morgan and Trevor Vickers, editors. On the refinement calculus. Formal approaches of computing and information technology series. Springer-Verlag, New York, NY, 1994.]]Google Scholar
- {NNA97} H. R. Nielson, F. Nielson, and T. Amtoft. Polymorphic subtyping for effect analysis: The static semantics. In M. Dam, editor, Proceedings of the Fifth LOMAPS Workshop, number 1192 in Lecture Notes in Computer Science. Springer-Verlag, 1997.]] Google ScholarDigital Library
- {Org96} 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
- {ORSvH95} Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107--125, February 1995.]] Google ScholarDigital Library
- {OSWZ94} William F. Ogden, Murali Sitaraman, Bruce W. Weide, and Stuart H. Zweben. Part I: The RESOLVE framework and discipline --- a research synopsis. ACM SIGSOFT Software Engineering Notes, 19(4): 23--28, October 1994.]] Google ScholarDigital Library
- {PH97} Arnd Poetzsch-Heffter. Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich, January 1997.]]Google Scholar
- {RDF+05} Edwin Rodríguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, and Robby. Extending JML for modular specification and verification of multi-threaded programs. In Andrew P. Black, editor, ECOOP 2005 --- Object-Oriented Programming 19th European Conference, Glasgow, UK, volume 3586 of Lecture Notes in Computer Science, pages 551--576. Springer-Verlag, Berlin, July 2005.]] Google ScholarDigital Library
- {RL00} Clyde Ruby and Gary T. Leavens. Safely creating correct subclasses without seeing superclass code. In OOPSLA 2000 Conference on Object-Oriented Programming, Systems, Languages, and Applications, Minneapolis, Minnesota, volume 35(10) of ACM SIGPLAN Notices, pages 208--228, October 2000.]] Google ScholarDigital Library
- {RL05} Arun D. Raghavan and Gary T. Leavens. Desugaring JML method specifications. Technical Report 00-03e, Iowa State University, Department of Computer Science, May 2005.]]Google Scholar
- {Ros95} David S. Rosenblum. A practical approach to programming with assertions. IEEE Transactions on Software Engineering, 21(1): 19--31, January 1995.]] Google ScholarDigital Library
- {Spi92} J. Michael Spivey. The Z Notation: A Reference Manual. International Series in Computer Science. Prentice-Hall, New York, NY, second edition, 1992.]] Google ScholarDigital Library
- {SR05} Alexandru Salcianu and Martin Rinard. Purity and side effect analysis for java programs. In Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation, January 2005.]] Google ScholarDigital Library
- {Tan94} Yang Meng Tan. Interface language for supporting programming styles. ACM SIGPLAN Notices, 29(8):74--83, August 1994. Proceedings of the Workshop on Interface Definition Languages.]] Google ScholarDigital Library
- {Tan95} Yang Meng Tan. Formal Specification Techniques for Engineering Modular C Programs, volume 1 of Kluwer International Series in Software Engineering. Kluwer Academic Publishers, Boston, 1995.]] Google ScholarDigital Library
- {TJ94} Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Information and Computation, 111(2):245--296, June 1994.]] Google ScholarDigital Library
- {WD96} Jim Woodcock and Jim Davies. Using Z: Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science, 1996.]] Google ScholarDigital Library
- {Wil94} Alan Wills. Refinement in Fresco. In Lano and Houghton {LH94}, chapter 9, pages 184--201.]]Google Scholar
- {Win83} Jeannette Marie Wing. A two-tiered approach to specifying programs. Technical Report TR-299, Massachusetts Institute of Technology, Laboratory for Computer Science, 1983.]] Google ScholarDigital Library
- {Win87} Jeannette M. Wing. Writing Larch interface language specifications. ACM Transactions on Programming Languages and Systems, 9(1): 1--24, January 1987.]] Google ScholarDigital Library
- {Win90} Jeannette M. Wing. A specifier's introduction to formal methods. Computer, 23(9):8--24, September 1990.]] Google ScholarDigital Library
- {WLB00} Tim Wahls, Gary T. Leavens, and Albert L. Baker. Executing formal specifications with concurrent constraint programming. Automated Software Engineering, 7(4):315--343, December 2000.]] Google ScholarDigital Library
- {WR25} A. N. Whitehead and B. Russell. Principia Mathematica. Cambridge University Press, London, second edition. edition, 1925.]]Google Scholar
- {Wri92} Andrew K. Wright. Typing references by effect inference. In Bernd Krieg-Bruckner, editor, ESOP '92, 4th European Symposium on Programming, Rennes, France, February 1992, Proceedings, volume 582 of Lecture Notes in Computer Science, pages 473--491. Springer-Verlag, New York, NY, 1992.]] Google ScholarDigital Library
Index Terms
- Preliminary design of JML: a behavioral interface specification language for java
Recommendations
Tutorial on JML, the java modeling language
ASE '07: Proceedings of the 22nd IEEE/ACM International Conference on Automated Software EngineeringThe Java Modeling Language (JML) is widely used in academic research as a common language for formal methods tools that work with Java. JML is a design by contract language that can be used to specify detailed designs of Java programs, frameworks, and ...
JML (poster session): notations and tools supporting detailed design in Java
OOPSLA '00: Addendum to the 2000 proceedings of the conference on Object-oriented programming, systems, languages, and applications (Addendum)JML is a notation for specifying the detailed design of Java classes and interfaces. JML's assertions are stated using a slight extension of Java's expression syntax. This should make it easy to use. Tools for JML aid in static analysis, verification, ...
Preliminary design of a unified JML representation and software infrastructure
FTfJP '09: Proceedings of the 11th International Workshop on Formal Techniques for Java-like ProgramsAs a Behavioral Interface Specification Language (BISL) for Java, the Java Modeling Language (JML) is tightly coupled to the base language it enhances. Up until Java 1.4, JML kept apace with the evolution of its base language. Java 5 and subsequent ...
Comments