# What does valid method overriding mean?

In Types and Programming Languages by Pierce, from p257 to p258, about featherweight Java,

The predicate override(m, D, C→C0) judges whether a method m with argument types C and a result type C0 may be deﬁned in a subclass of D. In case of overriding, if a method with the same name is declared in the superclass then it must have the same type.

I am not sure what the predicate override(m, D, C→C0) means.

Does the predicate apply only to the case of overriding? (The first sentence doesn't imply so.)

Isn't it always possible to define a method with any name and any type in any class?

• In case of non-overriding, that is true.
• In case of overriding, that is also true.

Could you give examples where it is possible and where it isn't?

Figure 19-2: Featherweight Java (auxiliary deﬁnitions) says:

Valid method overriding:

If mtype(m, D) = E→E0 implies C = E and C0 = E0, then override(m, D, C→C0 )

How can mtype(m, D) = E→E0 imply C = E and C0 = E0? mtype(m, D) = E→E0 only means that class D has a method m whose type is E→E0.

Why is "mtype(m, D) = E→E0 implies C = E and C0 = E0" a condition for override(m, D, C→C0 )?

Thanks.

The important sentence in the first quote is

In case of overriding, if a method with the same name is declared in the superclass then it must have the same type.

So if you have

class C1 { ... }
class C2 { ... }

class Cls {
C1 foo(C2 x) { ... }
}


override(foo, Cls, (C2)->C1) holds but override(foo, Cls, (C2)->C2) doesn't; the subclass

class SubCls extends Cls {
C2 foo(C2 x) { ... }
}


is illegal. In FJ, you can't have

class SubCls extends Cls {
C2 foo() { ... }
}


either, unlike in Java.

If mtype(m, D) = E→E0 implies C = E and C0 = E0, then override(m, D, C→C0 )

This is implicitly quantified "for all E and E0". If mtype(m, D) is undefined, then mtype(m, D) = E→E0 is always false, so it implies anything. If it's defined, then "mtype(m, D) = E→E0 implies C = E and C0 = E0" is equivalent to mtype(m, D) = C→C0.

So it ends up being the same as

If mtype(m, D) = C→C0 or mtype(m, D) is undefined, then override(m, D, C→C0)

(unless I went wrong somewhere)