Re: Type soundness issues in Java

I tested Martin's example (below) on the Metrowerks compiler (and IDE)
running on a Macintosh.  It reports a compile-time error when the
"implements I" after I dropped it from class A and selected "run".  It
no doubt succeeds at this because it keeps track of dependencies and
recompiles what it thinks needs recompiling when I ask it to run
(e.g., it has the equivalent of its own dynamically configured make
file).  This is obviously the right thing to do as changes to the
interface of a class change what should be legal in other classes.
The Java specification should obviously be rewritten to handle this

As for the problems with the collection classes, a number of people
(most prominently Joe Bergin in my experience) complained bitterly
about having classes optionally implement parts of interfaces.  This
is clearly a bad design decision for a class.  I'm not sure that this
is something that can be blamed on the language, as opposed to the
library designers.  Practically, it seems useful to allow a class of
exceptions which do not have to be handled or declared as they might
otherwise have to appear everywhere (though they clearly should
terminate the program if raised and not handled).  However, using such
exceptions for this kind of error certainly seems to be very bad

	Kim Bruce

> Date: Sun, 16 May 1999 14:02:03 +0300
> To: types@cis.upenn.edu
> From: Martin Buechi <Martin.Buechi@abo.fi>
> Subject: Type soundness issues in Java
> 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 
> 	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 
> not implement interface I
>         at Main.main(Compiled Code)
> --

> 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.
> ====================================================================