[Prev][Next][Index][Thread]
Re: subject reduction fails in Java -- how it CAN be proven
We at IC were quite surprised and intrigued by the counterexample
to the subject reduction property in Java. Indeed, we did not expect
the interaction of conditional expressions and method calls
to produce that effect.
On the other hand,
a) we feel that this problem is due to the type rule for conditionals
being too weak (it should say that the type of the conditional is
the most specific supertype of the two branches)
b) subject reduction can be proven, namely
> ... it seems, their proof methods cannot easily
> be extended to deal with the full Java language including conditional
> expressions.
our proof can easily be extended to deal with
conditional expressions. Namely, we can apply the same trick
which we developed for type checking assignments (suggested by Don
Syme),
whereby we have different type rules for the compiled
language (Java_SE), than for the run-time language (Java_R).
In more detail:
1. In Java_SE require for
( b ? e1 : e2 )
that b is boolean; e1, e2 have such types that one can
be widened to the other.
That is:
b : boolean
e_1 : T_1
e_2 : T_2
(T_1 widens to T_2 and T_2=T)
or (T_2 widens to T_1 and T_1=T)
----------------------------------------
( b ? e_1 : e_2 ) : T
2. In Java_R we only require for
( b ? e1 ? e2 )
that b is boolean; e_1 and e_2 are well-typed and the whole
expression has the minimal type to which those of
e_1 and e_2 can be widened.
That is:
b : boolean
e_1 : T_1
e_2 : T_2
T = min { T' |
T_1 widens to T', and T_2 widens to T')
------------------------------------------------
( b ? e_1 : e_2 ) : T
3. We prove that for a Java_SE term t
with \Gamma |-_{se} t : T using the Java_SE type
rules,
it also holds that
\Gamma |-_{r} t : T this time using the Java_R type
rules
4. We can now prove the subject reduction theorem stating, that
for a well typed Java_R term t, and a well-typed Java_SE
program p, rewriting t (which might invoke methods from p)
preserves types up to widening.
Furthermore, I believe that the type rule suggested for Java_R is the
rule that _should_ be given for the type of conditional expressions,
and that the actual type (as described for Java_SE) is an easy
approximation to it, which allows an easier implementation of the
compiler.
The suggestion given by Haruo Hosoya, Benjamin Pierce and David Turner,
>
> Integer i = new Integer();
> HashTable h = new HashTable();
> Object o = (b ? (Object)i : (Object)h);
>
> carrying the parameter types along explicitly during the substitution
is more concise, but, I feel, it is less faithful to what
really happens at run-time, since a conditional expression does
not require run-time checks, whereas the conditional as
transformed above does require run-time checks (which are guaranteed to
succeed).
Also, I feel that this feature of conditional expressions is another
indication that the approach of distinguishing the compiled language
from the run-time language (due to Don Syme, again), where typing
in the first reflects the compile - time checks whereas
typing in the latter serves the requirements of formulating and
proving soundness properties, is a useful vehicle when
considering full, "real-world" languages.
Greetings,
Sophia Drossopoulou
> CITATIONS
> ---------
....
> [2] Drossopolou and Eisenbach, "Java is type safe -- probably," ECOOP
> '97.
please, consider our more recent work:
Drossopoulou and Eisenbach:
"Towards an Operations Semantics and Proof of Type Soundness for Java"
April 1998, the most recent version of the previous work, in which we
clarify and simplify many issues. This paper will appear as a chapter
in a book. Also available at:
http://www-dse.doc.ic.ac.uk/projects/slurp/papers.html
--
Dr. Sophia Drossopoulou tel: +44 171 594 8368
http://www-ala.doc.ic.ac.uk/~scd/
Department of Computing fax: +44 171 581 8024
Imperial College of Science, Technology and Medicine
LONDON SW7 2BZ, England email: sd@doc.ic.ac.uk
--
Dr. Sophia Drossopoulou tel: +44 171 594 8368
http://www-ala.doc.ic.ac.uk/~scd/
Department of Computing fax: +44 171 581 8024
Imperial College of Science, Technology and Medicine
LONDON SW7 2BZ, England email: sd@doc.ic.ac.uk