Updated Featherweight Defenders document available

[Brian Goetz]

Yes, this notational trick -- where sometimes a variable is free, and 
sometimes is bound, and the reader has to tell the difference -- is 
common in many formal models.  In R-IntfSuper, i is a free variable, so 
the rule defines sres(C, I_i) simultaneously for ALL I_i that are 
superinterfaces of C.

In the other example you cite, i is bound by the union quantifier, so it 
is not a free variable.





On 12/2/2011 7:17 PM, Richard Warburton wrote:
> On 02/12/11 20:32, Brian Goetz wrote:
>> I have completed a major refinement of the formal model for defender
>> resolution.  There are significant cleanups in the math (mostly notably
>> fixing the ambiguity surrounding the meaning of 'nil' in lookup
>> functions) which enabled some simplifications in the model; we were able
>> to eliminate many of the internal predicates (SigOK, BodyOK) and thereby
>> simplify (and in some cases, eliminate) many rules.  Also added are new
>> judgments for resolution of I.super.m() calls.
>>
>> Comments welcome.
>>
>> http://hg.openjdk.java.net/lambda/defender-prototype/raw-file/f49be48f1225/doc/featherweight-defenders.pdf
> Thanks for posting this document to the list - it's a really interesting
> read.
>
> On a minor point in rule R-IntfSuper it appears as though the meaning of
> subscript i is overloaded.  It is used as an index into the set of all
> immediate super-interface when calculating S (the union of their
> defender candidates).  It is also used to denote a specific immediate
> super-interface of C that the super-call is being made through and
> appears to be referred to in that context in "dcand(Ii) = { J }".
>
> This was of initial confusion to me, and it would probably be clearer to
> the reader if the same name wasn't chosen for both meanings.  If I've
> misunderstood the linkage rule then I'm sorry.
>
> regards,
>
>     Richard
>