Inheritance

Overview

Single inheritance of classes, and without field expressions or superclass constructor expressions (just values)

Syntax

Extend the class of declarations by:

DecAtom ::= ...

| ClassKind class Id Params extends Id Vals { ClassBody } (DecAtom Class)

Dynamic semantics

Extend the grammar of resources:

Resource ::= ...

| ClassKind class Params extends Id Vals { ClassRes }{ ClassBody } (Resource Class)

The reduction relation is extended with (when CV₁ contains all the fields and methods of CV₃):

L[CK₁ class I₁ PS₁ extends I₂ VS₂ { CV₁ } D] | secret I₁; L[D] | (Redn Class)

L<I₂ = CK₂ class PS₂ extends I₃ VS₃ { CV₂ CV₃ }{ CB₂ }> L<I₁ = CK₁ class PS₁ extends I₂ VS₂ { CV₂[VS₂/PS₂] CV₁ }{ CV₁ }>

L<I₂ = CK₂ class PS₂ extends I₃ VS₃ { CV₂ CV₃ }{ CB₂ }>

Static semantics

Extend the grammar of contexts with type rules for classes:

ConAtom ::= ...

| Id : ClassKind class Types extends ClassName { ClassType } (ConAtom Class)

Judgements Context ClassName extends ClassName:

(Extends Defn)

C₁ I : CK class TS extends CN { CT } C₂ I extends CN

Extend the judgements Context Context : context with:

C₀ C₁ CN : class { CT₂ }

C₀ C₁ TS : types

C₀ | C₁ CT₁ : class type

C₀ C₁ CT₁ <: CT₂

(Context Class) [C₁ = (I₁ : CK class TS extends CN { CT₁ })]

C C₁ : context

Extend the judgements for declarations Context Dec : Context with:

C₀ CN₂ : [local] class

C₀ CN₂ : class { CT₂ CT₃ }

C₀ CN₂ (TL₂) : constructor

C₀ C₁ ((PL₁) : (TL₁)) : C₂

C₀ C₁ C₂ ES₂ : TS₂

C₀ | C₁ | C₂ | I₁ CB₁ : CT₁

C₀ C₁ CT₁ <: CT₃

C₀ C₁ CT₂ CT₁ : class type

(Context Class) [C₁ = (I₁ : local class (TL₁) extends CN₂ { CT₂ CT₁ })]

C₀ (local class I₁ (PL₁) extends CN₂ (EL₂) { CB₁ }) : C₁

Subtyping

Subsumption rules:

C C₀ <: C₁

C D : C₀

(Dec Subsumption)

C D : C₁

C A : T₁

C T₁ <: T₂

(Assign Subsumption)

C A : T₂

C V: T₁

C T₁ <: T₂

(Val Subsumption)

C V : T₂

Judgements for subtyping types Con Type <: Type:

C CN₁ extends CN₂

(SubType Object)

C object CN₁ <: object CN₂

C CN₁ extends CN₂

(SubType Record)

C record CN₁ <: record CN₂

(SubType Refl)

C T <: T

C T₁ <: T₂

C T₂ <: T₃

(SubType Trans)

C T₁ <: T₃

Judgements for subtyping types Con Types <: Types:

C T₁₁ <: T₁₂

...

C T_n₁ <: T_n₂

(SubTypes)

C (T₁₁, ... , T_n₁) <: (T₁₂, ... , T_n₂)

Judgements for subtyping contexts Con Con <: Con:

C T₁ <: T₂

(SubContext Id)

C (I : T₁;) <: (I : T₂;)

(SubContext Refl)

C C₁ <: C₁

C C₁ <: C₂

C C₂ C₃ <: C₄

(SubContext Comp)

C C₁ C₃ <: C₂ C₄

(SubContext Top)

C C₁ <: ()

Judgements for subtyping class types Con ClassType <: ClassType:

C (FT₁ FT₅) <: (FT₂ FT₆)

C FT₃ <: FT₄

C (MT₁ MT₃) <: (MT₂ MT₄)

(SubClassType)

C abstract { FT₁ MT₁ } static { FT₃ } FT₅ MT₃ <:

abstract { FT₂ MT₂ } static { FT₄ } FT₆ MT₄

Judgements for subtyping field types Con FieldType <: FieldType:

C T₁ <: T₂

(SubFieldType Id)

C field I : T₁; <: field I : T₂;

C FT₁ <: FT₂

C FT₃ <: FT₄

(SubFieldTypeComp)

C FT₁ FT₃ <: FT₂ FT₄

(SubFieldType Top)

C FT₁ <: ()

Judgements for subtyping method types Con MethodType <: MethodType:

C T₁ <: T₂

C TS₂ <: TS₁

(SubMethodType Id)

C MK method I TS₁ : T₁; <: MK method I TS₂ : T₂;

C MT₁ <: MT₂

C MT₃ <: MT₄

(SubMethodType Comp)

C MT₁ MT₃ <: MT₂ MT₄

(SubMethodType Top)

C MT₁ <: ()

DecAtom	::=	...
	\|	ClassKind class Id Params extends Id Vals { ClassBody }	(DecAtom Class)

Resource	::=	...
	\|	ClassKind class Params extends Id Vals { ClassRes }{ ClassBody }	(Resource Class)

L[CK₁ class I₁ PS₁ extends I₂ VS₂ { CV₁ } D] \|	secret I₁; L[D] \|	(Redn Class)
L<I₂ = CK₂ class PS₂ extends I₃ VS₃ { CV₂ CV₃ }{ CB₂ }>	L<I₁ = CK₁ class PS₁ extends I₂ VS₂ { CV₂[VS₂/PS₂] CV₁ }{ CV₁ }>
	L<I₂ = CK₂ class PS₂ extends I₃ VS₃ { CV₂ CV₃ }{ CB₂ }>

ConAtom	::=	...
	\|	Id : ClassKind class Types extends ClassName { ClassType }	(ConAtom Class)

			(Extends Defn)
C₁ I : CK class TS extends CN { CT } C₂		I extends CN

C₀ C₁	CN : class { CT₂ }
C₀ C₁	TS : types
C₀ \| C₁	CT₁ : class type
C₀ C₁	CT₁ <: CT₂
		(Context Class)	[C₁ = (I₁ : CK class TS extends CN { CT₁ })]
C	C₁ : context

C₀	CN₂ : [local] class
C₀	CN₂ : class { CT₂ CT₃ }
C₀	CN₂ (TL₂) : constructor
C₀ C₁	((PL₁) : (TL₁)) : C₂
C₀ C₁ C₂	ES₂ : TS₂
C₀ \| C₁ \| C₂ \| I₁	CB₁ : CT₁
C₀ C₁	CT₁ <: CT₃
C₀ C₁	CT₂ CT₁ : class type
		(Context Class)	[C₁ = (I₁ : local class (TL₁) extends CN₂ { CT₂ CT₁ })]
C₀	(local class I₁ (PL₁) extends CN₂ (EL₂) { CB₁ }) : C₁

C	CN₁ extends CN₂
		(SubType Object)
C	object CN₁ <: object CN₂

C	CN₁ extends CN₂
		(SubType Record)
C	record CN₁ <: record CN₂

C		T₁₁ <: T₁₂
	...
C		T_n₁ <: T_n₂
			(SubTypes)
C		(T₁₁, ... , T_n₁) <: (T₁₂, ... , T_n₂)

C	C₁ <: C₂
C C₂	C₃ <: C₄
		(SubContext Comp)
C	C₁ C₃ <: C₂ C₄

C	(FT₁ FT₅) <: (FT₂ FT₆)
C	FT₃ <: FT₄
C	(MT₁ MT₃) <: (MT₂ MT₄)
		(SubClassType)
C	abstract { FT₁ MT₁ } static { FT₃ } FT₅ MT₃ <:
	abstract { FT₂ MT₂ } static { FT₄ } FT₆ MT₄

C	T₁ <: T₂
		(SubFieldType Id)
C	field I : T₁; <: field I : T₂;

C	FT₁ <: FT₂
C	FT₃ <: FT₄
		(SubFieldTypeComp)
C	FT₁ FT₃ <: FT₂ FT₄

C	T₁ <: T₂
C	TS₂ <: TS₁
		(SubMethodType Id)
C	MK method I TS₁ : T₁; <: MK method I TS₂ : T₂;

C	MT₁ <: MT₂
C	MT₃ <: MT₄
		(SubMethodType Comp)
C	MT₁ MT₃ <: MT₂ MT₄