Featherweight Defenders: A formal model for
virtual extension methods in Java
Brian Goetz and Robert Field, Oracle Corporation
∗
March 27, 2012
1 Introduction
As a means of modeling the semantics of virtual extension methods (also known
as defender methods) in Java, we describe a lightweight model of Java in the
style of Featherweight Java (Pierce et al.), called Featherweight Defenders (or
FD).
This model retains many aspects of Java’s class and method inheritance.
We drastically simplify method overloading and naming (classes and interfaces
can have only one method, named m(), with no arguments), but retain single
inheritance of classes and multiple inheritance of interfaces, covariant overriding,
abstract and concrete class methods, and reabstraction of concrete class methods
(where a concrete method is overridden with an abstract one).
We add in a new feature not yet present in Java, virtual extension methods,
where an interface can provide a default implementation for a method. Interface
methods may be abstract definitions (no default clause) or specify a concrete
default implementation (default k). Concrete defaults may be overridden by
abstrac methods (by overriding the method without providing a new default),
which is akin to reabstraction of concrete methods in classes.
The goal of this model is twofold: to capture the rules regarding well-
formedness of types in the presence of extension methods, and to capture the
runtime mapping of method names within a class to concrete method bodies
which provide the implementation of that method for that class, which we call
the linkage of the method m() in C.
We believe that this model includes the most significant inheritance features
that are relevant to method linkage in the presence of extension methods. There
are some additional features relevant to the implementation, such as bridge
methods, that are beyond the scope of this model.
∗
The authors gratefully acknowlege the assistance of Sukyoung Ryu of KAIST in the
refinement of this formal model.
1
T ::= Object | C | I
K ::= class C extends D implements I
1
, ..., I
n
{ [ R m() h b | abstract i ] }
L ::= interface I extends I
1
, ..., I
n
{ [ R m() [ defaultk ] ] }
Figure 1: FD language syntax
2 Syntax
The metavariables C, D, and E (and their derivatives) range over class names
and the metavariable I, J, and K range over interface names. The metavari-
ables T , R, U, V , and W range over all types (classes and interfaces). The
metavariable S ranges over sets of types. The metavariable k ranges over a
set of nominal identifiers, and the metavariable b ranges over a set of method
bodies. Figure 1 shows the syntatic forms for FD.
3 Preliminaries
Figure 2 shows the subtyping judgements for classes and interfaces.
S-Refl
T <: T
S-Trans
T <: V V <: W
T <: W
S-Class
class C extends D implements I
1
, ..., I
n
{...}
C <: D ∀
i
C <: I
i
S-Intf
interface I extends I
1
, ..., I
n
{...}
∀
i
I <: I
i
Figure 2: Basic subtyping rules
As in Featherweight Java, we use “lookup functions” (such as mtype(T )) and
“marker predicates” (such as T OK) in the inference rules to record information
about types. These will be introduced as they are used by the inference rules.
4 Compile-time vs runtime
One of the goals of this model is to present a formal procedure for linking a
method m() in a class C among the many candidate choices contributed by
superclasses and interfaces. In languages like Java, method linkage analysis is
performed both at compile time (to ensure that methods link uniquely, that
2
required methods are implemented, and to reject source files that do not meet
these requirements) and at run time (to perform linkage dynamically.) It is
important to ensure that linkage decisions made at compile time and run time
are consistent, but issues like separate compilation and dynamic linking pose
challenges to this goal, since class files compiled separately may not provide a
consistent view of the type hierarchy at run time, which may lead to runtime
errors.
This model divides rules into two categories – typing-related (those beginning
with T-) and linkage-related (those beginning with R-). A compiler would
execute and enforce all the rules; the runtime would execute only the linkage
rules. In a well-typed program, the compiler and runtime view of the world
should be identical; in an inconsistently-typed program (say, due to separate
compilation), it may still be possible to perform method linkage at runtime
according to the R- rules. The treatment of separate compilation and dynamic
linkage is outside the scope of this model.
5 Method typing
Figure 3 shows the typing rules for resolving the type of method m() in classes
and interfaces. It defines the lookup function mtype(T ), which describes the
return type of the method m() in T .
Central to the typing analysis is identifying whether a method m() in type
T (whether defined explicitly or inherited) can legally override all signatures of
m() from supertypes of T . Java supports covariant overrides – where a method
in a subclass overrides a method in a supertype, but provides a narrower return
type. If a method m() in T overrides one or more methods from supertypes, the
return type of m() in T must be a subtype of each of the return types of m()
from supertypes. If there is such a type, we say m() has a well-defined return
type in T .
The value of mtype(T ) is a set of types, and is one of the following:
• The empty set {}, indicating that the method m() is not a member of T ;
• The set { U }, indicating that the method m() has a well-defined return
type in T , and that return type is U;
• undefined, indicating that the method m() does not have a well-defined
return type in T . The compiler should reject types for which mtype(T ) is
undefined, but having a well-defined return type is not sufficient to declare
that T is well-formed (for example, T could have conflicting defaults or
problems with covariant overrides.)
By defining mtype in this way, we can explicitly distinguish between the
case where we know that type T does not have a member m() (mtype(T ) =
{}), and the case where we cannot assign a well-defined type for m() in T
(mtype(T ) = undefined). If we bind a symbol to mtype(T ) in the precondition of
a typing judgement (such as the binding of S in T-ClassNone), and mtype(T )
is undefined, then the binding fails and therefore the judgement does not apply.
3
Having defined mtype in this way, we define a relation for optional subtyping
between a candidate type T and the return type of m() in U:
T
˜
<: mtype(U) ≡ mtype(U ) = {} ∨ [ mtype(U) = { V } ∧ T <: V ]
Intuitively, if T
˜
<: mtype(U), then T is a potentially valid return type for
the method m() in a subtype of U .
We extend this concept by defining the function lbi
mty pe
, which computes an
inclusive lower bound under optional subtyping for a projection under mtype of
a set of types. (The inclusive lower bound for a set S is the lower bound of S if S
contains its lower bound, and undefined otherwise.) We define lbi
mty pe
(T
1
, ..., T
n
)
as follows:
lbi
mty pe
(T
1
, ..., T
n
) =
{} if ∀
i
mtype(T
i
) = {}
mtype(T
i
) if ∃
i
such that mtype(T
i
) = { U }, and
∀
j6=i
U
˜
<: mtype(T
j
)
undefined otherwise
We use lbi
mty pe
to determine whether there is a consistent return type for
the method m() in T given the types of m() in the supertypes of T . (Note that
if mtype(T
i
) is undefined for any i, then lbi
mty pe
(T
1
, ..., T
n
) is also undefined.)
T-ClassExpl
class C extends D implements I
1
, ..., I
n
{ T m() h b | abstract i }
T
˜
<: mtype(D) ∀
i
T
˜
<: mtype(I
i
)
mtype(C) = { T }
T-ClassImpl
class C extends D implements I
1
, ..., I
n
{ }
mtype(C) = lbi
mty pe
(D, I
1
, ..., I
n
)
T-IntExpl
interface I extends I
1
, ..., I
n
{ T m() [ default k ] }
∀
i
T
˜
<: mtype(I
i
)
mtype(I) = { T }
T-IntImpl
interface I extends I
1
, ..., I
n
{ }
mtype(I) = lbi
mty pe
(I
1
, ..., I
n
)
T-Object
mtype(Object) = {} Object OK
Figure 3: Method typing
4
6 Method inheritance
The rules so far only have to do with computing the membership of a method
in a type, and the method’s return type in that type, and do not consider where
the method implementation codes from. We now explore the rules for inheriting
methods, including inheritance of bodies from superclasses and inheritance of
default implementations from superinterfaces.
All classes (except the root class Object) have a single superclass. We treat
a concrete method body and a declaration that the method is abstract in the
same way (collectively, we call these a method declaration). A class inherits
method declarations from its superclass, unless the method is explicitly given a
new declaration in the subclass.
A key aspect of inheritance of default methods is pruning of less-specific
default-providing interfaces from consideration in the linkage process. In Java,
it is allowable for a class or interface to extend an interface both directly and
indirectly, as in the following example:
interface A { Object m () default k }
int e rface B exte nds A { Object m () default l }
class C implements A, B { }
Here, C implements A both directly and indirectly. This idiom is common as
a documentation device, and in Java 7 and earlier the additional declaration of
A has no effect, because it is already implicit in the extension of B. This behavior
should continue to hold true in the presence of extension methods.
The inheritance rules for extension methods calls for “redundant” inher-
itance from less-specific interfaces (such as A in the example above) to not
be considered further in the inheritance decision, except inasmuch as the less-
specific interface has already contributed to its subinterface.
We capture this pruning behavior by the function prune(S):
prune(S) = { W ∈ S : ∀
V ∈S
V <: W ⇒ V = W }
Intuitively, the rules for method linkage behave as follows:
• A method defined in a type takes precedence over methods defined in its
supertypes (R-IntDef, R-ClassBody).
• A method declaration (concrete or abstract) inherited from a superclass
takes precedence over a default inherited from an interface (R-LinkImpl).
• More specific default-providing interfaces take precedence over less specific
ones (R-IntInh, R-ClassInh).
• If we are to link m() to a default method from an interface, there must a
unique most specific default-providing interface to link to (R-LinkDef).
Figure 4 covers the rules for computing the candidates for inheriting methods
from classes and interfaces. It defines the following lookup functions:
• icand(T ) (interface candidates), which indicates the set of interfaces which
could provide a default implementation for m() in T . This is used both in
5
member inheritance calculations, as well as identifying the valid targets
for a super-call.
• mprov(C) (method provenance), which indicates the most specific super-
class from which C could inherit a method declaration for m(). Like
mtype, the value of mprov(C) is a set, which is either empty (there is
no superclass that provides a declaration for m() in C), or a singleton set
that contains the class providing the declaration for m() in C.
• T HasBody, which indicates that T declares either a concrete method
body (for classes) or a default implementation (for interfaces). (It is not
inherited; it is strictly a property of the class or interface declaration, and
will be used in the final linkage decision.)
R-Object
mprov(Object) = {} icand(Object) = {}
R-IntDef
interface I extends I
1
, ..., I
n
{ T m() [ default k ] }
icand(I) = { I }
R-IntInh
interface I extends I
1
, ..., I
n
{ }
S =
S
i
icand(I
i
)
icand(I) = prune(S)
R-ClassInh
class C extends D implements I
1
, ..., I
n
{ . . . }
S =
S
U∈{ D,I
1
,...,I
n
}
icand(U)
icand(C) = prune(S)
R-ClassBody
class C extends D implements I
1
, ..., I
n
{ T m() h b | abstract i }
mprov(C) = { C }
R-ClassInhBody
class C extends D implements I
1
, ..., I
n
{ }
mprov(C) = mprov(D)
R-HasBody
class C extends D implements I
1
, ..., I
n
{ T m() b }
C HasBody
R-HasDef
interface I extends I
1
, ..., I
n
{ T m() default k }
I HasBody
Figure 4: Inheritance candidates from classes and interfaces
6
T-IntNoBody
interface I extends I
1
, ..., I
n
{ ... }
S = mtype(I) ∀
i
I
i
OK icand(I) = {}
I OK
T-IntInhBody
interface I extends I
1
, ..., I
n
{ ... }
∀
i
I
i
OK icand(I) = { J }
mtype(I) = mtype(J)
I OK
Figure 5: Typechecking of interfaces
7 Typechecking of interfaces and classes
We now consider the rules for when an interface or class should be accepted as
well-typed. We use the marker predicate T OK to indicate that T is well-typed.
Figure 5 shows the typechecking rules for interfaces. For an interface I, I OK
means:
• All the supertypes of I are OK;
• If m() is a member of I, it has a well-defined return type in I;
• If m() is a member of I, then there is at most one defender candidate for
m() in I, and if present, that defender candidate has the same return type
as m() in I.
Figure 6 shows the typechecking rules for classes. For a class C, C OK means:
• All the supertypes of C are OK;
• If m() is a member of C, it has a well-defined return type in C;
• If C inherits a method declaration from a superclass, it has the same
return type as m() in C.
• If C does not inherit a method declaration from a superclass, then there is
at most one defender candidate for m() in C, and if present, that defender
candidate has the same return type as m() in C.
Note that the typechecking rules do not reject classes which inherit abstract
method definitions from supertypes and which do not provide an implementa-
tion. These classes are considered valid, but at runtime are identified as having
no linkage. This is a consequence of simplifying the language model to not
explicitly track classes as abstract vs concrete, and does not interfere with the
goals of this model.
8 Method linkage
We are now able to define the linkage of m() in a class C which may inherit its
implementation from a superclass or from a default method in an interface.
7
T-ClassNone
class C extends D implements I
1
, ..., I
n
{ ... }
D OK ∀
i
I
i
OK
S = mtype(C) mprov(C) = {} icand(C) = {}
C OK
T-ClassFromSuper
class C extends D implements I
1
, ..., I
n
{ ... }
D OK ∀
i
I
i
OK
mprov(C) = { E } mtype(C) = mtype(E)
C OK
T-ClassFromDefault
class C extends D implements I
1
, ..., I
n
{ ... }
D OK ∀
i
I
i
OK
mprov(C) = {} icand(C) = { J }
mtype(C) = mtype(J )
C OK
Figure 6: Typechecking of classes
R-LinkImpl
class C extends D implements I
1
, ..., I
n
{ ... }
mprov(C) = { T } T HasBody
mres(C) = T
R-LinkDef
class C extends D implements I
1
, ..., I
n
{ ... }
mprov(C) = {} icand(C) = { J } J HasBody
mres(C) = J
Figure 7: Linkage
Figure 7 defines the lookup function mres(C), which indicates the linkage
of m() in class C. Its value is the type from which m() is inherited.
9 Superclass invocation linkage
Java provides a mechanism for a method overriding a method in a superclass
to invoke the overridden method, using the super.m() syntax. We would wish
to support a similar mechanism, where an interface or class overriding a default
method from an interface I could invoke the overridden default as I.super.m().
While the FD calculus does not provide syntax for method invocation, we
can define a lookup function sres(T, I) that would provide the desired linkage
for a super-call to m() from T through interface I, just as we did for mres(C).
Figure 8 shows the calculation of sres(T, I). For making a super-call from T
through interface I, I must be an immediate super-interface of T , I must have
8
R-ClassSuper
class C extends D implements I
1
, ..., I
n
{ ... }
icand(I
i
) = { J } J ∈ icand(C) J HasBody
sres(C, I
i
) = J
R-IntfSuper
interface I extends I
1
, ..., I
n
{ ... }
S =
S
k
icand(I
k
)
icand(I
i
) = { J } J ∈ prune(S) J HasBody
sres(I, I
i
) = J
Figure 8: Super-call linkage
a well-defined default on its own, and that default must not be overridden by
a more specific superinterface of T . (In other words, I.super.m() must link to
a method that was a candidate for inheritance by T if T were to not override
m().)
9
