[Prev][Next][Index][Thread]

paper on the soundness of the Java type system


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

A paper arguing the soundness of the Java type system is now
available by anonymous ftp from 
	directory:	/vol/ftp/pub/papers/S.Drossopoulou
	file:		JavaSound.ps

It is still "work in progress", and we expect to be updating it  
regularly, improving the English and removing typos, but
we believe that the formalisms and proofs are correct and stable.

Regards,

Sophia Drossopoulou  and Susan Eisenbach, Imperial College 


Abstract
========
We  argue that the Java type system is sound, by proving a subject 
reduction theorem. We define a subset of Java, a language which is safe and 
which  reflects the most essential features of Java, a term rewriting system 
for the operational semantics and a type inference system to describe compile 
time type checking. We prove that program execution preserves the types, up 
to the subclass/subinterface relationship.

In this paper we consider the following parts of the
Java language: primitive types, classes and inheritance, instance
variables and instance methods, interfaces, shadowing of instance variables,
and dynamic method binding. We plan to extend our study, starting with arrays
and the associated dynamic checks,  until we either have covered all of
Java -- or we have uncovered loopholes  in the
type system.

As an interesting subsidiary result, we formulated and prove two
important properties  which  any compile-time correct Java program
must satisfy:
	* the requirement for any class which according to
	the type rules widens another interface or class
	to provide an implementation for any method declared in that 
	superinterface or superclass 
	
	* the substitution property for compiled Java expressions