Formal model for defender method resolution

[Brian Goetz]

Dan Smith has pointed out a hole in the Featherweight Defenders 
document; there is an unsound disconnect introduced when we allow 
covariant overriding but don't require the implementation to be replaced 
(rules T-IntNoDef and T-ClassAbs).  This would allow the following failure:

   k1 : Object
   intf A { Object m() default k1 }
   intf B extends A { String m() }

Here, the default for A is going to produce a result that does not meet 
B's interface contract.  I believe what is needed is additional 
constraints on T-IntNoDef to include a
   \Gamma(mdef(I_i)) <: T
constraint (for the cases where mdef(I_i) is not nil).

I think this is all that is needed to plug this hole.

On 1/19/2011 12:48 PM, Brian Goetz wrote:
> At
>     http://cr.openjdk.java.net/~briangoetz/lambda/featherweight-defenders.pdf
>
> I have posted a draft of a formal model for resolution of defender
> methods.  This is written in the style of "Featherweight Java"
> (Igarashi, Pierce, et al), in which a number of real-world language
> concerns are abstracted away, in order to simplify the formalism for the
> portion of the language of interest, notably the typing and resolution
> of defender methods.
>
> Hopefully this will serve as a basis for discussion of the proposal.
>
> The T- and S- rules are implemented by the compiler and are used for
> typing; the R- rules are implemented by the VM to do method selection.
> (The primary computed item of interest is mres(C), which is the method
> resolution for a given class -- while this is not used in any further
> production (it would be used if the operational semantics were
> specified), it is in fact the whole point of this exercise.)
>
>