Abstract
In this article we present Bali, the formalization of a large (hitherto sequential) sublanguage of Java. We give its abstract syntax, type system, well-formedness conditions, and an operational evaluation semantics. Based on these definitions, we can express soundness of the type system, an important design goal claimed to be reached by the designers of Java, and prove that Bali is indeed type-safe.
All definitions and proofs have been done formally in the theorem prover Isabelle/HOL. Thus this article demonstrates that machine-checking the design of non-trivial programming languages has become a reality.
This is a completely revised and extended version of [NO98].
Research supported by DFG SPP Deduktion.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ole Agesen, Stephen N. Freund, and John C. Mitchell. Adding type parameterization to the Java language. In ACM Symp. Object-Oriented Programming: Systems, Languages and Applications, 1997.
Kim B. Bruce, Jon Crabtree, Thomas P. Murtagh, Robert van Gent, Allyn Dimock, and Robert Muller. Safe and decidable type checking in an objectoriented language. In Proc. OOPSLA’93, volume 18 of ACM SIGPLAN Notices, pages 29–46, October 1993.
Robert S. Boyer and J Strother Moore. A Computational Logic Handbook. Academic Press, 1988.
Kim B. Bruce. Safe type checking in a statically-typed object-oriented programming language. In Proc. 20th ACM Symp. Principles of Programming Languages, pages 285–298. ACM Press, 1993.
Egon Börger and Wolfram Schulte. A programmer friendly modular definition of the dynamic semantics of Java. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, Lect. Notes in Comp. Sci. Springer-Verlag, 1998. Chapter 11 of this volume.
Kim B. Bruce, Robert van Gent, and Angela Schuett. PolyTOIL: A typesafe polymorphic object-oriented language. In ed]W. Olthoff, editor, ECOOP’ 95, volume 952 of Lect. Notes in Comp. Sci., pages 27–51. Springer-Verlag, 1995.
Martin Büchi and Wolfgang Weck. Java needs compound types. Technical Report 182, Turku Center for Computer Science, May 1998. http://www.abo.fi/~mbuechi/publications/CompoundTypes.html.
Richard M. Cohen. The defensive Java Virtual Machine specification. Technical report, Computational Logic Inc., 1997. Draft version.
William Cook. A proposal for making Eiffel type-safe. In Proc. ECOOP’89, pages 57–70. Cambridge University Press, 1989.
Sophia Drossopoulou and Susan Eisenbach. Is the Java type system sound? In Proc. 4th Int. Workshop Foundations of Object-Oriented Languages, January 1997.
Sophia Drossopoulou and Susan Eisenbach. Java is type safe — probably. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, Lect. Notes in Comp. Sci. Springer-Verlag, 1998. Chapter 3 of this volume.
Drew Dean. The security of static typing with dynamic linking. In Proc. 4th ACM Conf. Computer and Communications Security. ACM Press, 1997.
James Gosling, Bill Joy, and Guy Steele. The Java Language Specfication. Addison-Wesley, 1996.
M.J.C. Gordon and T.F. Melham. Introduction to HOL: a theorem-proving environment for higher order logic. Cambridge University Press, 1993.
John Harrison. Proof style. Technical Report 410, University of Cambridge Computer Laboratory, 1997.
Andrew C. Myers, Joseph A. Bank, and Barbara Liskov. Parameterized types for Java. In Proc. 24th ACM Symp. Principles of Programming Languages, pages 132–145, 1997.
Robin Milner. A theory of type polymorphism in programming. J. Comp. Sys. Sci., 17:348–375, 1978.
Wolfgang Naraschewski and Tobias Nipkow. Type inference verified: Algorithm W in Isabelle/HOL. In C. Paulin-Mohring, editor, Proc. Int. Workshop TYPES’96, volume 1??? of Lect. Notes in Comp. Sci. Springer-Verlag, 1997. To appear.
Tobias Nipkow and David von Oheimb. Javalight is type-safe — definitely. In Proc. 25th ACM Symp. Principles of Programming Languages, pages 161–170. ACM Press, 1998.
Martin Odersky and Philip Wadler. Pizza into Java: Translating theory into practice. In Proc. 24th ACM Symp. Principles of Programming Languages, pages 146–159, 1997.
Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lect. Notes in Comp. Sci. Springer-Verlag, 1994.
Konrad Slind. Function definition in higher order logic. In J. vonWright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics, volume 1125 of Lect. Notes in Comp. Sci., pages 381–397. Springer-Verlag, 1996.
Donald Syme. DECLARE: A prototype declarative proof system for higher order logic. Technical Report 416, University of Cambridge Computer Laboratory, 1997.
Donald Syme. Proving Java type soundness. Technical Report 427, University of Cambridge Computer Laboratory, 1997.
Donald Syme. Proving Java type soundness. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, Lect. Notes in Comp. Sci. Springer-Verlag, 1998. Chapter 4 of this volume.
Myra VanInwegen. Towards type preservation for core SML. University of Cambridge Computer Laboratory, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
von Oheimb, D., Nipkow, T. (1999). Machine-Checking the Java Specification: Proving Type-Safety. 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_4
Download citation
DOI: https://doi.org/10.1007/3-540-48737-9_4
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