Re: subject reduction fails in Java -- how it CAN be proven

At 3:57 PM 19/6/98, Robert O'Callahan wrote:

>> 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)
>Unfortunately that's not possible. Two Java types may not have a most
>specific supertype, e.g. the classes X and Y:
>interface A { ... }
>interface B { ... }
>class X implements A, B { ... }
>class Y implements A, B { ... }
>The most specific supertype would be the combination of the two interfaces
>A and B, but that is not a Java type.
>This has already come up at the bytecode level ... see the work of Qian.
>The solution is obviously to fix the definition of a type --- not a problem
>if we're just talking about proof machinery, but perhaps more serious if it
>means a change to the language definition.

At the byecode level, one can define a "type" to be a class and a set of
interfaces (this is the strategy we have used in the JAWS project).  The
LUB of X and Y is then the pair (Object,{A,B}).

One could apply this strategy at the source code level, but only by creating
a new class during the rewriting process which X and Y extend (acceptable for
the purposes of static partial evaluation, but not very nice):

abstract class XY implements A, B { }

class X extends XY implements A, B { ... }

class Y extends XY implements A, B { ... }

This rewriting of the program as a whole doesn't alter the semantics: it just
makes a new LUB possible.

Tony Dekker

Anthony Dekker      dekker@ACM.org      http://www.acm.org/~dekker/

PO Box 3925, Manuka ACT 2603, AUSTRALIA