Skip to main content
SpringerLink
Log in

Proving Theorems About JML Classes

  • Chapter
Formal Methods and Hybrid Real-Time Systems

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4700))

Abstract

We present an initial link between Z and JML that has enabled us to use Z/Eves to prove theorems about JML classes. We have applied this to the JML type system and the Java HashMap class from the Java Collections Framework. We present and discuss the issues behind a more general strategy for translation in both directions between Z and JML. This work is a contribution to the Verified Software Repository, part of the Grand Challenge in Verified Software.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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. Back, R.J., von Wright, J.: Refinement Calculus: A Systematic Introduction. In: Graduate Texts in Computer Science, Springer, Heidelberg (1998)

    Google Scholar 

  2. Bloch, J.: Effective Java Programming Language Guide. Prentice Hall, Englewood Cliffs (2001)

    Google Scholar 

  3. 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. STTT 7(3), 212–232 (2005)

    Article  Google Scholar 

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

    Google Scholar 

  5. Butterfield, A., Woodcock, J.: Formalising flash memory: first steps. In: 12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007), Auckland, New Zealand, July 11-14, 2007, IEEE Computer Press, Los Alamitos (2007)

    Google Scholar 

  6. Cavalcanti, A.L.C.: A Refinement Calculus for Z. DPhil Thesis. University of Oxford (1997)

    Google Scholar 

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

    MATH  Google Scholar 

  8. Freitas, L., Cavalanti, A.L.C., Woodcock, J.C.P.: Taking our own medicine: applying the refinement calculus to state-rich refinement model checking. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 697–716. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  9. Freitas, L., et al.: Verified Software Repository @ SourceForge (2006), vsr.sourceforge.net

  10. Freitas, L., Fu, Z., Woodcock, J.: POSIX file store in Z/Eves: an experiment in the verified software repository. In: 12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007), Auckland, New Zealand, July 11–14, 2007, IEEE Computer Press, Los Alamitos (2007)

    Google Scholar 

  11. Fu, Z.: A Refinement of the UNIX Filing System using Z/Eves. Master’s thesis, University of York (2006)

    Google Scholar 

  12. Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison Wesley, Reading (2005)

    Google Scholar 

  13. Hoare, T.: The Verifying Compiler Software Grand Challenge. Journal of the ACM 50(1), 63–69 (2003)

    Article  Google Scholar 

  14. Hoare, C.A.R., He, J.: Unifying Theories of Programming. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  15. Huisman, M., Jacobs, B., van den Berg, J.: A Case study in class library verification: Java’s Vector class. In: Moreira, A.M.D., Demeyer, S. (eds.) Object-Oriented Technology. ECOOP’99 Workshop Reader. LNCS, vol. 1743, pp. 109–110. Springer, Heidelberg (1999)

    Google Scholar 

  16. Huisman, M.: Reasoning about Java Programs in Higher-Order Logic using PVS and Isabelle. PhD thesis, Universiteit Nijmegen (2001)

    Google Scholar 

  17. Huisman, M.: Verification of Java’s AbstractCollection class: a case study. In: Boiten, E.A., Möller, B. (eds.) MPC 2002. LNCS, vol. 2386, pp. 175–194. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  18. IBM: CICS Application Programming Interface Release 3. Technical Report SC33-1688-01, IBM Hursley Park (1999)

    Google Scholar 

  19. Intel Corp.: Open NAND Flash Interface Specification. Open NAND Flash Interface Consortium (2007), http://www.onfi.org/

  20. ISO/IEC 13568: Information Technology—Z Formal Specification Notation—Syntax, Type System and Semantics. First edn. ISO/IEC (2002)

    Google Scholar 

  21. Josey, A. (ed.): The Single UNIX Specification Version 3. Open Group (2004), ISBN: 193162447X

    Google Scholar 

  22. Joshi, R., Holzmann, G.J.: A mini-challenge: build a verifiable filesystem. In: Verified Software: Theories, Tools, Experiments (VSTTE), IFIP Working Conference, Zurich (in press)

    Google Scholar 

  23. Lakatos, I.: Proofs and Refutations: The Logic of Mathematical Discovery. Cambrdige University Press, Cambrdige (2005)

    Google Scholar 

  24. Leavens, G. T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P.: JML Reference Manual. Iowa State University. Revision 1.200 (2007)

    Google Scholar 

  25. Morgan, C.: Programming from Specifications. Prentice-Hall, Englewood Cliffs (1994)

    MATH  Google Scholar 

  26. Morgan, C., Sufrin, B.: Specification of the UNIX filing system. IEEE Transactions on Software Engineering SE-10, 128–142 (1984)

    Article  Google Scholar 

  27. Paige, R.F., Brooke, P.J.: Integrating BON and Object-Z. Journal of Object Technology 3(3), 121–141 (2004)

    Google Scholar 

  28. Paige, R.F., Ostroff, J.S.: From Z to BON/Eiffel. In: ASE, pp. 209–212 (1998)

    Google Scholar 

  29. Poll, E., van den Berg, J., Jacobs, B.: 3. In: Specification of the JavaCard API in JML. Smart Card Research and Advanced Applications. Proceedings of the Fourth Working Conference on Smart Card Research and Advanced Applications, CARDIS 2000, September 20-22, 2000. Bristol. IFIP Conference Proceedings, vol. 180, pp. 135–154. Kluwer, Dordrecht (2000)

    Google Scholar 

  30. Raghavan, A.D., Leavens, G.T.: Desugaring JML Method Specifications. Technical Report TR#00-03e, Iowa State University, Department of Computer Science 226 Atanasoff Hall Ames Iowa 50011-1041, USA (2005)

    Google Scholar 

  31. Russell, B.: Recent Work in Philosophy of Mathematics. International Monthly (1901) Reprinted in Mysticism and Logic and Other Essays (p.59–74) Barnes & Noble (1976)

    Google Scholar 

  32. Saaltink, M.: Z/Eves 2.0 User’s Guide. ORA Canada, TR-99-5493-06a (1999)

    Google Scholar 

  33. Smith, G.: The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, Dordrecht (2000)

    Google Scholar 

  34. Spivey, J.M.: The Z Notation: A Reference Manual. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  35. SRI: Workshop on the Verification Grand Challenge (2005), http://www.csl.sri.com

  36. Stepney, S., Cooper, D., Woodcock, J.: An Electronic Purse: Specification, Refinement, and Proof. Technical Monograph PRG-126, University of Oxford (2000)

    Google Scholar 

  37. Stepney, S., Polack, F., Toyn, I.: A Z Patterns Catalougue: volume 1. Technical Report YCS349, Department of Computer Science, University of York (2003)

    Google Scholar 

  38. Utting, M., Wang, S.: Object orientation without extending Z. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 319–338. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  39. van den Berg, J., Jacobs, B., Poll, E.: Formal specification and verification of JavaCard’s Application Identifier class. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol. 2041, pp. 137–150. Springer, Heidelberg (2001)

    Google Scholar 

  40. Woodcock, J.C.P., Cavalcanti, A.L.C.: A concurrent language for refinement. In: 5th Irish Workshop on Formal Methods, IWFM 2001, Dublin, Ireland, 16–17 July 2001. BCS Workshops in Computing (2001)

    Google Scholar 

  41. Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1996)

    MATH  Google Scholar 

  42. Woodcock, J., Freitas, L.: Z/Eves and the Mondex Electronic Purse. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 15–34. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of York, UK

    Leo Freitas & Jim Woodcock

Authors
  1. Leo Freitas
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jim Woodcock
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Cliff B. Jones Zhiming Liu Jim Woodcock

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Freitas, L., Woodcock, J. (2007). Proving Theorems About JML Classes. In: Jones, C.B., Liu, Z., Woodcock, J. (eds) Formal Methods and Hybrid Real-Time Systems. Lecture Notes in Computer Science, vol 4700. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75221-9_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-75221-9_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-75220-2

  • Online ISBN: 978-3-540-75221-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation