Abstract
Java combines the experience from the development of several object oriented languages, such as C++, Smalltalk and Clos. The philosophy of the language designers was to include only features with already known semantics, and to provide a small and simple language.
Nevertheless, we feel that the introduction of some new features in Java, as well as the specific combination of features, justifies a study of the Java formal semantics. The use of interfaces, reminiscent of [10,6] is a simplification of the signatures extension for C++ [4] and is — to the best of our knowledge — novel. The mechanism for dynamic method binding is that of C++, but we know of no formal definition. Java adopts the Smalltalk [15] approach whereby all object variables are implicitly pointers.
Furthermore, although there are a large number of studies of the semantics of isolated programming language features or of minimal programming languages [1], [31], [34], there have not been many studies of the formal semantics of actual programming languages. In addition, the interplay of features which are very well understood in isolation, might introduce unexpected effects.
Experience confirms the importance of formal studies of type systems early on during language development. Eiffel, a language first introduced in 1985, was discovered to have a loophole in its type system in 1990 [9,22]. Given the growing usage of Java, it seems important that if there are loopholes in the type system they be discovered early on.
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
M. Abadi and L. Cardelli. A Semantics of Object Types. In LICS’94 Proceedings, 1994.
Ole Ageson, Stephen Freunds, and John C. Mitchell. Adding paraleterized types to Java. In OOPSLA’97 Proceedings, 1997.
Joseph A. Bank, Barbara Liskov, and Andrew C. Myers. Parameterized Types and Java. In POPL’97 Proceedings, January 1997.
Gerald Baumgartner and Vincent F. Russo. Signatures: A language extension for improving type abstraction and subtype polymorphism in C++. Software-Practice & Experience, 25(8):863–889, August 1995.
John Boyland and Giuseppe Castagna. Type-Safe Compilation of Covariant Specialization: A Practical Case. In ECOOP’96 Proceedings, July 1996.
P. Canning, William Cook, and William Olthoff. Interfaces for object-oriented programming. In OOPLSA’89, pages 457–467, 1989.
Giuseppe Castagna. Parasitic Methods: Implementation of Multimethods for Java. Technical report, C.N.R.S, November 1996.
Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A calculus for over-loaded functions with subtyping. Information and Computation, 117(1):115–135, 15 February 1995.
William Cook. A Proposal for making Eiffel Type-safe. In S. Cook, editor, ECOOP’87 Proceedings, pages 57–70. Cambridge University Press, July 1989.
William Cook, Walter Hill, and Peter Canning. Inheritance is not Subtyping. In POPL’90 Proceedings, January 1990.
Luis Damas and Robin Milner. Principal Type Schemes for Functional Languages. In POPL’82 Proceedings, 1982.
Sophia Drossopoulou and Susan Eisenbach. Is the Java type system sound? In Fourth International Workshop on Foundations of Object-Oriented Languages, January 1997.
Sophia Drossopoulou and Susan Eisenbach. Java is type safe — probably. In Proceedings of the European Conference on Object-Oriented Programming, June 1997.
Sophia Drossopoulou, Susan Eisenbach, and Sarfraz Khurshid. Is Java Sound? Theory and Practice of Object Systems, 1998. to appear, available athttp://www-dse.doc.ic.ac.uk/projects/slurp/.
A. Goldberg and D. Robson. SmallTalk-80: The Language and Its Implementation. Addison-Wesley, 1983.
M. Gordon and T.F. Melhams, editors. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.
James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison-Wesley, August 1996.
R. Harper. A simplified account of polymorphic references. Technical Report CMU-CS-93-169, Carnegie Mellon University, 1993.
Daniel Ingalls. The Smalltalk-76 programming system design and implementation. In POPL’78 Proceedings, pages 9–15, January 1978.
The Java Language Specification, May 1996.
Sarfraz Khurshid. Some Aspects of Type Soundness for Java, 1997. BSc thesis.
Bertrand Meyer. Static typing and other mysteries of life, http://www.eiffel.com 1995.
Tobias Nipkow and David von Oheimb. Javalight is type-safe — definitely. In POPL Proceedings, 1998.
Martin Odersky and Philip Wadler. Pizza into Java: Translating theory into practice. In POPL’97 Proceedings, January 1997.
Peter Sellinger. private communication, October 1996.
Donald Syme. DECLARE: A Prototype Declarative Proof System for Higher Order Logic. Technical Report 416, Cambridge University, March 1997.
Donald Syme. Private Communication, 1997.
Donald Syme. Proving Java Type Sound. Technical Report 427, Cambridge University, June 1997.
Donald Syme. Proving Java Type Sound. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, Lecture Notes in Computer Science. Springer-Verlag, 1998. Chapter 4 of this volume.
Mads Tofte. Type Inference for Polymorphic References. In Information and Computation’80 Conference Proceedings, pages 1–34, November 1980.
Myra VanInwegen. Towards Type Preservation in Core SML. Technical report, Cambridge University, 1997.
David von Oheimb and Tobias Nipkow. Machine-checking the Java Specification: Proving Type-Safety. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, Lecture Notes in Computer Science. Springer-Verlag, 1998. Chapter 5 of this volume.
David Wragg, Sophia Drossopoulou, and Susan Eisenbach. Java Binary Compatibility is Almost Correct. Technical report, Imperial College, 1998. http://www-dse/projects/SLURP/bc.
Andrew Wright and Matthias Felleisen. A Syntactic Approach to Type Soundness. Information and Computation, 115(1), 1994.
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
Drossopoulou, S., Eisenbach, S. (1999). Describing the Semantics of Java and Proving 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_2
Download citation
DOI: https://doi.org/10.1007/3-540-48737-9_2
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