[Prev][Next][Index][Thread]
Type soundness issues in Java
Type soundness in Java has received quite a bit of attention, with a number
of proofs both for the language and the byte code. However, I recently
stumbled over two practical type soundness problems that don't seem to be
covered by the above work or by any binary compatibility publications that
I am aware of:
1.Failure of type soundness in combination with binary compatibility
--------------------------------------------------------------------
I have stumbled over what I consider to be a failure of type soundness in
Java. The problem is exposed in combination with binary compatibility.
However, since Java even defines an exception for this case, I am wondering
how type soundness is really defined in Java. Or is this just an
implementation error, that is present in all JVM's that I have tested?
Here goes the example:
-- I.java
interface I {
int c=4;
void m();
}
-- A.java
public class A implements I { // "implements I" commented out for recompilation
public void m() {
System.out.println("m");
}
}
-- Main.java
public class Main {
public static void main(String args[]) {
A a = new A();
I i;
System.out.println("I've been started");
if(a instanceof I)
System.out.println("a is instance of I!");
else
System.out.println("a Is NOT instance of I");
i=a;
System.out.println("Cast succeeded!");
System.out.println(java.lang.Integer.toString(i.c,10));
i.m();
}
}
--
I have tested this under JDK 1.2 on Solaris 2.6 (as well as JDK 1.1.7 on
Solaris and under Netscape 4.07 and on the Mac MRJ 2.0):
First we compile everything:
% /opt/jdk_1.2/bin/javac Main.java
Then we comment out "implements I" in A.java, save it, and recompile only
A.java.
% /opt/jdk_1.2/bin/javac A.java
Then we run it.
% /opt/jdk_1.2/bin/java Main
I've been started
a Is NOT instance of I
Cast succeeded!
4
Exception in thread "main" java.lang.IncompatibleClassChangeError: class A does
not implement interface I
at Main.main(Compiled Code)
--
The interesting thing is that the assignment i=a succeeds, even though the
run-time type of a is A and A does not implement I, as correctly noted by
the previous output statement. At this point I consider type soundness to
be broken.
That i.c doesn't cause any error isn't really surprising because its value
is independent of the value of i. It works even if i is null.
The method call i.m() finally produces the expect error message. So the
type system indicates the problem and prevents any damage from happening.
However, I think that this error message should occur at the point where we
(try to) assign a to i.
This issue is actually discussed in Sect. 13.4.4 of the Java Language
Specification:
"Changing the direct superclass or the set of direct superinterfaces of a
class type will not break compatibility with pre-existing binaries,
provided that the
total set of superclasses or superinterfaces, respectively, of the class
type loses no members."
"If a change to the direct superclass or the set of direct superinterfaces
results in any class or interface no longer being a superclass or
superinterface, respectively, then link-time errors may result if
pre-existing binaries are loaded with the binary of the modified class."
A similar example follows, but with an explicit superclass removed/replaced
by Object. The manual claims that in this case: "... then a VerifyError is
thrown at link time."
However, the case of removing an interface is not explicitly mentioned.
Although I believe it should be treated similarly.
Have I just overlooked something else in the manuals, or has this problem
been documented before? (I checked the type soundness and binary
compatibility papers of Drossopoulou, Eisenbach, Wragg, von Oheimb, and
Nipkow, but didn't find anything.)
2. Practical undermining of type soundness by "bad" programming practice
------------------------------------------------------------------------
The second issue concerns the advocated programming style of the Java
Collections Framework (JCF)
(http://java.sun.com/products/jdk/1.2/docs/guide/collections/overview.html):
"All of the modification methods in the collection interfaces are labeled
optional. Some implementations may not perform one or more of these
operations, throwing a runtime exception (UnsupportedOperationException) if
they are attempted. Implementations must specify in their documentation
which optional operations they support. Several terms are introduced to aid
in this specification."
What is the difference from the client's perspective between an object
explicitly throwing a UnsupportedOperationException as advocated in JCF and
an automatically generated "no such method" in an untyped/not type sound
language?
(UnsupportedOperationException being a subclass of
java.lang.RuntimeException, methods are not even required to declare in
their throws clause that this type of exceptions might be thrown during the
execution of the methods but not caught. Anyhow, I am not sure if it would
make a big practical difference if UnsupportedOperationException would have
to be listed in the throws clause.)
I don't believe too much in the "Implementations must specify in their
documentation which optional operations they support" either because the
documentation is not fed to the compiler and, therefore, easily ignored.
In a strongly type language with by-name equivalence for types, I would
like to use types to stand for explicit external specifications (behavioral
typing). If we introduce UnsupportedOperationException's we have to reduce
the specifications to "does the desired thing or throws an exception",
where the "or" stands for a demonic choice. Hence, no meaningful properties
can be proved anymore. Therefore, I personally believe that the much
acclaimed JCF sets a bad example by promoting the practical undermining of
type soundness.
I think that the solution to the JCF design problem would be to introduce
many smaller interfaces (e.g. CollectionWithoutModification, CollectionAdd,
CollectionRemove) grouping related methods, that are likely to be fully or
not at all implemented,that are then combined. Of course, I would advocate
compound types (Martin Büchi and Wolfgang Weck. Compound Types for Java.
Proceedings of OOPSLA'98. Pages 362-373. ACM Press, 1998 [End of own paper
ad :)]) or a similar mechanism to avoid cluttering the name space with all
the combinations required because of strict by-name type equivalence.
Yours,
Martin
====================================================================
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
--------------------------------------------------------------------
Make something idiot proof, and someone will build a better idiot.
====================================================================