Subtype Relation

type-theory

Definition

Subtype Relation

Let and be types. is called subtype of , denoted as , if anywhere where an expression of type is expected, an expression of type can be safely used (Liskov Substitution Principle).

The subtype relation forms a partial order.

Language-Specific

Java

Let be reference types.

• (reflexive)
• (transitive)
• (antisymmetric)

Thus, the subtype relation is a partial order.

• Every dynamic type is a Java class
• is not an object of , whereby the compiler accepts it

Assumption: Method comments in and are compatible, with :

• Comment in explains the same method as comment in
• Comment in can be more concrete
• Comment in can be more abstract

Object-Oriented Perspective

A type is subtype of type iff:

1. 1. i.e. type of is subtype of type
2. 1. i.e. type of is equivalent to type
3. 1. parameter count and types are equal
   2. parameter types are compatible
   3. result type of is subtype of result type in
   4. does not throw more exceptions than