Formal model for defender method resolution

[Brian Goetz]

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.)