Formal model for defender method resolution

[Brian Goetz]

I have updated the formal model to deal more correctly with covariant 
overrides.  Changes:

  - Break rule T-IntDef into T-IntSimpleOvr and T-IntDefOvr, which deal 
separately with the case of a (potentially) covariant override of a 
method which does not have a default in a superinterface, and an 
override of one that does.  (We can simplify the design by simply 
removing rule T-IntDefOvr, which would have the effect of prohibiting 
any override of a defended method without specifying a new default. 
Doing so would require a syntax like "default I.m()" to allow explicit 
inheritance so as to avoid brittleness.)

  - Break rule T-IntInh into T-IntSimpleInh and T-IntDefInh, which deal 
with implicit (potentially) covariant overrides.  Again, we can simplify 
the design by eliminating rule T-IntDefInh, requiring all potential 
covariant overrides (including the case where a defended version of m() 
is inherited from one parent and a non-defended version is inherited by 
another parent, regardless of covariance) to be explicit.  However this 
might annoy users, who would be forced to explicitly declare a default 
even for simple interfaces like:

   intf A { String m() }
   intf B extends A { String m() default k }
   intf C extends A, B {
     // without T-IntDefInh, need to explicitly redeclare m w/default
   }

  - Fix a bug in R-Defender where T had not been defined.

Current draft at same link:
   http://cr.openjdk.java.net/~briangoetz/lambda/featherweight-defenders.pdf

Old draft renamed to featherweight-defenders-2011-01-19.pdf

On 1/28/2011 2:38 PM, Brian Goetz wrote:
> Thinking more, the logical thing to do is require that a covariant
> override of an extension method in an interface must also provide a new
> default.  The cases where the old default will still be OK (even when it
> is type-correct, which is already rare) under a covariant override seem
> pretty limited.
>
> However, it is a common behavior currently to override a method in an
> interface solely to provide new Javadoc (or annotations).  Currently
> these are a no-op from a language semantics perspective, and I believe
> this is a behavior we should continue to respect.  Hence the current
> implementation (and formal model) interprets
>
> interface A { T m() default k }
> interface B extends A { T m() }  // non-covariant override
>
> as B inheriting A's default, rather than B overriding A's default with
> some magic "no default".  (This is different from the "obvious" analogy
> to concrete classes, where it is permitted to reabstract a concrete
> method.  But such reabstraction for defaults would introduce a lot of
> additional complexity for relatively little value.)
>
> Some people find this "sub-inheritance" (inheritance of part of a
> signature) disturbing, because there is no precedent for it in Java.
>
> What do people think?  Do you find this interpretation of B (m()
> continues to use A's default) confusing or natural (or both)?
>
> On 1/24/2011 11:26 AM, Brian Goetz wrote:
>> 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.)
>>>
>>>
>>
>