RE: Type soundness issues in Java

Thanks for all the answers. I would like to share three observations:

1. Verification is delayed as far as possible
It seems that verification is, presumably for optimization, delayed as far
as possible. This seems to explain the observed behavior. If one forces
I.class to be loaded, e.g. by introducing a class B similar to A and
invoking one of its methods via I as below, the
IncompatibleClassChangeError is still raised at the same point.

public class Main {

        public static void main(String args[]) {
                A a = new A();
                I i = new B();
                i.m(); // force I.class to be loaded,
		       //  but might not be linked with A yet
                System.out.println("I've been started");

2. Type soundness violations that are not exploited go unnoticed
The second issue was brought to my attention by Christian Horn. If we do
not exploit the type soundness violation ---but still use the value of i---
than the violation will never be detected. The following Main2 should be
compiled against I.java and A.java from the previous posting and then
A.java recompiled with "implements I" removed:

public class Main2 {
        public static void main(String args[]) {
                A a=new A();
                I i;
                i=a; // type soundness violation
                A aa;
                aa=(A)i; // we use "i", but in a sound way

This issue is not due to an optimization by javac. It might --of course--
be optimized away by a JVM:

Method void main(java.lang.String[])
   0 new #1 <Class A>
   3 dup
   4 invokespecial #4 <Method A()>
   7 astore_1
   8 aload_1
   9 astore_2
  10 aload_2
  11 checkcast #1 <Class A>
  14 astore_3
  15 aload_3
  16 invokevirtual #6 <Method void m()>
  19 return

3. The abuse of exceptions to signal not implemented methods is worse
Whereas the above type soundness issue in conjunction with binary
compatibility is definitely interesting, I am personally more worried about
the bad example set by the abuse of exceptions to signal unimplemented
methods in JCF.



Abo Akademi University          | mailto:Martin.Buechi@abo.fi
Department of Computer Science  | phone: +358 (0)2 215-4034
Lemminkaisenkatu 14a            | fax:   +358 (0)2 215-4732
20520  Turku                    | www:   http://www.abo.fi/~mbuechi/
FINLAND                         | time:  UTC +0300
    Kokko, kokoo kokoon koko kokko! Koko kokkoko? Koko kokko!