[Prev][Next][Index][Thread]
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
--------------------------------------------------------------------