Skip to main content
SpringerLink
Log in

Proving Java Type Soundness

  • Chapter
  • First Online:
Book cover Formal Syntax and Semantics of Java

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1523))

Abstract

This chapter describes a machine checked proof of the type soundness of a subset of Java (we call this subset JavaS). In Chapter 3, a formal semantics for approximately the same subset was presented by Drossopoulou and Eisenbach. The work presented here serves two roles: it complements the written semantics by correcting and clarifying some details; and it demonstrates the utility of formal, machine checking when exploring a large and detailed proof based on operational semantics.1 This work contributes to three distinct fields of formal reasoning:

  • -The Formal Study of Java: We contribute a detailed analysis of a significant property of Java, and provide corrections to proofs that are interesting in their own right.

  • -Tools for Formal Methods: This work is a major case study in so-called ‘declarative’ proof techniques. The tool we use, called DECLARE [Sym97], has been developed by the author to demonstrate the utility of these techniques.

  • -Formally Checked Properties of Languages: This work contributes a tool and a methodology for the general task of machine checking properties of languages.

Most of this chapter should be clear to readers with a basic understanding of operational semantics, formal specification and the results presented in Chapter 3.

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. Juanito Camilleri and Tom Melham. Reasoning with inductively defined relations in the HOL theorem prover. Technical Report 265, University of Cambridge Computer Laboratory, Cambridge, CB2 3QG, U.K., August 1992.

    Google Scholar 

  2. Sophia Drossopoulou and Susan Eisenbach. Is the Java type system sound? (version 2.01). Technical report, Imperial College, University of London, Cambridge, CB2 3QG, U.K., January 1997. This version was distributed on the Internet. Please contact the authors if a copy is required for reference.

    Google Scholar 

  3. James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison-Wesley, 1996.

    Google Scholar 

  4. M.J.C Gordon and T.F Melham. Introduction to HOL: A Theorem Proving Assistant for Higher Order Logic. Cambridge University Press, 1993.

    Google Scholar 

  5. John Harrison. HOL light: A tutorial introduction. In Mandayam Srivas and Albert Camilleri, editors, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD’96), volume 1166 of Lecture Notes in Computer Science, pages 265–269. Springer-Verlag, 1996.

    Chapter  Google Scholar 

  6. John R. Harrison. Proof Style. Technical Report 410, University of Cambridge Computer Laboratory, Cambridge, CB2 3QG, U.K., January 1997.

    Google Scholar 

  7. D. W. Loveland. Mechanical Theorem Proving by Model Elimination. Journal of the ACM, 15:236–251, 1968.

    Article  MATH  MathSciNet  Google Scholar 

  8. S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking and model checking. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV’ 96, volume 1102, pages 411–414. Springer-Verlag, July/August 1996.

    Google Scholar 

  9. L. C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361–385. Academic Press, 1990.

    Google Scholar 

  10. Lawrence C. Paulson. A Fixed Point Approach to Implementing (Co)inductive Definitions. 18th International Conference on Automated Deduction, pages 148–161, 1994.

    Google Scholar 

  11. Roly Perera and Peter Bertelsen. The Unoffcial Java Bug Report, June 1997. Published on the WWW at http://www2.vo.lu/homepages/gmid/java.htm.

  12. Gordon D. Plotkin. A structural approach to operational semantics. Technical report, Computer Science Department, Aarhus University, DK-8000 Aarhus C. Denmark, September 1991.

    Google Scholar 

  13. Zhenyu Qian. A Formal Specification of Java Virtual Machine Instructions. Technical report, UniversitÄt Bremen, FB3 Informatik, D-28334 Bremen, Germany, November 1997.

    Google Scholar 

  14. P. Rudnicki. An Overview of the MIZAR Project, 1992. Unpublished; available by anonymous FTP from menaik.cs.ualberta.ca as pub/Mizar/Mizar_Over.tar.Z.

    Google Scholar 

  15. Don Syme. DECLARE: A prototype declarative proof system for higher order logic. Technical Report 416, University of Cambridge Computer Laboratory, Cambridge, CB2 3QG, U.K., March 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK

    Don Syme

Authors
  1. Don Syme
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Center for Secure and Dependable Software, University of Idaho, Moscow, ID, 83844-1010, USA

    Jim Alves-Foss

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Syme, D. (1999). Proving Java Type Soundness. In: Alves-Foss, J. (eds) Formal Syntax and Semantics of Java. Lecture Notes in Computer Science, vol 1523. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48737-9_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-48737-9_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66158-0

  • Online ISBN: 978-3-540-48737-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation