In Types and Programming Languages by Pierce, from p257 to p258, about featherweight Java,
override(m, D, C→C0)judges whether a method
mwith argument types
Cand a result type
C0may 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:
mtype(m, D) = E→E0implies
C = Eand
C0 = E0, then
override(m, D, C→C0 )
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
Why is "
mtype(m, D) = E→E0 implies
C = E and
C0 = E0" a condition for
override(m, D, C→C0 )?