A Type System For Object Initialization 
              In the Java Virtual Machine Bytecode Language
		
                    Stephen Freund and John Mitchell
                          Stanford University
                  {freunds,mitchell}@cs.stanford.edu 


The Java language enables the creation of portable, compact programs which 
can be transmitted over a network and run safely on any computer.  To 
support this paradigm, Java compilers typically translate a Java program 
into an intermediate language which can be interpreted by any Java Virtual 
Machine.  This intermediate language is a typed, machine-independent 
bytecode language, and it is the foundation for many of Java's features, 
including portability across platforms, dynamic type resolution, and 
run-time type safety.  Despite the bytecode language's important role in 
the success of Java, there is no formal definition of its type system.  
This paper develops a sound type system for a small set of ten bytecode 
instructions.  These instructions are sufficient to study the type rules 
associated with object creation and initialization.

We begin by developing a model of the Java Virtual Machine's bytecode 
interpreter using the standard framework of structured operational 
semantics.  We model execution using a simplified abstract machine for 
which each bytecode instruction is characterized by a transformation of 
machine states.  We then formulate syntax-directed type rules for the 
bytecodes in our language.  These rules are fairly complex due to certain 
features of the bytecode language.  For example, local variables may have 
different types at different locations within a method.  Also, there are 
specific rules governing the use of allocated, but not initialized, 
objects.  We show our type system is sound by proving that any well-typed 
program will not produce a run-time type error.  

This paper is part of an effort to specify a type system for the whole 
bytecode language, and it builds on the previous work of Stata and Abadi.  
Once this system has been developed, it can be used to study the impact of 
possible extensions or changes to the Java language and to formally specify 
type safety for a compiled Java program.  In addition, this study may lead 
to more expressive, but simpler, typed intermediate languages in the 
future.

Special thanks to Martin Abadi and Raymie Stata (DEC SRC) for their
assistance on this project.