Skip to main content
SpringerLink
Log in

A Methodology for Invariants, Framing, and Subtyping in JML

  • Chapter
  • First Online:
Principled Software Development

Abstract

The Java Modeling Language (JML) is a specification language for describing the functional behavior of sequential Java program modules. The object-oriented features of Java make specifying invariants and framing difficult in the presence of subtyping. Using regions as a basis for a methodology, we precisely describe a technique for specifying invariants and framing in the presence of subtyping. We also extend JML by adding separating conjunction (from separation logic) for certain kinds of assertions.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 11439
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 14299
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
JPY 14299
Price includes VAT (Japan)
  • Durable hardcover 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.

Similar content being viewed by others

References

  1. Pierre America. A Behavioural Approach to Subtyping in Object-Oriented Programming Languages. Tech. rep. 443. Revised from the January 1989 version. Nederlandse Philips Bedrijven B. V.: Philips Research Laboratories, Apr. 1989.

    Google Scholar 

  2. Anindya Banerjee, David A. Naumann, and Stan Rosenberg. “Local Reasoning for Global Invariants, Part I: Region Logic”. In: Journal of the ACM 60.3 (June 2013), 18:1–18:56. ISSN: 0004-5411. https://doi.org/10.1145/2485982. URL: http://doi.acm.org/10.1145/2485982.

  3. Yuyan Bao. “Reasoning About Frame Properties in Object-Oriented Programs”. PhD thesis. University of Central Florida, 2017. URL: http://www.cs.ucf.edu/~ybao/tech-reports/TR_dissertation.pdf.

  4. Yuyan Bao, Gary T. Leavens, and Gidon Ernst. “Conditional Effects in Fine-grained Region Logic”. In: Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs. FTfJP ’15. Prague, Czech Republic: ACM, 2015, 5:1–5:6. ISBN: 978-1-4503-3656-7. https://doi.org/10.1145/2786536.2786537. URL: http://doi.acm.org/10.1145/2786536.2786537.

  5. Yuyan Bao, Gary T. Leavens, and Gidon Ernst. “Unifying Separation Logic and Region Logic to Allow Interoperability”. In: Formal Aspects of Computing 30.3 (Aug. 2018), pp. 381–441.

    Article  MathSciNet  Google Scholar 

  6. Mike Barnett and David Naumann. “Friends Need a Bit More: Maintaining Invariants Over Shared State”. In: Mathematics of Program Construction (MPC). Ed. by Dexter Kozen. Vol. 3125. Lecture Notes in Computer Science. Springer-Verlag, July 2004, pp. 54–84. URL: http://www.springerlink.com/content/6gt28um7j5jgra12.

    Google Scholar 

  7. Mike Barnett et al. “Verification of Object-Oriented Programs with Invariants”. In: Journal of Object Technology 3.6 (2004), pp. 27–56. URL: http://tinyurl.com/m2a8j.

  8. Kevin Bierhoff and Jonathan Aldrich. “Lightweight Object Specification with Typestates”. In: SIGSOFT Softw. Eng. Notes 30.5 (Sept. 2005), pp. 217–226. ISSN: 0163-5948. https://doi.org/10.1145/1095430.1081741 URL: http://doi.acm.org/10.1145/1095430.1081741.

    Article  Google Scholar 

  9. Alex Borgida, John Mylopoulos, and Raymond Reiter. “On the Frame Problem in Procedure Specifications”. In: IEEE Transactions on Software Engineering 21.10 (Oct. 1995), pp. 785–798. URL: http://doi.ieeecomputersociety.org/10.1109/32.469460.

    Article  Google Scholar 

  10. Patrice Chalin et al. “Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2”. In: Formal Methods for Components and Objects (FMCO) 2005, Revised Lectures. Vol. 4111. Lecture Notes in Computer Science. Berlin: Springer-Verlag, 2006, pp. 342–363. URL: http://dx.doi.org/10.1007/11804192%5C_16.

  11. Robert DeLine and Manuel Fähndrich. “Typestates for objects”. In: ECOOP 2004 — Object-Oriented Programming, 18th European Conference. Vol. 3086. Lecture Notes in Computer Science. Springer Verlag, June 2004, pp. 465–490. URL: http://research.microsoft.com/apps/pubs/default.aspx?id=67463.

  12. Sophia Drossopoulou, Adrian Francalanza, and Peter Müller. “A Unified Framework for Verification Techniques for Object Invariants”. In: International Workshop on Foundations of Object-Oriented Languages (FOOL’08). 2008. URL: http://fool08.kuis.kyoto-u.ac.jp/drossopoulou.pdf.

  13. Samin S. Ishtiaq and Peter W. O’Hearn. “BI as an assertion language for mutable data structures”. In: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. POPL ’01. London, United Kingdom: ACM, 2001, pp. 14–26. ISBN: 1-58113-336-7. https://doi.org/10.1145/360204.375719. URL: http://doi.acm.org/10.1145/360204.375719.

  14. Ioannis T. Kassios. “The dynamic frames theory”. In: Formal Aspects of Computing 23.3 (May 2011), pp. 267–288. ISSN: 0934-5043. https://doi.org/10.1007/s00165-010-0152-5. URL: http://dx.doi.org/10.1007/s00165-010-0152-5.

    Article  MathSciNet  Google Scholar 

  15. Gary T. Leavens. “JML’s Rich, Inherited Specifications for Behavioral Subtypes”. In: Formal Methods and Software Engineering: 8th International Conference on Formal Engineering Methods (ICFEM). Ed. by Zhiming Liu and He Jifeng. Vol. 4260. Lecture Notes in Computer Science. New York, NY: Springer-Verlag, Nov 2006, pp. 2–34. URL: http://dx.doi.org/10.1007/11901433.

  16. Gary T. Leavens and Peter Müller. “Information Hiding and Visibility in Interface Specifications”. In: International Conference on Software Engineering (ICSE). Los Alamitos, California: IEEE, May 2007, pp. 385–395. URL: http://dx.doi.org/10.1109/ICSE.2007.44.

  17. Gary T. Leavens and David A. Naumann. “Behavioral Subtyping, Specification Inheritance, and Modular Reasoning”. In: TOPLAS 37.4 (Aug. 2015), 13:1–13:88. https://doi.org/10.1145/2766446. URL: http://doi.acm.org/10.1145/2766446.

    Article  Google Scholar 

  18. Gary T. Leavens and William E. Weihl. “Specification and Verification of Object-Oriented Programs Using Supertype Abstraction”. In: Acta Informatica 32.8 (Nov. 1995), pp. 705–778. URL: http://dx.doi.org/10.1007/BF01178658.

  19. Gary T. Leavens et al. “JML Reference Manual”. Available from http://www.jmlspecs.org. Sept. 2009.

  20. K. Rustan M. Leino. “Dafny: An Automatic Program Verifier for Functional Correctness”. In: Logic for Programming, Artificial Intelligence, and Reasoning, 16th International Conference, LPAR-16. Vol. 6355. Lecture Notes in Computer Science. Darkar, Senegal: Springer-Verlag, 2010, pp. 348–370.

    Google Scholar 

  21. K. Rustan M. Leino. “Data groups: Specifying the modification of extended state”. In: OOPSLA ’98 Conference Proceedings. Vol. 33(10). ACM SIGPLAN Notices. New York, NY: ACM, Oct. 1998, pp. 144–153. URL: http://doi.acm.org/10.1145/286936.286953.

  22. Barbara H. Liskov and Jeannette M. Wing. “A Behavioral Notion of Subtyping”. In: 16.6 (Nov. 1994), pp. 1811–1841. URL: http://doi.acm.org/10.1145/197320.197383.

  23. Bertrand Meyer. “Applying ‘Design by Contract”’. In: Computer 25.10 (Oct. 1992), pp. 40–51.

    Google Scholar 

  24. Peter Müller. Modular Specification and Verification of Object-Oriented Programs. Vol. 2262. Lecture Notes in Computer Science. Berlin: Springer-Verlag, 2002. URL: http://tinyurl.com/jtwot.

  25. Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. “Modular Specification of Frame Properties in JML”. In: Concurrency and Computation: Practice and Experience 15.2 (Feb. 2003), pp. 117–154. https://doi.org/10.1002/cpe.713 URL: ftp://ftp.cs.iastate.edu/pub/techreports/TR02-02/TR.pdf.

    Article  Google Scholar 

  26. Peter W. O’Hearn, Hongseok Yang, and John C. Reynolds. “Separation and Information Hiding”. In: ACM Trans. Program. Lang. Syst. 31.3 (Apr. 2009), 11:1–11:50. ISSN: 0164-0925. https://doi.org/10.1145/1498926.1498929. URL: http://doi.acm.org/10.1145/1498926.1498929.

    Article  Google Scholar 

  27. Matthew Parkinson and Gavin Bierman. “Separation Logic, Abstraction and Inheritance”. In: ACM Symposium on Principles of Programming Languages. Ed. by Philip Wadler. New York, NY: ACM, Jan. 2008, pp. 75–86.

    Google Scholar 

  28. D. L. Parnas. “On the Criteria to be Used in Decomposing Systems into Modules”. In: Communications of the ACM 15.12 (Dec. 1972), pp. 1053–1058.

    Article  Google Scholar 

  29. John C. Reynolds. “Separation Logic: A Logic for Shared Mutable Data Structures”. In: Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science. Los Alamitos, California: IEEE Computer Society Press, 2002, pp. 55–74. URL: http://dx.doi.org/10.1109/LICS.2002.1029817.

  30. Jan Smans et al. “Automatic verification of Java programs with dynamic frames”. In: Formal Aspects of Computing 22.3 (2010), pp. 423–457. ISSN: 1433-299X. https://doi.org/10.1007/s00165-010-0148-1. URL: http://dx.doi.org/10.1007/s00165-010-0148-1.

    Article  Google Scholar 

  31. Alexander J. Summers, Sophia Drossopoulou, and Peter Müller. “The Need for Flexible Object Invariants”. In: International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming. IWACO ’09. Genova, Italy: ACM, 2009, 6:1–6:9. ISBN: 978-1-60558-546-8. https://doi.org/10.1145/1562154.1562160. URL: http://doi.acm.org/10.1145/1562154.1562160.

  32. Benjamin Weiß. “Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction”. PhD thesis. Karlsruhe Institute of Technology, 2011.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The Pennsylvania State University, University Park, PA, USA

    Yuyan Bao

  2. University of Central Florida, Orlando, FL, USA

    Gary T. Leavens

Authors
  1. Yuyan Bao
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gary T. Leavens
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gary T. Leavens .

Editor information

Editors and Affiliations

  1. Department of Computer Science, ETH Zürich, Zürich, Switzerland

    Peter Müller

  2. Institut für Softwaretechnik und Fahrzeuginformatik, Technische Universität Braunschweig, Braunschweig, Germany

    Ina Schaefer

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Bao, Y., Leavens, G.T. (2018). A Methodology for Invariants, Framing, and Subtyping in JML. In: Müller, P., Schaefer, I. (eds) Principled Software Development. Springer, Cham. https://doi.org/10.1007/978-3-319-98047-8_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-98047-8_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-98046-1

  • Online ISBN: 978-3-319-98047-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation