Preliminary design of JML: a behavioral interface specification language for java

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.

REFERENCES

• 1: {AGH00} Ken Arnold, James Gosling, and David Holmes. The Java Programming Language Third Edition. Addison-Wesley, Reading, MA, 2000.
• 2: Pierre America, Inheritance and subtyping in a parallel object-oriented language, European conference on object-oriented programming on ECOOP '87, p.234-242, October 1987, Paris, France
• 3: Pierre America, Designing an Object-Oriented Programming Language with Behavioural Subtyping, Proceedings of the REX School/Workshop on Foundations of Object-Oriented Languages, p.60-90, May 28-June 01, 1990
• 4: R. J. R. Back, A calculus of refinements for program derivations, Acta Informatica, v.25 n.6, p.593-624, Aug. 1988 [doi>10.1007/BF00291051]
• 5: {BG98} Kent Beck and Erich Gamma. Test infected: Programmers love writing tests. Java Report, 3(7):37--50, 1998.
• 6: Alex Borgida , John Mylopoulos , Raymond Reiter, On the Frame Problem in Procedure Specifications, IEEE Transactions on Software Engineering, v.21 n.10, p.785-798, October 1995 [doi>10.1109/32.469460]
• 7: Ralph Back , Anna Mikhajlova , Joakim Wright von, Modeling Component Environments and Interactive Programs Using Iterative Choice, Turku Centre for Computer Science, 1998
• 8: Ralph-Johan J. Back , Abo Akademi , J. Von Wright , F. B. Schneider , D. Gries, Refinement Calculus: A Systematic Introduction, Springer-Verlag New York, Inc., Secaucus, NJ, 1998
• 9: Martin Büchi , Wolfgang Weck, Generic Wrappers, Proceedings of the 14th European Conference on Object-Oriented Programming, p.201-225, June 12-16, 2000
• 10: {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.
• 11: {Cha04} Patrice Chalin. JML support for primitive arbitrary precision numeric types: Definition and semantics. Journal of Object Technology, 3(6):57--79, June 2004.
• 12: {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.
• 13: {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.
• 14: Yoonsik Cheon , Gary T. Leavens, A Simple and Practical Approach to Unit Testing: The JML and JUnit Way, Proceedings of the 16th European Conference on Object-Oriented Programming, p.231-255, June 10-14, 2002
• 15: Yoonsik Cheon , Gary T. Leavens, A contextual interpretation of undefinedness for runtime assertion checking, Proceedings of the sixth international symposium on Automated analysis-driven debugging, p.149-158, September 19-21, 2005, Monterey, California, USA [doi>10.1145/1085130.1085150]
• 16: Edward Cohen, Programming in the 1990s: an introduction to the calculation of programs, Springer-Verlag New York, Inc., New York, NY, 1990
• 17: Krishna Kishore Dhara , Gary T. Leavens, Forcing behavioral subtyping through specification inheritance, Proceedings of the 18th international conference on Software engineering, p.258-267, March 25-29, 1996, Berlin, Germany
• 18: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001 [doi>10.1109/32.908957]
• 19: Kate Finney, Mathematical Notation in Formal Specification: Too Difficult for the Masses?, IEEE Transactions on Software Engineering, v.22 n.2, p.158-159, February 1996 [doi>10.1109/32.485225]
• 20: {FL98} John Fitzgerald and Peter Gorm Larsen. Modelling Systems: Practical Tools in Software Development. Cambridge, Cambridge, UK, 1998.
• 21: John V. Guttag , James J. Horning, Larch: languages and tools for formal specification, Springer-Verlag New York, Inc., New York, NY, 1993
• 22: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java Language Specification, Second Edition: The Java Series, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 23: David K. Gifford , John M. Lucassen, Integrating functional and imperative programming, Proceedings of the 1986 ACM conference on LISP and functional programming, p.28-38, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319848]
• 24: {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.
• 25: Ian Hayes , Bill Flinn, Specification Case Studies, Prentice Hall Professional Technical Reference, 1992
• 26: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 27: {Hoa72} C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271--281, 1972.
• 28: {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.
• 29: Cliff B. Jones, Systematic software development using VDM (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 30: H. B. M. Jonkers, Upgrading the Pre- and Postcondition Technique, Proceedings of the 4th International Symposium of VDM Europe on Formal Software Development-Volume I: Conference Contributions, p.428-456, October 21-25, 1991
• 31: Bart Jacobs , Joachim van den Berg , Marieke Huisman , Martijn van Berkum , U. Hensel , H. Tews, Reasoning about Java classes: preliminary report, ACM SIGPLAN Notices, v.33 n.10, p.329-340, Oct. 1998
• 32: Gary T. Leavens , Albert L. Baker, Enhancing the Pre- and Postcondition Technique for More Expressive Specifications, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume II, p.1087-1106, September 20-24, 1999
• 33: {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.
• 34: {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.
• 35: {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.
• 36: {Lea00} Gary T. Leavens. Larch frequently asked questions. Version 1.110. Available in http://www.cs.iastate.edu/~leavens/larch-faq.html, May 2000.
• 37: {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 [e-mail].
• 38: {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.
• 39: K. Rustan M. Leino, Data groups: specifying the modification of extended state, ACM SIGPLAN Notices, v.33 n.10, p.144-153, Oct. 1998
• 40: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 41: K. Lano , H. Haughton, Object-oriented specification case studies, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994
• 42: {LNS00} K. Rustan M. Leino, Greg Nelson, and James B. Saxe. ESC/Java user's manual. Technical note, Compaq Systems Research Center, October 2000.
• 43: {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.
• 44: K. Rustan M. Leino , Arnd Poetzsch-Heffter , Yunhong Zhou, Using data groups to specify and check side effects, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 45: {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.
• 46: {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.
• 47: David C. Luckham , Friedrich W. von Henke , Bernd Krieg-Brückner , Olaf Owe, ANNA: a language for annotating Ada programs, Springer-Verlag New York, Inc., New York, NY, 1987
• 48: Barbara H. Liskov , Jeannette M. Wing, A behavioral notion of subtyping, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.6, p.1811-1841, Nov. 1994 [doi>10.1145/197320.197383]
• 49: {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.
• 50: Gary T. Leavens , Jeannette M. Wing, Protective Interface Specifications, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.520-534, April 14-18, 1997
• 51: Bertrand Meyer, Applying "Design by Contract", Computer, v.25 n.10, p.40-51, October 1992 [doi>10.1109/2.161279]
• 52: Bertrand Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 53: Bertrand Meyer, Object-oriented software construction (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• 54: Carroll Morgan, Programming from specifications (2nd ed.), Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994
• 55: Peter Müller, Modular specification and verification of object-oriented programs, Springer-Verlag New York, Inc., New York, NY, 2002
• 56: {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.
• 57: Hanne Riis Nielson , Flemming Nielson , Torben Amtoft, Polymorphic Subtyping for Effect Analysis: The Static Semantics, Selected papers from the 5th LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages, p.141-171, June 24-26, 1996
• 58: {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.
• 59: Sam Owre , John Rushby , Natarajan Shankar , Friedrich von Henke, Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS, IEEE Transactions on Software Engineering, v.21 n.2, p.107-125, February 1995 [doi>10.1109/32.345827]
• 60: William F. Ogden , Murali Sitaraman , Bruce W. Weide , Stuart H. Zweben, Part I: the RESOLVE framework and discipline: a research synopsis, ACM SIGSOFT Software Engineering Notes, v.19 n.4, p.23-28, Oct. 1994 [doi>10.1145/190679.190681]
• 61: {PH97} Arnd Poetzsch-Heffter. Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich, January 1997.
• 62: {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.
• 63: Clyde Ruby , Gary T. Leavens, Safely creating correct subclasses without seeing superclass code, ACM SIGPLAN Notices, v.35 n.10, p.208-228, Oct. 2000
• 64: {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.
• 65: David S. Rosenblum, A Practical Approach to Programming With Assertions, IEEE Transactions on Software Engineering, v.21 n.1, p.19-31, January 1995 [doi>10.1109/32.341844]
• 66: J. M. Spivey, The Z notation: a reference manual, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1992
• 67: {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.
• 68: Yang Meng Tan, Interface language for supporting programming styles, ACM SIGPLAN Notices, v.29 n.8, p.74-83, Aug. 1994
• 69: Yang Meng Tan, Formal Specification Techniques for Engineering Modular C Programs, Kluwer Academic Publishers, Norwell, MA, 1996
• 70: Jean-Pierre Talpin , Pierre Jouvelot, The type and effect discipline, Information and Computation, v.111 n.2, p.245-296, June 1994 [doi>10.1006/inco.1994.1046]
• 71: Jim Woodcock , Jim Davies, Using Z: specification, refinement, and proof, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
• 72: {Wil94} Alan Wills. Refinement in Fresco. In Lano and Houghton {LH94}, chapter 9, pages 184--201.
• 73: J. M. Wing, A TWO-TIERED APPROACH TO SPECIFYING PROGRAMS, Massachusetts Institute of Technology, Cambridge, MA, 1983
• 74: Jeannette M. Wing, Writing Larch interface language specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.1, p.1-24, Jan. 1987 [doi>10.1145/9758.10500]
• 75: Jeannette M. Wing, A Specifier's Introduction to Formal Methods, Computer, v.23 n.9, p.8-23, September 1990 [doi>10.1109/2.58215]
• 76: Tim Wahls , Gary T. Leavens , Albert L. Baker, Executing Formal Specifications with Concurrent Constraint Programming, Automated Software Engineering, v.7 n.4, p.315-343, December 2000 [doi>10.1023/A:1026554217992]
• 77: {WR25} A. N. Whitehead and B. Russell. Principia Mathematica. Cambridge University Press, London, second edition. edition, 1925.
• 78: Andrew K. Wright, Typing references by effect inference, Symposium proceedings on 4th European symposium on programming, p.473-491, January 1992, Rennes, France

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.12 Interoperability
            Subjects: Interface definition languages

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages
        D.2.11 Software Architectures
            Subjects: Languages (e.g., description, interconnection, definition)

General Terms:
Languages