Describing the Semantics of Java and Proving Type Soundness

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 [6,10] 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.