[Prev][Next][Index][Thread]

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

Sophia Drossopoulou wrote:
> We at IC were quite surprised and intrigued by the counterexample
> to the subject reduction property in Java. Indeed, we did not expect
> the interaction of conditional expressions and method calls
> to produce that effect.
> 
> On the other hand,
> 
> 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.

Rob
-- 
[Robert O'Callahan (roc+@cs.cmu.edu)        4th year CMU SCS PhD
Home page: http://www.cs.cmu.edu/~roc       1 Samuel 15:22 ---
"But Samuel replied: "Does the Lord delight in burnt offerings and
sacrifices as much as in obeying the voice of the Lord? To obey is
better than sacrifice, and to heed is better than the fat of rams."]