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.