FHJ: A Formal Model for Hierarchical Dispatching
and Overriding
Yanlin Wang1
The University of Hong Kong, China
ylwang@cs.hku.hk

Haoyuan Zhang1
The University of Hong Kong, China
hyzhang@cs.hku.hk

Bruno C. d. S. Oliveira1
The University of Hong Kong, China
bruno@cs.hku.hk

Marco Servetto
Victoria University of Wellington, New Zealand
marco.servetto@ecs.vuw.ac.nz

Abstract
Multiple inheritance is a valuable feature for Object-Oriented Programming. However, it is also
tricky to get right, as illustrated by the extensive literature on the topic. A key issue is the ambiguity arising from inheriting multiple parents, which can have conflicting methods. Numerous
existing work provides solutions for conflicts which arise from diamond inheritance: i.e. conflicts
that arise from implementations sharing a common ancestor. However, most mechanisms are
inadequate to deal with unintentional method conflicts: conflicts which arise from two unrelated
methods that happen to share the same name and signature.
This paper presents a new model called Featherweight Hierarchical Java (FHJ) that deals
with unintentional method conflicts. In our new model, which is partly inspired by C++, conflicting methods arising from unrelated methods can coexist in the same class, and hierarchicaldispatching supports unambiguous lookups in the presence of such conflicting methods. To avoid
ambiguity, hierarchical information is employed in method dispatching, which uses a combinationof static and dynamic type information to choose the implementation of a method at run-time.
Furthermore, unlike all existing inheritance models, our model supports hierarchical method
overriding: that is, methods can be independently overridden along the multiple inheritance hierarchy. We give illustrative examples of our language and features and formalize FHJ as aminimal Featherweight-Java style calculus.
2012 ACM Subject Classification Software and its engineering → Object oriented languages
Keywords and phrases multiple inheritance; hierarchical dispatching; OOP; language design
Digital Object Identifier 10.4230/LIPIcs.ECOOP.2018.20
Acknowledgements We thank the anonymous reviewers for their valuable comments.

1

Funded by Hong Kong Research Grant Council projects number 17210617 and 17258816© Yanlin Wang, Haoyuan Zhang, Bruno C. d. S. Oliveira and Marco Servetto;
licensed under Creative Commons License CC-BY
32nd European Conference on Object-Oriented Programming (ECOOP 2018).
Editor: Todd Millstein; Article No. 20; pp. 20:1–20:30
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

20:2

FHJ: A Formal Model for Hierarchical Dispatching and Overriding

1

Introduction

Inheritance in Object-Oriented Programming (OOP) offers a mechanism for code reuse.
However many OOP languages are restricted to single inheritance, which is less expressive
and flexible than multiple inheritance. Nevertheless, different flavours of multiple inheritancehave been adopted in some popular OOP languages. C++ has had multiple inheritance fromthe start. Scala adapts the ideas from traits [28, 9, 16] and mixins [5, 11, 32, 2, 13] to offer adisciplined form of multiple inheritance. Java 8 offers a simple variant of traits, disguised asinterfaces with default methods [12].
A reason why programming languages have resisted to multiple inheritance in the pastis that, as Cook [7] puts it, “multiple inheritance is good but there is no good way to do it”.
One of the most sensitive and critical issues is perhaps the ambiguity introduced by multiple
inheritance. One case is the famous diamond problem [27, 29] (also known as the fork-join
inheritance [27]). In the diamond problem, inheritance allows one feature to be inheritedfrom multiple parent classes that share a common ancestor. Hence conflicts arise. The variety
of strategies for resolving such conflicts urges the occurrence of different multiple inheritancemodels, including traits, mixins, CZ [17], and many others. Existing languages and research
have addressed the issue of diamond inheritance extensively. Other issues including how
multiple inheritance deals with state, have also been discussed quite extensively [33, 17, 31].
In contrast to diamond inheritance, the second case of ambiguity is unintentional method
conflicts [28]. In this case, conflicting methods do not actually refer to the same feature. In
a nominal system, methods can be designed for different functionality but happen to havethe same names (and signatures). A simple example of this situation is two draw methods
that are inherited from a deck of cards and a drawable widget, respectively. In such context,
the two draw methods have very different meanings, but they happen to share the same
name. When inheritance is used to compose these classes, a compilation error happens
due to conflicts. However, unlike the diamond problem, the conflicting methods have very
different meanings and do not share a common parent. We call such a case fork inheritance,
in analogy to diamond inheritance.
When unintentional method conflicts happen, they can have severe effects in practice if
no appropriate mechanisms to deal with them are available. In practice, existing languages
only provide limited support for the issue. In most languages, the mechanisms available
to deal with this problem are the same as the diamond inheritance. However, this is often
inadequate and can lead to tricky problems in practice. This is especially the case when it
is necessary to combine two large modules and their features, but the inheritance is simply
prohibited by a small conflict. As a workaround from the diamond inheritance side, it ispossible to define a new method in the child class to override those conflicting methods.
However, using one method to fuse two unrelated features is clearly unsatisfactory. Therefore
we need a better solution to keep both features separately during inheritance, so as not tobreak independent extensibility [36].
C++ and C# do allow for two unintentionally conflicting methods to coexist in a class.
C# allows this by interface multiple inheritance and explicit method implementations. But
since C# is a single inheritance language, it is only possible to implement multiple interfaces(but not multiple classes). C++ accepts fork inheritance and resolves the ambiguity by
specifying the expected path by upcasts. However, neither the C# nor C++ approaches allow
such conflicting methods to be further overridden. Some other workarounds or approaches
include delegation and renaming/exclusion in the trait model. However, renaming/exclusion
can break the subtyping relation between a subclass and its parent. This is not adequate for

Y. Wang, H. Zhang, B. C. d. S. Oliveira and M. Servetto

20:3

Figure 1 DrawableSafeDeck: an illustration of hierarchical overriding.

the class model commonly used in mainstream OOP languages, where the subclass is always
expected to be a subtype of the parent class.
This paper proposes two mechanisms to deal with unintentional method conflicts: hierarchical dispatching and hierarchical overriding. Hierarchical dispatching is inspired by
the mechanisms in C++ and provides an approach to method dispatching, which combines
static and dynamic information. Using hierarchical dispatching, the method binder will
look at both the static type and the dynamic type of the receiver during runtime. When
there are multiple branches that cause unintentional conflicts, the static type can specify one
branch among them for unambiguity, and the dynamic type helps to find the most specificimplementation. In that case, both unambiguity and extensibility are preserved. The mainnovelty over existing work is the formalization of the essence of a hierarchical dispatchingalgorithm, which (as far as we know) has not been formalized before.
Hierarchical overriding is a novel language mechanism that allows method overriding tobe applied only to one branch of the class hierarchy. Hierarchical overriding adds expressive
power that is not available in languages such as C++ or C#. In particular, it allows overriding
to work for classes with multiple (conflicting) methods sharing the same names and signatures.
An example is presented in Figure 1. In this example, there are 4 classes/interfaces. Twoclasses Deck and Drawable model a deck of cards and a drawable widget, respectively. The
class SafeDeck adds functionality to check whether the deck is empty so as to prevent drawing
a card from an empty deck. The interesting class is DrawableSafeDeck, which inherits fromboth SafeDeck and Drawable. Hierarchical overriding is used in DrawableSafeDeck to keep two
separate draw methods for each parent, but override only the draw method coming fromDrawable, in order to draw a widget with a deck of cards. Note that hierarchical overriding isdenoted in the UML diagram with the notation draw()↑Drawable, expressing that the draw
method from Drawable is overridden. Although in this example only one of the draw methods
is overridden (and the other is simply inherited), hierarchical overriding supports multiple
conflicting methods to be independently overridden as well.
To present hierarchical overriding and dispatching, we introduce a formalized model FHJ
in Section 3 based on Featherweight Java [14], together with theorems and proofs for typesoundness. We also have a prototype implementation of an FHJ interpreter written in Scala.
The implementation validates all the examples presented in the paper. One nice feature of
the implementation is that it can show the detailed step-by-step evaluation of the program,which is convenient for understanding and debugging programs & semantics.
In summary, our contributions are:
A formalization of the hierarchical dispatching algorithm that integrates boththe static type and dynamic type for method dispatch, and ensures unambiguity as well

ECOOP 2018

20:4

FHJ: A Formal Model for Hierarchical Dispatching and Overriding

as extensibility in the presence of unintentional method conflicts.
Hierarchical overriding: a novel notion that allows methods to override individual
branches of the class hierarchy.
FHJ: a formalized model based on Featherweight Java, supporting the above features.
We provide the static and dynamic semantics and prove the type soundness of the model.
Prototype implementation2 : a simple implementation of FHJ interpreter in Scala.
The implementation can type-check and run variants of all the examples shown in thispaper.

2

A Running Example: Drawable Deck

This section illustrates the problem of unintentional method conflicts, together with thefeatures of our model for addressing this issue, by a simple running example. In thefollowing text, we will introduce three problems one by one and have a discussion on possible
workarounds and our solutions. Problems 1 and 2 are related to hierarchical dispatching, andin C++ it is possible to have similar solutions to both problems. Hence it is important toemphasize that, with respect to hierarchical dispatching, our model is not a novel mechanism.
Instead, inspired by the C++ solutions, our contribution is formalizing a minimal calculus of
this feature together with a proof of type soundness. However, for the final problem, there
is no satisfactory approach in existing languages, thus what we propose is a novel feature(hierarchical overriding) with the corresponding formalization of that feature.
In the rest of the paper, we use a Java-like syntax for programs. All types are definedwith the keyword interface; the concept is closely related to Java 8 interfaces with default
methods [4] and traits. In short, an interface in our model has the following characteristics:
It allows multiple inheritance.
Every method is either abstract or implemented with a body (like Java 8 default methods).
The new keyword is used to instantiate an interface.
It cannot have state.

2.1

Problem 1: Basic Unintentional Method Conflicts

Suppose that two components Deck and Drawable have been developed in a system. Deck
represents a deck of cards and defines a method draw for drawing a card from the deck.
Drawable is an interface for graphics that can be drawn and also includes a method called
draw for visual display. For simple illustration, the default implementation of the draw inDrawable only creates a blank canvas on the screen, while the draw method in Deck simply
prints out a message "Draw a card.".
interface Deck {void draw() { // draws a card from the Deckprintln("Draw a card.");}}interface Drawable {void draw() { // create a blank canvas
JFrame frame = new JFrame();frame.setVisible(true);}

2

The implementation is available at https://github.com/YanlinWang/MIM/tree/master/Calculus

Y. Wang, H. Zhang, B. C. d. S. Oliveira and M. Servetto

20:5

}

In Deck, draw uses println, which is a library function. The two draw methods can havedifferent return types, but for simplicity, the return types are both void here. Note that,similarly to Featherweight Java [14], void is unsupported in our formalization. We could havealso defined an interface called Void and return an object of that type instead. To be concise,
however, we use void in our examples. In interface Drawable, the draw method creates a blankcanvas.
Now, suppose that a programmer is designing a card game with a GUI. He may want todraw a deck on the screen, so he first defines a drawable deck using multiple inheritance:interface DrawableDeck extends Drawable, Deck {}The point of using multiple inheritance is to compose the features from various components
and to achieve code reuse, as supported by many mainstream OO languages. Nevertheless,at this point, languages like Java simply treat the two draw methods as the same, hence thecompiler fails to compile the program and reports an error.
This case is an example of a so-called unintentional method conflict. It arises when two
inherited methods happen to have the same name and parameter types, but they are designed
for different functionalities with different semantics. Now one may quickly come up with aworkaround, which is to manually merge the two methods by creating a new draw method in
DrawableDeck to override the old ones. However, merging two methods with totally different
functionalities does not make any sense. This non-solution would hide the old methods andbreak independent extensibility.

2.1.1

Problem and Possible Workarounds

The essential problem is how to resolve unintentional method conflicts and invoke theconflicting methods separately without ambiguity. To tackle this problem, there are several
other workarounds that come to our mind. We briefly discuss those potential fixes andworkarounds next:
I. Delegation. As an alternative to multiple inheritance, delegation can be used byintroducing two fields (or field methods) with the Drawable type and Deck type, respectively.
Although it avoids method conflicts, it is known that using delegation makes it hard tocorrectly maintain self-references in an extensible system and also introduces a lot ofboilerplate code.
II. Refactor Drawable and/or Deck to rename the methods. If the source code for Drawable or
Deck is available then it may be possible to rename one of the draw methods. However, thisapproach is non-modular, as it requires modifying existing code and becomes impossible
if the code is unavailable.
III. Method exclusion/renaming. Eiffel [18] and some trait models support method
exclusion/renaming. Those features can eliminate conflicts, although most programming
languages do not support them. In a traditional OO system, they can break the subtyping
relationship. Moreover, in contrast with exclusion, renaming can indeed preserve bothconflicting behaviours. However, it is cumbersome in practice, as introducing new names
can affect other code blocks.

ECOOP 2018

20:6

FHJ: A Formal Model for Hierarchical Dispatching and Overriding

2.1.2

FHJ’s solution

To solve this problem it is important to preserve both conflicting methods during inheritanceinstead of merging them into a single method. Therefore FHJ accepts the definition ofDrawableDeck. To disambiguate method calls, we can use upcasts in FHJ to specify the“branch” in the inheritance hierarchy that should be called. The following code illustrates
the use of upcasts for disambiguation:interface Deck { void draw() {...} }interface Drawable { void draw() {...} }interface DrawableDeck extends Drawable, Deck {}// main program((Deck) new DrawableDeck()).draw() // calls Deck.draw// new DrawableDeck().draw() // this call is ambiguous and rejected

In our language, a program consists of interfaces declarations and a main an expression which
produces the final result. In the above main expression ((Deck)new DrawableDeck()).draw(),
the cast indicates that we expect to invoke the draw method from the branch Deck. Similarly,
we could have used an upcast to Drawable to call the draw method from Drawable. Without
the cast, the call would be ambiguous and FHJ’s type system would reject it.
This example illustrates the basic form of fork inheritance, where two unintentionallyconflicting methods are accepted by multiple inheritance. Note that C++ supports thisfeature and also addresses the ambiguity by upcasts. The code for the above example in
C++ is similar.

2.2

Problem 2: Dynamic Dispatching

Using explicit upcasts for disambiguation helps when making calls to classes with conflicting
methods, but things become more complicated with dynamic dispatching. Dynamic dispatching is very common in OO programming for code reuse. Let us expand the previous example
a bit, by redefining those interfaces with more features:interface Deck {void draw() {...}
void shuffle() {...}
void shuffleAndDraw() { this.shuffle(); this.draw(); }}Here shuffleAndDraw invokes draw from its own enclosing type. In FHJ, this invocation is
dynamically dispatched. This is important, because a programmer may define a subtype ofDeck and override the method draw:
interface SafeDeck extends Deck {boolean isEmpty() {...}
void draw() { // overriding
if (isEmpty()) println("The deck is empty.");else println("Draw a card");}}Without dynamic dispatching, we may have to copy the shuffleAndDraw code into SafeDeck, sothat shuffleAndDraw calls the new draw defined in SafeDeck. Dynamic dispatching immediately
saves us from the duplication work, since the method becomes automatically dispatchedto the most specific one. Nevertheless, as seen before, dynamic dispatch would potentiallyintroduce ambiguity. For instance, when we have the class hierarchy structure shown in
Figure 2(left) with the following code:

Y. Wang, H. Zhang, B. C. d. S. Oliveira and M. Servetto

20:7

Figure 2 UML diagrams for 3 variants of DrawableSafeDeck.

interface DrawableSafeDeck extends Drawable, SafeDeck {}new DrawableSafeDeck().shuffleAndDraw()

Indeed, using reduction steps following the reduction rules in FJ [14]-like languages, where
no static types are tracked, the reduction steps would roughly be:
new DrawableSafeDeck().shuffleAndDraw()-> new DrawableSafeDeck().shuffle(); new DrawableSafeDeck().draw()-> ...
-> new DrawableSafeDeck().draw()-> <<error: ambiguous call!!!>>

When the DrawableSafeDeck object calls shuffleAndDraw, the implementation in Deck is dispatched. But then shuffleAndDraw invokes “this.draw()”, and at this point, the receiver isreplaced by the object new DrawableSafeDeck(). From the perspective of DrawableSafeDeck,the draw method seems to be ambiguous since DrawableSafeDeck inherits two draw methods from both SafeDeck and Drawable. But ideally we would like shuffleAndDraw to invoke
SafeDeck.draw because they belong to the same class hierarchy branch.

2.2.1

FHJ’s solution

The essential problem is how to ensure that the correct method is invoked. To solve thisproblem, FHJ uses a variant of method dispatching that we call hierarchical dispatching. In
hierarchical dispatching, both the static and dynamic type information are used to selectthe right method implementation. During runtime, a method call makes use of both thestatic type and the dynamic type of the receiver, so it is a combination of static and dynamic
dispatching. Intuitively, the static type specifies one branch to avoid ambiguity, and the
dynamic type finds the most specific implementation on that branch. To be specific, thefollowing code is accepted by FHJ:
interface Deck {void draw() {...}
void shuffle() {...}
void shuffleAndDraw() { this.shuffle(); this.draw(); }}interface Drawable {...}
interface SafeDeck extends Deck {...}
interface DrawableSafeDeck extends Drawable, SafeDeck {}new DrawableSafeDeck().shuffleAndDraw() // SafeDeck.draw is called

The computation performed in FHJ is as follows:
new DrawableSafeDeck().shuffleAndDraw()-> ((DrawableSafeDeck) new DrawableSafeDeck()).shuffleAndDraw()

ECOOP 2018

20:8

FHJ: A Formal Model for Hierarchical Dispatching and Overriding-> ((Deck) new DrawableSafeDeck()).shuffle(); ((Deck) new DrawableSafeDeck()).draw()-> ...
-> ((Deck) new DrawableSafeDeck()).draw()-> ... // SafeDeck.draw

Notably, we track the static types by adding upcasts during reduction. In contrast to FJ,
where new C() is a value, in FHJ such an expression is not a value. Instead, an expressionof the form new C() is reduced to (C)new C(), which is a value in FHJ and the cast denotes
the static type of the expression. This rule is applied in the first reduction step. In thesecond reduction step, when shuffleAndDraw is dispatched, the receiver (DrawableSafeDeck)new DrawableSafeDeck() replaces the special variable this by (Deck)new DrawableSafeDeck().
Here, the static type used in the cast (Deck) denotes the origin of the shuffleAndDraw
method, which is discovered during method lookup. Later, in the fourth step, ((Deck)new
DrawableSafeDeck()).draw() is an instance of hierarchical invocation, which can be read as“finding the most specific draw above DrawableSafeDeck and along path Deck”. The meaning of“above DrawableSafeDeck” implies its supertypes, and “along path Deck” specifies the branch.
Finally, in the last reduction step, we find the most specific version of draw in SafeDeck. In
this sequence of reduction steps, the cast that tracks the origin of shuffleAndDraw is crucial
to unambiguously find the correct implementation of draw. The formal procedure will be
introduced in Section 3 and Section 4.

2.3

Problem 3: Overriding on Individual Branches

Method overriding is common in Object-Oriented Programming. With diamond inheritance,
where conflicting methods are intended to have the same semantics, method overriding is
not a problem. If conflicting methods arise from multiple parents, we can override all thosemethods in a single unified (or merged) method in the subclass. Therefore further overriding
is simple, because there is only one method that can be overridden.
With unintentional method conflicts, however, the situation is more complicated because
different, separate, conflicting methods can coexist in one class. Ideally, we would like tosupport overriding for those methods too, in exactly the same way that overriding is available
for other (non-conflicting) methods. However, we need to be able to override the individual
conflicting methods, rather than overriding all conflicting methods into a single merged one.
We illustrate the problem and the need for a more refined overriding mechanism withan example. Suppose that the programmer defines a new interface DrawableSafeDeck (basedon the code in Section 2.2 without the old DrawableSafeDeck), but he needs to override
Drawable.draw and give a new implementation of drawing so that the deck can indeed bevisualized on the canvas.

2.3.1

Potential solutions/workarounds in existing languages

Unfortunately in all languages we know of (including C++), the existing approaches areunsatisfactory. One direction is to simply avoid this issue, by putting overriding before
inheritance. For example, as shown in Figure 2(middle), we define a new component
DrawableRect that extends Drawable, which simply draws the deck as a rectangle, and modifies
the hierarchy:
interface DrawableRect extends Drawable {void draw() {JFrame frame = new JFrame("Canvas");frame.setSize(600, 600);
frame.getContentPane().setBackground(Color.red);Y. Wang, H. Zhang, B. C. d. S. Oliveira and M. Servetto

20:9

frame.getContentPane().add(new Square(10,10,100,100)); ...
}}interface DrawableSafeDeck extends DrawableRect, SafeDeck {}This workaround seems to work, but there are severe issues:
It changes the hierarchy and existing code, hence breaks the modularity.
Separate overriding is required to come after the fork inheritance, especially when theimplementation needs functionality from both parents. In the above code, we haveassumed that the overriding is unrelated to Deck. But when the drawing relies on some
information of the Deck object, we have to either introduce field methods for delegationor change the signature of draw to take a parameter. Either way introduces unnecessary
complexity and affects extensibility.
There are more involved workarounds in C++ using templates and complex patterns,
but such patterns are complex to use and there are still issues. A more detailed discussion ofsuch an approach is presented in Section 6.2.

2.3.2

FHJ’s solution

An additional feature of our model is hierarchical overriding. It allows conflicting methods
to be overridden on individual branches, hence offers independent extensibility. The above
example can be easily realized by:interface DrawableSafeDeck extends Drawable, SafeDeck {void draw() override Drawable {JFrame frame = new JFrame("Canvas");frame.setSize(600, 600);
frame.getContentPane().setBackground(Color.red);frame.getContentPane().add(new Square(10,10,100,100)); ...
}}((Drawable)new DrawableSafeDeck()).draw(); //calls the draw in DrawableSafeDeck

The UML graph is shown in Figure 2(right), where the up-arrow ↑ is short for “override”.
Here the idea is that only Drawable.draw is overridden. This is accomplished by specifying, inthe method definition, that the method only overrides the draw from Drawable. The individual
overriding allows us to make use of the methods from SafeDeck as well. In the formalization,
the hierarchical overriding feature is an important feature, involved in the algorithm of
hierarchical dispatch.
Note that, although the example here only shows one conflicting method being overridden,
hierarchical overriding allows (as expected) multiple conflicting methods to be overridden in
the same class.

2.3.3

Terminology

In Drawable, Deck, and SafeDeck, the draw methods are called original methods in this paper,
because they are originally defined by the interfaces. In contrast, DrawableSafeDeck defines ahierarchical overriding method. The difference is that traditional method overriding overrides
all branches by defining another original method, whereas hierarchical overriding only refines
one branch.
A special rule for hierarchical overriding is: it can only refine original methods, and cannot
jump over original methods with the same signature. For instance, writing "void draw()

ECOOP 2018

20:10FHJ: A Formal Model for Hierarchical Dispatching and Overriding

(a)

(d)

mbody(m, C, A) = (A, ...)(b)

mbody(m, C, A) = (C, ...)

(c)mbody(m, C, A) = (C, ...)

mbody(m, C, B) = (B, ...)

mbody(m, C, B) = (C, ...)

mbody(m, C, B) = (B, ...)

mbody(m, C, C) = undefined

mbody(m, C, C) = (C, ...)

mbody(m, C, C) = undefined

mbody(m, T, T ) = (T, ...)
mbody(m, C, T ) = undefined

C rejected by type-check(e)

mbody(m, T, T ) = (T, ...)

(f)mbody(m, C, T ) = undefined
C rejected by type-checkmbody(m, C, T ) = (C, ...)
mbody(m, C, A) = (C, ...)
mbody(m, C, B) = (C, ...)
mbody(m, C, C) = (C, ...)

Figure 3 Examples in FHJ. “m ↑ A” stands for hierarchical overriding “m override A”.

override Deck {...}" is disallowed in DrawableSafeDeck, because the existing two branches

are Drawable.draw and SafeDeck.draw, while Deck.draw is already covered. It does not reallymake sense to refine the old branch Deck.

2.3.4

A peek at the hierarchical dispatching algorithm

In FHJ, fork inheritance allows several original methods (branches) to coexist, and hierarchical dispatch first finds the most specific original method (branch), then it finds the most
specific hierarchical overriding on that branch.
Before the formalized algorithm, Figure 3 gives a peek at the behavior using a few examples.
The UML diagrams present the hierarchy. In (d) and (e), a cross mark indicates that theinterface fails to type-check. Generally, FHJ rejects the definition of an interface duringcompilation if it reaches a diamond with ambiguity. mbody is the method lookup function for
hierarchical dispatch, formally defined in Section 4.1. In general, mbody(m, X, Y) = (Z, ...)
reflects that the source code ((Y)new X()).m() calls Z.m at runtime. It is undefined when
method dispatch is ambiguous.
In Figure 3, (a) is the base case for unintentional conflicts, namely the fork inheritance.
(b) uses overriding to explicitly merge the conflicting methods. (c) represents hierarchicaloverriding.
Furthermore, our model supports diamond inheritance and can deal with diamondproblems. For example, (d) and (e) are two base cases of diamond inheritance in FHJ andthe definition of each C is rejected because T is an ambiguous parent to C. One solution for
diamond inheritance is to merge methods coming from different parents. (f) gives a common
solution to the diamond as in Java or traits, which is to explicitly override A.m and B.m
in C. And our calculus supports this kind of merging methods. In the last three examples,
conflicting methods A.m and B.m should be viewed as intentional conflicts, as they come

Y. Wang, H. Zhang, B. C. d. S. Oliveira and M. Servetto

20:11

from the same source T .

3Formalization

In this section, we present a formal model called FHJ (Featherweight Hierarchical Java),
following a similar style as Featherweight Java [14]. FHJ is a minimal core calculus thatformalizes the core concept of hierarchical dispatching and overriding. The syntax, typing
rules and small-step semantics are presented.

3.1

SyntaxThe abstract syntax of FHJ interface declarations, method declarations, and expressions isgiven in Figure 4. The multiple inheritance feature of FHJ is inspired by Java 8 interfaces,
which supports method implementations via default methods. This feature is closely related
to traits. To demonstrate how unintentional method conflicts are untangled in FHJ, we only
focus on a small subset of the interface model. For example, all methods declared in aninterface are either default methods or abstract methods. Default methods provide default
implementations for methods. Abstract methods do not have a method body. Abstract
methods can be overridden with future implementations.

3.1.1

Notations

The metavariables I, J, K range over interface names; x ranges over variables; m ranges overmethod names; e ranges over expressions; and M ranges over method declarations. Following
Featherweight Java, we assume that the set of variables includes the special variable this,which cannot be used as the name of an argument to a method. We use the same conventions
as FJ; we write I as shorthand for a possibly empty sequence I1 , ..., In , which may be indexedby Ii ; and write M as shorthand for M1 ...Mn (with no commas). We also abbreviate
operations on pairs of sequences in an obvious way, writing I x for I1 x1 , ..., In xn , where nis the length of I and x.

3.1.2

Interfaces

In order to achieve multiple inheritance, an interface can have a set of parent interfaces, wheresuch a set can be empty. Moreover, as usual in class-based languages, the extension relation
over interfaces is acyclic. The interface declaration interface I extends I {M} introduces
an interface named I with parent interfaces I and a suite of methods M. The methods of I
may either override methods that are already defined in I or add new functionality special toI, we will illustrate this in more detail later.

3.1.3

Methods

Original methods and hierarchically overriding methods share the same syntax in our model
for simplicity. The concrete method declaration I m(Ix x) override J {return e; } introduces
a method named m with result type I, parameters x of type Ix and the overriding target
J. The body of the method simply includes the returned expression e. Notably, we haveintroduced the override keyword for two cases. Firstly, if the overridden interface is exactly
the enclosing interface itself, then such a method is seen as originally defined. Note that thecase of merging methods from different branches, also counts as originally defined. Secondly,
for all other cases the method is considered a hierarchical overriding method. Note that in

ECOOP 2018

20:12

FHJ: A Formal Model for Hierarchical Dispatching and Overriding

Interfaces
Methods
Expressions
Context
Values

IL
M
e
Γ
v

::=
::=
::=
::=
::=

interface I extends I {M}
I m(Ix x) override J {return e; } | I m(Ix x) override J ;x | e.m(e) | new I() | (I)ex:I(I)new J()

Figure 4 Syntax of FHJ.

an interface J, I m(Ix x) {return e; } is syntactic sugar for I m(Ix x) override J {return e; },which is the standard way to define methods in Java-like languages. The definition of abstract
methods is written as I m(Ix x) override J ;, which is similar to a concrete method but
without the method body. For simplicity, overloading is not modelled for methods, which
implies that we can uniquely identify a method by its name.

3.1.4

Expressions & Values

Expressions can be standard constructs such as variables, method invocation, object creation,
together with cast expressions. Object creation is represented by new I()3 . Fields andprimitive types are not modelled in FHJ. The casts are merely safe upcasts, and in fact,
they can be viewed as annotated expressions, where the annotation indicates its static type.
The coexistence of static and dynamic types is the key to hierarchical dispatch. A value“(I)new J()” is the final result of multiple reduction steps for evaluating an expression.
For simplicity, FHJ does not formalize statements like assignments and so on because
they are orthogonal features to the hierarchical dispatching and overriding feature. A programin FHJ consists of a list of interface declarations, plus a single expression.

3.2
3.2.1

Subtyping and Typing Rules
Subtyping

The subtyping of FHJ consists of only a few rules shown at the top of Figure 5. In short,subtyping relations are built from the inheritance in interface declarations. Subtyping isboth reflexive and transitive.

3.2.2

Type-checking

Details of type-checking rules are displayed at the bottom of Figure 5, including expression
typing, well-formedness of methods and interfaces. As a convention, an environment Γ ismaintained to store the types of variables, together with the self-reference this.
(T-Invk) is the typing rule for method invocation. Naturally, the receiver and thearguments are required to be well-typed. mbody is our key function for method lookup that
implements the hierarchical dispatching algorithm. The formal definition will be introducedin Section 4. Here mbody(m, I0 , I0 ) finds the most specific m above I0 . “Above I0 ” specifies
the search space, namely the supertypes of I0 including itself. For the general case, however,
the hierarchical invocation mbody(m, I, J) finds “the most specific m above I and along

3

In Java the corresponding syntax is new I(){}.

Y. Wang, H. Zhang, B. C. d. S. Oliveira and M. Servetto

I <: J
I <: J

I <: I

interface I extends I1 , I2 , ..., In {M}J <: KI <: KI <: I1 , I <: I2 , ..., I <: In(T-Var) Γ ` x : Γ (x)Γ `e:IΓ ` e0 : I0

20:13

mbody(m, I0 , I0 ) = (K, J x, I _)(T-Invk)Γ `e:II <: JΓ ` e0 .m(e) : I(T-New)

interface I extends I {M}canInstantiate(I)Γ ` new I() : IΓ `e:I(T-Anno)I <: JΓ ` (J)e : J
findOrigin(m, I, J) = {J}mbody(m, J, J) = (K, Ix x, Ie _)(T-Method)(T-AbsMethod)

I <: Jx : Ix , this : I ` e0 : I0

I0 <: Ie

Ie m(Ix x) override J {return e0 ; } OK IN I
I <: J findOrigin(m, I, J) = {J}mbody(m, J, J) = (K, Ix x, Ie _)Ie m(Ix x) override J ; OK IN I

M OK IN I∀J :> I and m, mbody(m, J, J) is defined ⇒ mbody(m, I, J) is defined∀J :> I and m, I[m override I] and J[m override J] defined ⇒ canOverride(m, I, J)(T-Intf)

interface I extends I {M} OK

Figure 5 Subtyping and Typing Rules of FHJ.

path/branch J”. “Along path J” additionally requires the result to relate to J, that is to say,the most specific interface that has a subtyping relationship with J.
In (T-Invk), as the compilation should not be aware of the dynamic type, it only requiresthat invoking m is valid for the static type of the receiver. The result of mbody contains
the interface that provides the most specific implementation, the parameters and the return
type. We use underscore for the return expression, matching both implemented and abstract
methods.
(T-New) is the typing rule for object creation new I(). The auxiliary function canInstantiate(I)(see definition in Section 4.4) checks whether an interface I can be instantiated or not. Since
fork inheritance accepts conflicting branches to coexist, the check requires that the most
specific method is concrete for each method on each branch.
(T-Method) is more interesting since a method can either be an original method
or a hierarchical overriding, though they share the same syntax and method typing rule.
findOrigin(m, I, J) is a fundamental function, used to find “the most specific interfaces thatare above I and along path J, and originally defines m” (see Section 4 for full definition).

ECOOP 2018

20:14

FHJ: A Formal Model for Hierarchical Dispatching and Overriding

By “most specific interfaces”, it implies that the inherited supertypes are excluded. Thus
the condition findOrigin(m, I, J) = {J} indicates a characteristic of a hierarchical overriding:
it must override an original method; the overriding is direct and there does not exist anyother original method m in between. Then mbody(m, J, J) provides the type of the original
method, so hierarchical overriding has to preserve the type. Finally the return expression is
type-checked to be a subtype of the declared return type. For the definition of an original
method, I equals J and the rule is straightforward. (T-AbsMethod) is a similar rule but
works on abstract method declarations.
(T-Intf) defines the typing rule on interfaces. The first condition is obvious, namely, its
methods need to be well checked. The third condition checks whether the overriding between
original methods preserves typing. In this condition we again use some helper functions definedin Section 4. I[m override I] is defined if I originally defines m, and canOverride(m, I, J)
checks whether I.m has the same type as J.m. Generally the preservation of method type isrequired for any supertype J and any method m.
The second condition of (T-Intf) is more complex and is the key to type soundness.
Unlike C++ which rejects on ambiguous calls, FHJ rejects on the definition of interfaces when
they form a diamond. Consider the case when the second condition is broken: mbody(m, J, J)
is defined but mbody(m, I, J) is undefined for some J and m. This indicates that m is available
and unambiguous from the perspective of J, but is ambiguous to I on branch J. It meansthat there are multiple overriding paths of m from J to I, which form a diamond. Hencerejecting that case meets our expectation. Below is an example (Figure 3 (e)) that illustrates
the reason why this condition is needed:
interface T{ T m() override T { return new T(); } }interface A extends T { T m() override T { return new A(); } }interface B extends T { T m() override T { return new B(); } }interface C extends A, B {}((T) new C()).m()

This program does not compile on interface C, because of the second condition in (T-Intf),
where I equals C and J equals T . By the algorithm, mbody(m, T, T ) will refer to T.m, but
mbody(m, C, T ) is undefined, since both A.m and B.m are most specific to C along pathT , which forms a diamond. The expression ((T)new C()).m() is one example of triggering
ambiguity, but FHJ simply rejects the definition of C. To resolve the issue, the programmer
needs to have an overriding method in C, to explicitly merge the conflicting ones.
Finally, rule (T-Anno) is the typing rule for a cast expression. By the rule, only upcasts
are valid.

3.3

Small-step Semantics and Propagation

Figure 6 defines the small-step semantics and propagation rules of FHJ. When evaluating
an expression, they are invoked and produce a single value in the end.

3.3.1

Semantic Rules(S-Invk) is the only computation rule we need for method invocation. As a small-step
rule and by congruence, it assumes that the receiver and the arguments are already values.
Specifically, the receiver (J)new I() indicates the dynamic type I together with the static
type J. Therefore mbody(m, I, J) carries out hierarchical dispatching, acquires the types, thereturn expression e0 and the interface I0 which provides the most specific method. Here weuse e0 to imply that the return expression is forced to be non-empty because it requires a

Y. Wang, H. Zhang, B. C. d. S. Oliveira and M. Servetto

20:15

concrete implementation. Now the rule reduces method invocation to e0 with substitution.
Parameters are substituted with arguments, and the this reference is substituted with thereceiver, and in the meanwhile the static types are recorded via annotations. Finally, thereturn type Ie is put in the front as an annotation.

3.3.2

Propagation Rules(C-Receiver), (C-Args) and (C-FReduce) are natural propagation rules on receivers,arguments, and cast-expressions, respectively. (C-StaticType) automatically adds anannotation I to the new object new I(). (C-AnnoReduce) merges nested upcasts into asingle upcast with the outermost type.

4

Key Algorithms and Type-Soundness

In this section, we present the fundamental algorithms and auxiliary definitions used in ourformalization and show that the resulting calculus is type sound. The functions presented inthis section are the key components that implement our algorithm for method lookup.

4.1

The Method Lookup Algorithm in mbody

mbody(m, Id , Is ) denotes the method body lookup function. We use Id , Is , since mbody isusually invoked by a receiver of a method m, with its dynamic type Id and static typeIs . Such a function returns the most specific method implementation. More accurately,
mbody returns (J, Ix x, Ie e0 ) where J is the found interface that contains the desired method;Ix x are the parameters and its types, e0 is the returned expression (empty for abstract
methods). It considers both originally-defined methods and hierarchical overriding methods,
so findOrigin and findOverride (see the definition in Section 4.2 and Section 4.3) are both
invoked. The formal definition gives the expected results for the earlier examples in Figure 3.

B Definition of mbody(m, Id , Is ) :• mbody(m, Id , Is ) = (J, Ix x, Ie e0 )with: findOrigin(m, Id , Is ) = {I}findOverride(m, Id , I) = {J}J[m override I] = Ie m(Ix x) override I {return e0 ; }• mbody(m, Id , Is ) = (J, Ix x, Ie ø)
with: findOrigin(m, Id , Is ) = {I}findOverride(m, Id , I) = {J}J[m override I] = Ie m(Ix x) override I ;To calculate mbody(m, Id , Is ), the invocation of findOrigin looks for the most specificoriginal methods and their interfaces, and expects a singleton set, so as to achieve unambiguity.
Furthermore, the invocation of findOverride also expects a unique and most specifichierarchical override. And finally the target method is returned.

ECOOP 2018

20:16

FHJ: A Formal Model for Hierarchical Dispatching and Overriding

mbody(m, I, J) = (I0 , Ix x, Ie e0 )(S-Invk)(C-Receiver)((J)new I()) .m(v) → (Ie )[(Ix )v/x, (I0 )new I()/this]e0

e0 → e00

e → e0(C-Args)

e0 .m(e) → e00 .m(e)(C-StaticType)e0 .m(. . . , e, . . .) → e0 .m(. . . , e 0 , . . .)new I() → (I)new I()e → e0(C-FReduce)

e 6= new J()(I)e → (I)e 0(C-AnnoReduce) (I)((J)new K()) → (I)new K()

Figure 6 Small-step semantics.

4.2

Finding the Most Specific Origin: findOrigin

We proceed to give the definitions of two core functions that support method lookup, namely,
findOrigin and findOverride. Generally, findOrigin(m, I, J) finds the set of most specificinterfaces where m is originally defined. Interfaces in this set should be above interface I
and along path J. Finally with prune (defined in Section 4.4) the overridden interfaces will
be filtered out.
B Definition of findOrigin(m, I, J) :• findOrigin(m, I, J) = prune(origins)
with: origins = {K | I <: K, and K <: J ∨ J <: K,
and K[m override K] is defined}
By the definition, an interface belongs to findOrigin(m, I, J) if and only if:
It originally defines m;
It is a supertype of I (including I);
It is either a supertype or a subtype of J (including J);
Any subtype of it does not belong to the same result set because of prune.

4.3

Finding the Most Specific Overriding: findOverride

The findOrigin function only focuses on original method implementations, where all
the hierarchical overriding methods are omitted during that step. On the other hand,findOverride(m, I, J) has the assumption that J defines an original m, and this function
tries to find the interfaces with the most specific implementations that hierarchically overrides
such an m. Formally,
B Definition of findOverride(m, I, J) :• findOverride(m, I, J) = prune(overrides)
with: overrides = {K | I <: K, K <: J and K[m override J] is defined

Y. Wang, H. Zhang, B. C. d. S. Oliveira and M. Servetto

20:17

By the definition, an interface belongs to findOverride(m, I, J) if and only if:
it is between I and J (including I, J);it hierarchically overrides J.m;
any subtype of it does not belong to the same set.

4.4

Other Auxiliaries

Below we give other minor definitions of the auxiliary functions that are used in previous
sections.

B Definition of I[m override J] :• I[m override J] = Ie m(Ix x) override J {return e0 ; }with: interface I extends I {Ie m(Ix x) override J {return e0 ; } . . .}• I[m override J] = Ie m(Ix x) override J ;with: interface I extends I {Ie m(Ix x) override J ; . . .}Here I[m override J] is basically a direct lookup for method m in the body of I, where sucha method overrides J (like static dispatch). The method can be either concrete or abstract,
and the body of definition is returned. Notice that by our syntax, I[m override I] is looking
for the originally-defined method m in I.
B Definition of prune(set) :• prune(set) = {I ∈ set | @J ∈ set \ I, J <: I}
The prune function takes a set of types, and filters out those that have subtypes in thesame set. In the returned set, none of them has subtyping relation to one another, since allsupertypes have been removed.
B Definition of canOverride(m, I, J) :• canOverride(m, I, J) holds
iff: I[m override I] = Ie m(Ix x) override I . . .
J[m override J] = Ie m(Ix y) override J . . .
canOverride just checks that two original m in I and J have the same type.

B Definition of canInstantiate(I) :• canInstantiate(I) holds
iff: ∀m, ∀J ∈ findOrigin(m, I, I), findOverride(m, I, J) = {K},and K[m override J] = Ie m(Ix x) override J {return e0 ; }canInstantiate(I) checks whether interface I can be instantiated by the keyword new.
findOrigin(m, I, I) represents the set of branches that I inherits on method m. I can beinstantiated if and only if for every branch, the most specific implementation is non-abstract.

ECOOP 2018

20:18

FHJ: A Formal Model for Hierarchical Dispatching and Overriding

4.5

Properties

We present the type soundness of the model by a few theorems below, following the standard
technique of subject reduction and progress proposed by Wright and Felleisen [35]. The
proof, together with some lemmas, is presented in Appendix. Type soundness states that if
an expression is well-typed, then after many reduction steps it must reduce to a value, andits annotation is the same as the static type of the original expression.
I Theorem 1 (Subject Reduction). If Γ ` e : I and e → e 0 , then Γ ` e 0 : I.
Proof. See Appendix A.1.

J

I Theorem 2 (Progress). Suppose e is a well-typed expression, if e includes ((J)new I()) .m(v)as a sub-expression, then mbody(m, I, J) = (I0 , Ix x, Ie e0 ) and #(x) = #(v) for some I0 , Ix ,x, Ie and e0 .
Proof. See Appendix A.1.

J

I Theorem 3 (Type Soundness). If ø ` e : I and e →∗ e 0 with e 0 a normal form, then e 0 isa value v with ø ` v : I.
Proof. Immediate from Theorem 1 and Theorem 2.

J

Note that in Theorem 2, “#(x)” denotes the length of x.
Our theorems are stricter than those of Featherweight Java [14]. In FJ, the subject
reduction theorem states that after a step of reduction, the type of an expression may change
to a subtype due to subtyping. However, in FHJ, the type remains unchanged because wekeep track of the static types and use them for casting during reduction.
Finally we show that one-step evaluation is deterministic. This theorem is helpful toshow that our model of multiple inheritance is not ambiguous (or non-deterministic).
I Theorem 4 (Determinacy of One-Step Evaluation). If t → t 0 and t → t 00 , then t 0 = t 00 .
Proof. See Appendix A.1.

5

J

Discussion

In this section, we will discuss the design space and reflect about some of the design decisionsof our work. We relate our language to traits, Java interfaces as well as other languages.
Furthermore, we discuss ways to improve our work.

5.1

Abstract Methods

Abstract methods are one of the key features in most general OO languages. For example,
Java interfaces (prior to Java 8) were designed to include only method declarations, andthose abstract methods can be implemented in a class body. The formal FeatherweightJava model [14] does not include abstract methods because of the orthogonality to the corecalculus. In traits, a similar idea is to use keywords like “require” for abstract method
declarations [28]. Abstract methods provide a way to delay the implementations to future
subtypes. Using overriding, they also help to “exclude” existing implementations.
In our formalized calculus, however, abstract methods are not a completely orthogonalfeature. The canInstantiate function has to check whether an interface can be instantiatedY. Wang, H. Zhang, B. C. d. S. Oliveira and M. Servetto

20:19

Figure 7 Fork inheritance (left) and diamond inheritance (right) on abstract methods.

by looking at all the inherited branches and checking if each most specific method is concreteor not.
Our formalization has a simple form of abstract methods, which behave similarly toconventional methods with respect to conflicts. Other languages may behave differently.
For instance, in Java 8 when putting two identical abstract methods together by multiple
inheritance, there is no conflict error. In Figure 7, we use italic m to denote abstract methods.
In both cases, the Java compiler accepts the definition of C and automatically merges thetwo inherited methods m into a single one. FHJ behaves differently from Java in both cases.
In the fork inheritance case (left), C will have two distinct abstract methods corresponding
to A.m and B.m. In the diamond inheritance case, the definition of C is rejected. There are
two reasons for this difference in behaviour. Firstly, our formalization just treats abstract
methods as concrete methods with an empty body, and that simplifies the rules and proofs alot. Secondly, and more importantly, we distinguish and treat differently conflicting methods,
since they may represent different operations, even if they are abstract. Thus our model
adopts a very conservative behavior rather than automatically merging methods by default(as done in many languages). Arguably, the diamond case it is actually an intentional
conflict due to the same source T . Therefore our model conservatively rejects this case. It is
possible to change our model to account for other behaviors for abstract methods, but weview this as a mostly orthogonal change to our work, and should not affect the essence ofthe model presented here.

5.2

Orthogonal & Non-Orthogonal Extensions

Our model is designed as a minimal calculus that focuses on resolving unintentional conflicts.
Therefore, we have omitted a number of common orthogonal features including primitive
types, assignments, method overloading, covariant method return types, static dispatch, andso on. Those features can, in principle, be modularly added to the model without breaking
type soundness. For example, we present the additional syntax, typing and semantic rules ofstatic invocation below as an extension:

Expressionse::= . . . | e.J0 @J1 :: m(e)J0 [m override J1 ] = I m(J x) override J1 {return e; }Γ ` e0 : I0
I0 <: J0Γ `e:II <: J(T-StaticInvk)(S-StaticInvk)

Γ ` e0 .J0 @J1 :: m(e) : I

J0 [m override J1 ] = Ie m(Ix x) override J1 {return e0 ; }((J)new I()) .J0 @J1 :: m(v) → (Ie )[(Ix )v/x, (J0 )new I()/this]e0

ECOOP 2018

20:20FHJ: A Formal Model for Hierarchical Dispatching and Overriding

A static invocation e.J0 @J1 :: m(e) aims at finding the method m in J0 that hierarchicallyoverrides J1 , thus J0 [m override J1 ] is invoked. As shown in (S-StaticInvk), static dispatchneeds a receiver for the substitution of the “this” reference, so as to provide the latest
implementations. In fact, static dispatch is common in OO programming, as it provides
a shortcut to the reuse of old implementation easily, and super calls can also rely on thisfeature. For convenience we just make it simple above, whereas in languages like C++ orJava, the static or super invocations are more flexible, as they can climb the class hierarchy.
One non-orthogonal extension to FHJ could be to generalize the model to allow multiple
hierarchical method overriding, meaning that, we allow overriding methods to update multiple
branches instead of only one branch. This feature offers a more fine-grained mechanism for
merging and can be helpful to easily understand the structure of the hierarchy. Multiple
overriding would be useful in the following situation, for example:
interface A { void m() {...} }interface B { void m() {...} }interface C { void m() {...} }interface D extends A, B, C {void m() override A,B {...} // overrides branches A and B only
void m() override C {...} // overrides branch C}

Here D inherits from three interfaces A, B, C with conflicting methods m, but only merges
two of those methods. While we can simulate D without multiple overriding in our calculus(by introducing an intermediate class), a better approach would be to support multiple
overriding natively.
We present the modification of syntax, typing and semantic rules below (abstract methods
omitted):
Methods M ::= . . . | I m(Ix x) override J {return e; }∀Ji ∈ J, I <: JifindOrigin(m, I, Ji ) = {Ji }mbody(m, Ji , Ji ) = (K, Ix x, Ie _)(T-MoMethod)x : Ix , this : I ` e0 : I0

I0 <: Ie

Ie m(Ix x) override J {return e0 ; } OK IN I

Semantic rules themselves remain unchanged, however, we need to change slightly thedefinition of findOverride in mbody:
B Definition of findOverride(m, I, J) :• findOverride(m, I, J) = prune(overrides)
with: overrides = {K | I <: K, K <: J and K[m override J] where J ∈ J
With this approach, branches A and B are merged in the sense that they share the samecode, which can be separately updated in future interfaces. Another approach would be to
deeply merge the branches, with similar effect as introducing an intermediate interface AB to
explicitly merge the two branches. However, this approach is problematic because there isno clear mechanism for identifying and further updating the merged branches. This could be
an interesting future work to explore.
Other typical non-orthogonal extensions to FHJ could be to have fields. The design of
FHJ can be viewed as a variant of Java 8 with default methods which allows for unintentional
method conflicts. Like Java interfaces and traits, state is forbidden in FHJ. There are someY. Wang, H. Zhang, B. C. d. S. Oliveira and M. Servetto

20:21

inheritance models that also account for fields, such as C++ that uses virtual inheritance [10].
In our model, however, we can perhaps borrow the idea of interface-based programming [33],which models state with abstract state operations. This can be realized by extending ourcurrent model with static methods and anonymous classes from Java. However such an
extension requires more thought, so we leave it to future work.

5.3

Loosening the Model: Reject Early or Reject Later?

FHJ rejects the following case of diamond inheritance:interface A { void m() {...} }interface B extends A { void m() {...} }interface C extends A { void m() {...} }interface D extends B, C {}Here both B.m and C.m override A.m, and D inherits both conflicting methods without an
explicit override. In this case, automatically merging the two methods (to achieve diamond
inheritance) is not possible, which is why many models (like traits and Java 8) reject suchprograms. Moreover, keeping the two method implementations in D is problematic. In essence,hierarchical information is not helpful to disambiguate later method calls, since the two
methods share the same origin (A.m). Our calculus rejects such conflicts by the (T-Intf)
rule, where D is considered to be ill-formed. We believe that rejecting D follows the principleof models like traits and Java 8 interfaces, where the language/type-system is meant to alert
the programmer for a possible conflict early.
Nonetheless, C++ accepts the definition of D, but forbids later upcasts from D to A becauseof ambiguity. Our language is more conservative on definitions of interfaces compared to
C++, but on the upside, upcasts are not rejected. We could also loosen the model to accept
definitions such as D, and perform ambiguity check on upcasts and other expressions. Then,we would need to handle more cases than C++ because of the complication caused by thehierarchical overriding feature.

6

Related WorkWe describe related work in four parts. We first discuss mainstream popular multiple
inheritance models and then some specific models (e.g., C++ and C#) which are closest
to our work. Then we discuss related techniques used in SELF. Finally, we discuss thefoundation and related work of our formalization.

6.1

Mainstream Multiple Inheritance Models

Multiple inheritance is a useful feature in object-oriented programming, although it is difficult
to model and can cause various problems (e.g. the diamond problem [27, 29]). There are many
existing languages/models that support multiple inheritance [10, 22, 5, 28, 17, 19, 20, 11, 2].
The mixin models [5, 11, 32, 2, 13] allow naming components that can be applied to various
classes as reusable functionality units. However, the linearization (total ordering) of mixin
inheritance cannot provide a satisfactory resolution in some cases and restricts the flexibilityof mixin composition. Scala traits [22] are in fact linearized mixins and hence have the sameproblem as mixins.
Simplifying the mixins approach, traits [28, 9] draw a strong line between units of reuseand object factories. Traits act as units of reuse, containing functionality code. Classes, on theother hand, are assembled from traits and act as object factories. Java 8 interfaces are closely

ECOOP 2018

20:22

FHJ: A Formal Model for Hierarchical Dispatching and Overriding

related to traits: concrete method implementations are allowed (via the default keyword)
inside interfaces, thus allowing for a restricted form of multiple inheritance. There are also
proposals such as FeatherTrait Java [16] for extending Java with traits. Extensions [25, 26]
to the original trait model exists with various advanced features, such as renaming. As
discussed in Section 2, the renaming feature gives a workaround to the unintentional method
conflicts problem. However, it breaks structural subtyping.
Malayeri and Aldrich proposed a model CZ [17] which aims to do multiple inheritancewithout the diamond problem. Inheritance is divided into two concepts: inheritance dependency and implementation inheritance. Using a combination of requires and extends, aprogram with diamond inheritance is transformed to one without diamonds. Moreover, fields
and multiple inheritance can coexist. However untangling inheritance also untangles theclass structure. In CZ, not only the number of classes but also the class hierarchy complexity
increases.
The above-mentioned models/languages support multiple inheritance, focusing on diamond inheritance. They handle method conflicts in the same way, by simply disallowing two
methods with the same signature from two different units to coexist. In contrast, our work
provides mechanisms that allow methods with the same signatures, but different parents
to coexist in a class. Disambiguation is possible in many cases by using both static anddynamic type information during method dispatching. In the cases where real ambiguity
exists, FHJ’s type system can reject interface definitions and/or method calls statically.

6.2

Resolving Unintentional Method Conflicts

A few language implementations have realized the problem of unintentional conflicts andprovide some support for it.
C++ model. C++ supports a very flexible inheritance model. C++ allows the existence of
unintentional conflicts and users may specify a hierarchical path via casts for disambiguation,
as discussed in Section 2. With virtual methods, dynamic dispatch is used and the method
lookup algorithm will find the most specific method definition. A contribution of our work is
to provide a minimal formal model of hierarchical dispatching, whereas C++ can be viewed
as a real-world implementation. There are several formalizations [34, 24, 23] in the literaturemodeling various C++ features. However, as far as we know, there is no formal model that
captures this aspect of the C++ method dispatching model. Apart from this, as discussed in
Section 5.3, FHJ conservatively rejects some interface/class definitions that C++ accepts,
and upcasts are never rejected since the ambiguity is prevented beforehand.
Although C++ supports hierarchical dispatching, it does not support hierarchical overriding. However, there are some possible workarounds that can mimic hierarchical overriding,including the MiddleMan approach4 , the interface classes pattern as described in Section
25.6 of [31], the LotterySimulation discussion in [30]. Since these workarounds share the same
spirit, we will discuss in detail the MiddleMan approach, with the code shown in Figure 8.
In this example, classes A and B are two classes that both define a method with the same
name m unintentionally.
Class MiddleMan, as its name suggests, acts as a middleman between its class C and its
parents A, B. MiddleMan defines a virtual method m that overrides a parent method m anddelegates the implementation to another method m_impl that takes this as a parameter. C++

4https://stackoverflow.com/questions/44632250/can-i-do-mimic-things-likes-this-partial-ove
rride-in-c

Y. Wang, H. Zhang, B. C. d. S. Oliveira and M. Servetto

20:23

class A { public: virtual void m() {cout << "MA" << endl;}};class B { public: virtual void m() {cout << "MB" << endl;}};template<class C>class MiddleMan : public C {void m() override final { m_impl(this); }protected:
virtual void m_impl(MiddleMan*) { return this->C::m(); }};class C : public MiddleMan<A>, public MiddleMan<B> {private:void m_impl (MiddleMan<A>*) override {cout << "MA2" << endl;}
void m_impl (MiddleMan<B>*) override {cout << "MB2" << endl;}};

int main(){
C* c = new C();((A*)c)->m();//print "MA2"
return 0;}

Figure 8 The MiddleMan approach.

supports method overloading, so that multiple m_impl methods with different parametertypes can coexist. When defining class C, we specify the parents to be MiddleMan<A>,
MiddleMan<B> instead of A, B. In this way, programmers may define new versions of A.mand B.m in class C by providing the corresponding m_impl methods. Then in the client
code, the method call ((A*)c)->m() will print out the string "MA2", as expected. Although
this workaround can help us defining partial method overrides to a certain extent, thedrawbacks are obvious. Firstly, the approach is complex and requires the programmer to fully
understand this approach. Moreover, the lack of direct syntax support makes MiddleMan
code cumbersome to write. Finally, the approach is ad-hoc, meaning that the class MiddleMan
shown in Figure 8 is not general enough to be used in other cases: more middlemen areneeded if partial method overrides happen in other classes; and it is even worse when return
types differ.
C# explicit method implementations. Explicit method implementations is a special
feature supported by C#. As described in C# documentation [19], a class that implements aninterface can explicitly implement a member of that interface. When a member is explicitly
implemented, it can only be accessed through an instance of the interface. Explicit interface
implementations allow an interface to inherit multiple interfaces that share the same member
names and give each interface member a separate implementation.
Explicit interface member implementations have two advantages. Firstly, they allow
interface implementations to be excluded from the public interface of a class. This isparticularly useful when a class implements an internal interface that is of no interest
to a consumer of that class or struct. Secondly, they allow disambiguation of interface
members with the same signature. However, there are two critical differences to FHJ: (1)default method implementations are not allowed in C# interfaces; (2) there is only one
level of conflicting method implementations at the class that implements the multiple parent
interfaces. Further overriding of those methods is not possible in subclasses.
Languages using hygienicity. In NextGen/MixGen [1], HygJava [15] and Magda [3], hygienicity is proposed to deal with unintentional method conflicts. The idea is to give a method
a unique identifier by prefixing the name with an unambiguous path. As shown in Figure 9,
the prefix HelloWorld in the method call (new HelloWorld []).HelloWorld.MainMatter() is

ECOOP 2018

20:24

FHJ: A Formal Model for Hierarchical Dispatching and Overriding

mixin HelloWorld of Object =new Object MainMatter()begin"Hello world".String.print();
end;
end;
(new HelloWorld []).HelloWorld.MainMatter();

Figure 9 Full-qualified name of method calls in Magda.
mixin A of Object =new String m()
begin
return "A";
end;
end;
mixin B of Object =new String m()
begin
return "B";
end;
end;
mixin C of A, B =new String m()
begin
return "C";
end;
end;

Figure 10 Code in Magda.

mandatory. So writing programs in these languages is tedious if not supported by a specialized IDE, that aids filling prefix/method information. The advantage of this approach,compared to ours, is that it does not require any additional notion for method dispatching.
Indeed the compilation strategy is simple, just by generating conventional code (say in Javaor C++) with method names attached with prefixes. Unfortunately, the disadvantage isthat some expressive power is lost. In particular merging methods arising from diamond
inheritance is not possible because the methods have different prefixes. As shown in Figure 10,
two methods m from different branches A and B cannot be overridden by the method m inC because they are regarded as unrelated methods, and m in C is just another new methodthat has nothing to do with A.m or B.m. The reason is that in these hygienic approaches,
path names are used to distinguish different methods. In contrast, our model can deal with
unintentional conflicts, as well as merged methods because our semantics is not simply basedon prefixing. Instead, our model keeps the names of methods unchanged, and our direct
operational semantics takes static and dynamic type information into account at runtime
when doing method dispatching. Finally, the multiple inheritance model in Magda is basedon Mixins, whereas FHJ is based on traits. Thus, Magda inherits all limitations of Mixins(such as the linearization problem, etc).

6.3

Hierarchical Dispatch in SELF

As we have discussed before, although the mix of static and dynamic dispatch is particularly
useful under certain circumstances, it has received little research attention. In the prototypebased language SELF [6], inheritance is a basic feature. SELF does not include classes but

Y. Wang, H. Zhang, B. C. d. S. Oliveira and M. Servetto

20:25

instead allows individual objects to inherit from (or delegate to) other objects. Although it
is different from class-based languages, the multiple inheritance model is somewhat similar.
The SELF language supports multiple (object) inheritance in a clever way. It not only
develops the new inheritance relation with prioritized parents but also adopts sender pathtiebreaker rule for method lookup. In SELF “if two slots with the same name are defined inequal-priority parents of the receiver, but only one of the parents is an ancestor or descendantof the object containing the method that is sending the message, then that parent’s slot takes
precedence over the over parent’s slot”. Similarly to our model, this sender path tiebreaker
rule resolves ambiguities between unrelated slots. However, it is used in a prototype-based
language setting and it does not support method hierarchical overriding as FHJ does.

6.4

Formalization Based on Featherweight Java

Featherweight Java (FJ) [14] is a minimal core calculus of the Java language, proposed by
Igarashi et. al. There are many models built on Featherweight Java, including FeatherTrait [16], Featherweight defenders [12], Jx [21], Featherweight Scala [8], and so on. FJ
provides the standard model of formalizing Java-like object-oriented languages and is easily
extensible. In terms of formalization, the key novelty of our model is making use of various
types (such as parameter types, method return types, etc) to track the static types as well as
the dynamic types during reduction. As far as we know, this technique has not appeared in
the literature before. This notion is of vital importance in our hierarchical dispatch algorithm,
and it allows for a more precise subject-reduction theorem as discussed in Section 3.

7

Conclusion

This paper proposes FHJ as a formalized multiple inheritance model for unintentional method
conflicts. Previous approaches either do not support unintentional method conflicts, thus haveto compromise between code reuse and type safety, or do not fully support overriding in thepresence of unintentional conflicts. To deal with unintentional method conflicts we introduce
two key mechanisms: hierarchical dispatching and hierarchical overriding. Hierarchicaldispatching is inspired by the mechanisms in C++. We provide a minimal formal modelof hierarchical dispatching in FHJ. Such an algorithm makes use of both dynamic type
information and static information from either upcasts or parameters’ information. It not onlyoffers code reuse and dynamic dispatch, but also ensures unambiguity using our hierarchicaldispatching algorithm for method resolution. Additionally we introduce hierarchical overriding
to allow conflicting methods in different branches to be individually overridden.
FHJ is formalized following the style of Featherweight Java and proved to be sound.
A prototype interpreter is implemented in Scala. We believe that the formalization ofhierarchical dispatching features is general and can be safely embedded in other OO models,so as to have support for the fork inheritance.
Our model can certainly be improved in some aspects. As discussed in Section 5, there
are orthogonal and non-orthogonal features that can potentially be added to the design space.
The future work relates to loosening the model without giving up its soundness, together
with more exploration on supporting fields in the multiple inheritance setting.
References1

Eric Allen, Jonathan Bannet, and Robert Cartwright. A first-class approach to genericity. In Proceedings of the 18th Annual ACM SIGPLAN Conference on Object-oriented

ECOOP 2018

20:26

FHJ: A Formal Model for Hierarchical Dispatching and Overriding

2
3

4
5
6
7
8
9

10
11
12

13
14
15
16
17
18
19
20
21
22

23
24

Programing, Systems, Languages, and Applications, OOPSLA ’03, pages 96–114, New
York, NY, USA, 2003. ACM. URL: http://doi.acm.org/10.1145/949305.949316, doi:
10.1145/949305.949316.
Davide Ancona, Giovanni Lagorio, and Elena Zucca. Jam—designing a java extension withmixins. ACM Trans. Program. Lang. Syst., 25(5):641–712, 2003.
Viviana Bono, Jarek Kuśmierek, and Mauro Mulatero. Magda: A new language formodularity. In Proceedings of the 26th European Conference on Object-Oriented Programming, ECOOP’12, pages 560–588, Berlin, Heidelberg, 2012. Springer-Verlag. URL: http://dx.doi.org/10.1007/978-3-642-31057-7_25, doi:10.1007/978-3-642-31057-7_25.
Viviana Bono, Enrico Mensa, and Marco Naddeo. Trait-oriented programming in java 8.
In PPPJ ’14, 2014.
Gilad Bracha and William Cook. Mixin-based inheritance. In OOPSLA/ECOOP ’90, 1990.
Craig Chambers, David Ungar, Bay-Wei Chang, and Urs Hölzle. Parents are shared partsof objects: Inheritance and encapsulation in self. Lisp Symb. Comput., 4(3), July 1991.
Steve Cook. Varieties of inheritance. In OOPSLA ’87 Panel P2, 1987.
Vincent Cremet, François Garillot, Sergueï Lenglet, and Martin Odersky. A core calculus
for scala type checking. In MFCS ’06, 2006.
Stéphane Ducasse, Oscar Nierstrasz, Nathanael Schärli, Roel Wuyts, and Andrew P. Black.
Traits: A mechanism for fine-grained reuse. ACM Trans. Program. Lang. Syst., 28(2):331–
388, 2006.
Margaret A Ellis and Bjarne Stroustrup. The annotated C++ reference manual. AddisonWesley, 1990.
Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen. Classes and mixins. In
POPL ’98, 1998.
Brian Goetz and Robert Field. Featherweight defenders: A formal model for virtual extension methods in java. http://cr.openjdk.java.net/~briangoetz/lambda/
featherweight-defenders.pdf, 2012.
James Hendler. Enhancement for multiple-inheritance. In OOPWORK ’86, 1986.
Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight java: A minimalcore calculus for java and gj. ACM Trans. Program. Lang. Syst., 23(3):396–450, 2001.
Jaroslaw DM Kusmierek and Viviana Bono. Hygienic methods - introducing hygjava. Journal of Object Technology, 6(9):209–229, 2007.
Luigi Liquori and Arnaud Spiwack. Feathertrait: A modest extension of featherweight java.
ACM Trans. Program. Lang. Syst., 30(2):11, 2008.
Donna Malayeri and Jonathan Aldrich. Cz: Multiple inheritance without diamonds. In
OOPSLA ’09, 2009.
B Meyer. Eiffel: Programming for reusability and extendibility. SIGPLAN Not., 22(2),1987.
Microsoft. Csharp explicit interface member implementations document. https://msdn.
microsoft.com/en-us/library/aa664591(v=vs.71).aspx, 2003.
David A. Moon. Object-oriented programming with flavors. In OOPSLA ’86, 1986.
Nathaniel Nystrom, Stephen Chong, and Andrew C. Myers. Scalable extensibility via
nested inheritance. In OOPSLA ’04, 2004.
Martin Odersky, Philippe Altherr, Vincent Cremet, Burak Emir, Sebastian Maneth,
Stéphane Micheloud, Nikolay Mihaylov, Michel Schinz, Erik Stenman, and Matthias Zenger.
An overview of the scala programming language. Technical report, 2004.
G. Ramalingam and Harini Srinivasan. A member lookup algorithm for c++. In PLDI ’97,
1997.
Tahina Ramananandro. Mechanized Formal Semantics and Verified Compilation for C++
Objects. PhD thesis, Université Paris-Diderot-Paris VII, 2012.

Y. Wang, H. Zhang, B. C. d. S. Oliveira and M. Servetto

25
26
27
28
29
30
31
32

33
34
35
36

20:27

John Reppy and Aaron Turon. A foundation for trait-based metaprogramming. In FOOL/WOOD ’06, 2006.
John Reppy and Aaron Turon. Metaprogramming with traits. In ECOOP ’07, 2007.
Markku Sakkinen. Disciplined inheritance. In ECOOP ’89, 1989.
Nathanael Schärli, Stéphane Ducasse, Oscar Nierstrasz, and Andrew P. Black. Traits:
Composable units of behaviour. In ECOOP ’03, 2003.
Ghan Bir Singh. Single versus multiple inheritance in object oriented programming. SIGPLAN OOPS Mess., 1995.
Bjarne Stroustrup. The design and evolution of C++. Pearson Education India, 1994.
Bjarne Stroustrup. The C++ programming language. Pearson Education India, 1995.
Marc Van Limberghen and Tom Mens. Encapsulation and composition as orthogonal
operators on mixins: A solution to multiple inheritance problems. Object Oriented Systems,
3(1):1–30, 1996.
Yanlin Wang, Haoyuan Zhang, Bruno C. d. S. Oliveira, and Marco Servetto. Classless java.
In GPCE ’16, 2016.
Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, and Frank Tip. An operational semantics and type safety prooffor multiple inheritance in c++. In OOPSLA ’06, 2006.
A.K. Wright and M. Felleisen. A syntactic approach to type soundness. Inf. Comput.,
115(1):38–94, 1994.
Matthias Zenger and Martin Odersky. Independently extensible solutions to the expression
problem. In FOOL ’05, 2005.

ECOOP 2018

20:28

FHJ: A Formal Model for Hierarchical Dispatching and Overriding

A

Appendix

A.1

ProofsI Lemma 5. If mbody(m, Id , Is ) = (J, Ix x, Ie e0 ), then x : Ix , this : J ` e0 : I0 for some
I0 <: Ie .
Proof. By the definition of mbody, the target method m is found in J. By the method typing
rule (T-Method), there exists some I0 <: Ie such that x : Ix , this : J ` e0 : I0 .
J
I Lemma 6 (Weakening). If Γ ` e : I, then Γ, x : J ` e : I.
Proof. Straightforward induction.

J

I Lemma 7 (Method Type Preservation). If mbody(m, J, J) = (K, Ix _, Ie _), then for any
I <: J, mbody(m, I, J) = (K 0 , Ix _, Ie _).
Proof. Since mbody(m, J, J) is defined, by (T-Intf) we derive that mbody(m, I, J) is also
defined. Suppose thatfindOrigin(m, J, J) = {I0 }findOverride(m, J, I0 ) = {K}findOrigin(m, I, J) = {I00 }findOverride(m, I, I00 ) = {K 0 }Below we use I[m ↑ J] to denote the type of method m defined in I that overrides J. We
have to prove that K 0 [m ↑ I00 ] = K[m ↑ I0 ]. Two facts:
A. By (T-Intf), canOverride ensures that an override between any two original methods
preserves the method type. Formally,
I1 <: I2 ⇒ I1 [m ↑ I1 ] = I2 [m ↑ I2 ]B. By (T-Method) and (T-AbsMethod), any partial override also preserves method
type. Formally,
I1 <: I2 ⇒ I1 [m ↑ I2 ] = I2 [m ↑ I2 ]By definition of findOverride, K <: I0 , K 0 <: I00 . By Fact B,
K[m ↑ I0 ] = I0 [m ↑ I0 ]K 0 [m ↑ I00 ] = I00 [m ↑ I00 ]Hence it suffices to prove that I00 [m ↑ I00 ] = I0 [m ↑ I0 ]. Actually when calculating
findOrigin(m, J, J), by the definition of findOrigin we know that I0 <: J and I0 [m override I0 ]is defined. So when calculating findOrigin(m, I, J) with I <: J, I0 should also appear in
the set before pruned, since the conditions are again satisfied. But after pruning, only I00 is
obtained, by definition of prune it implies I00 <: I0 . By Fact A, the proof is done.
J
I Lemma 8 (Term Substitution Preserves Typing). If Γ, x : Ix ` e : I, and Γ ` y : Ix , thenΓ ` [y/x]e : I.

Y. Wang, H. Zhang, B. C. d. S. Oliveira and M. Servetto

20:29

Proof. We prove by induction. The expression e has the following cases:
Case Var. Let e = x. If x ∈/ x, then the substitution does not change anything.
Otherwise, since y have the same types as x, it immediately finishes the case.
Case Invk. Let e = e0 .m(e). By (T-Invk) we can suppose thatΓ, x : Ix ` e0 : I0

mbody(m, I0 , I0 ) = (_, J _, I _)Γ, x : Ix ` e : Ie

Ie <: JΓ, x : Ix ` e : I

By induction hypothesis,Γ ` [y/x]e0 : I0Γ ` [y/x]e : Ie

Again by (T-Invk), Γ ` [y/x]e : I.
Case New. Straightforward.
Case Anno. Straightforward by induction hypothesis and (T-Anno).
J

A.1.1

Proof for Theorem 1

Proof.
Case S-Invk. Let
e = ((J)new I()).m(v)Γ ` e : Ie0e = (Ie0 )[(Ix )v/x, (I0 )new I()/this]e0
mbody(m, I, J) = (I0 , Ix x, Ie0 e0 )Since mbody(m, I, J) is defined, the definition of mbody ensures that I <: J. And since e iswell-typed, by (T-Invk),
Γ ` v : Iv Iv <: Ix
By the rules (T-Anno) and (T-New),Γ ` (Ix )v : IxΓ ` (I0 )new I() : I0

On the other hand, by Lemma 5,
x : Ix , this : I0 ` e0 : Ie0 0

Ie0 0 <: Ie0

By Lemma 6,
Γ, x : Ix , this : I0 ` e0 : Ie0 0
Hence by Lemma 8, the substitution preserves typing, thusΓ ` [(Ix )v/x, (I0 )new I()/this]e0 : Ie0 0
Since Ie0 0 <: Ie0 , the conditions of (T-Anno) are satisfied, hence Γ ` e 0 : Ie0 . Now
we only need to prove that Ie0 = Ie . Since Ie0 is from mbody(m, I, J), whereas Ie is frommbody(m, J, J), by the rule (T-Invk) on e. Since I <: J, by Lemma 7, Ie0 = Ie .
Case C-Receiver. Straightforward induction.
Case C-Args. Straightforward induction.
Case C-StaticType. Immediate by (T-Anno).
Case C-FReduce. Immediate by (T-Anno) and induction.
Case C-AnnoReduce. Immediate by (T-Anno) and transitivity of <:.
J

ECOOP 2018

20:30FHJ: A Formal Model for Hierarchical Dispatching and Overriding

A.1.2

Proof for Theorem 2

Proof. Since e is well-typed, by (T-Invk) and (T-Anno) we know that
I <: J, and mbody(m, J, J) is defined
By (T-Intf), mbody(m, I, J) is also defined, and the type checker ensures the expected
number of arguments.
On the other hand, since I <: J, by the definition of findOrigin,
findOrigin(m, I, J) ⊆ findOrigin(m, I, I)

By (T-New), canInstantiate(I) = T rue. By the definition of canInstantiate, any
J0 ∈ findOrigin(m, I, I) satisfies that findOverride(m, I, J0 ) contains only one interface, inwhich the m that overrides J0 is a concrete method. Therefore mbody(m, I, J) also provides aconcrete method, which finishes the proof.
J

A.1.3

Proof for Theorem 4

Proof. The Proof is done by induction on a derivation of t → t 0 , following the book TAPL.
If the last rule used in the derivation of t → t 0 is (S-Invk), then we know that t has theform ((J)new I()) .m(v) with I, J, m determined. Now it is obvious that the last rule in thederivation of t → t 00 should also be (S-Invk) with the same I, J, m. Since mbody(m, I, J)
is a function that given the same input will calculate the same result, we know the two
induction results are the same, thus t 0 = t 00 is immediately proved.
If the last rule used in the derivation of t → t 0 is (C-Receiver), then t has the form
e0 .m(e) and e0 → e00 . Since e0 is not a value, the last rule used in t → t 00 has to be(C-Receiver) (other rules do not match) too. Assume in the reduction t → t 00 , e0 → e000 ,thus e00 .m(e) = e000 .m(e). Thus, t 0 = t 00 proved.
If the last rule used in the derivation of t → t 0 is (C-StaticType), then t is fixed tobe new I(). The last rule used in t → t 00 has to be (C-StaticType), and obviously,t 0 = t 00 = (I)new I().
If the last rule used in the derivation of t → t 0 is (C-FReduce), then t has the form(I)e and e → e 0 . The last rule used in t → t 00 cannot be (C-StaticType) because it
requires t to be new I(); it can neither be (C-AnnoReduce) because it requires t tobe (I)((J)new K()) where (J)new K() is already a value. So the last rule used in t → t 00
can only be (C-FReduce) (other rules do not match). Assume in the reduction t → t 00 ,e → e 00 , and (I)e → (I)e 00 . By induction hypothesis, e 0 = e 00 , thus t 0 = t 00 proved.
If the last rule used in the derivation of t → t 0 is (C-AnnoReduce), then the formof t is fixed to be (I)((J)new K()). Since (I)((J)new K()) is not reducible, the rule (CFReduce) does not apply. The only rule applies in t → t 00 is (C-AnnoReduce). Thust 0 = t 00 = (I)new K() proved.
If the last rule used in the derivation of t → t 0 is (C-Args), then t has the form
v.m(..., e, ...) and e → e 0 . The last rule used in t → t 00 cannot be (S-Invk) because it
requires all arguments to be values. Thus only (C-Args) applies to t → t 00 . Assume in
the reduction t → t 00 , e → e 00 . By induction hypothesis, e 0 = e 00 , thus v.m(..., e 0 , ...) =v.m(..., e 00 , ...), thus t 0 = t 00 proved.
J