RE: Type soundness issues in Java
I found Martin's example most interesting, as well as the explanations
from Ole and Phillip.
I would like first to (probably needlessly) clarify that the example
has nothing to do with binary compatibility, since removal of an
interface is not listed as a binary compatible change in the spec. The
example only has to to with the loader and verifier.
Secondly, this example raised (in discussion with Mariangiola
Dezani-Ciancaglini) the following question:
Obviously, and because of the laziness allowed in verification and
loading, different Java implementations may behave differently, and
some will throw exceptions where others might not. So, what about the
claim that Java will have the same behaviour across all platforms?
Could we replace the above claim by the following, weaker one?
Let us consider an eager implementation EI (eager loading and verification).
Then, every program that executes on EI without throwing an unchecked
exception should have the same behaviour on every other implementation.
On the other hand, a program that throws an unchecked exception on some
implementation will also throw an unchecked exception (although not
necessarily the same one) on EI.
(Of course I am ignoring here the issue of different package
implementations across platforms).
The applicability of the above claim would be severy reduced by the
fact that we can handle exceptions in Java. Therefore, the behaviour
of a program that throws an unchecked exception AND handles it cannot
be compared to the behaviour of the same program on EI. The two
implementations could even return different values, or one could
terminate abnormaly and the other could handle the exception and
Sophia Drossopoulou, from Imperial College London, (perm email: firstname.lastname@example.org)
currently visiting Prof. Mariangiola Dezani-Ciancaglini, Univ. Torino
(curr email: email@example.com)