MetaFJig (a meta-circular composition language for Java-like classes)

MetaFJig - A meta-circular composition language for Java-like classes (full version with proofs)

Marco Servetto and Elena Zucca

DISI, Univ. of Genova, v. Dodecaneso 35, 16146 Genova, Italy email: {servetto,zucca}@disi.unige.it

Abstract. We propose a Java-like language where class denitions are

rst class values, hence new classes can be derived from existing, rather than by a xed mechanism like inheritance, by exploiting the full power of the language on top of a small set of primitive composition operators. Hence, compilation of a class table requires to perform (meta-)reduction steps, by a process that we call . This approach diers from meta-programming techniques provided in mainstream languages since it is meta-circular, hence the programmer does not need to learn new syntax and idioms. Compile-time execution is guaranteed to be sound (not to get stuck) by a lightweight technique, where class composition errors are detected dynamically, and conventional typing errors are detected by interleaving typechecking with meta-reduction steps. This allows a modular approach, that is, compile-time execution is dened, and can be implemented, on top of typechecking and execution of the underlying language. Moreover, programmers can handle errors due to composition operators. Besides soundness, our technique ensures an additional important property called soundness, that is, typing errors never originate from (meta-)code in already compiled programs.

compile-time execution

meta-level

1

Introduction

The recognized need of going beyond inheritance has led, in the last years, to a variety of proposals for improving the exibility and expressivity of objectoriented programming, such as, e.g., mixin classes [15,3], virtual classes [11,12], generic classes as in Java 5, mixin modules [13,4] and other proposals for adding a module/component level [24,1], traits [10,26,14,23]. All these proposals share a common limitation: users are provided with a xed set of composition mechanisms. A natural way to overcome this limitation is to allow programmers to write (meta-)code that can be used to generate customized code. However, meta-programming techniques provided in mainstream Java-like

1 such as

languages,

template meta-programming

in C++, can be very dicult to

understand, since their syntax and idioms are esoteric compared to conventional

1

By Java-like languages we mean object-oriented class-based languages with nominal types, such as Java, C++ and C#.

programming, and well-formedness of generated code can only be checked a posteriori, making the whole process hard to debug.

limited meta-programming approach which sound. That is, respectively:

In this paper, instead, we propose a is

meta-circular



and

Class denitions

2 are rst-class values, hence new classes can be derived from

existing, rather than by a xed mechanism like inheritance, by exploiting the full power of the language on top of a small set of primitive composition operators, as in [7,6,20]. Hence, compilation of a class table requires to perform



(meta-)reduction steps, by a process that we call

compile-time execution.

Well-formedness of generated code is checked during compile-time execution itself, making the process easy to debug.

Here, rather than guaranteeing soundness employing (only) static checks, that would require a sophisticated type system with structural types for meta-expressions, we propose a lightweight solution, called

checked compile-time execution, where

typechecking at the conventional level is the standard one. However, metareduction steps are always perfomed on typechecked code, hence are safe. Type checking at the level of class composition operators, instead, is dynamic. The motivation is twofold: to allow a modular approach, that is, compile-time execution is dened, and can be implemented, on top of typechecking and execution of the underlying language, and to allow the programmer to handle composition errors, e.g., by relying on the Java exception mechanism. Besides soundness, our technique ensures an additional important property called

meta-level

soundness. Intuitively, typing errors found during compile-time exe-

cution never originate from library (meta-)code, that is, programs which have already been compiled. This is not granted by other approaches like C++ templates . We describe our approach by dening a calculus, called

MetaFJig,

where class

denitions are rst-class values which can be combined by four primitive operators, namely

sum, restrict, alias, and redirect. The conventional (that is, exclud-

ing meta-level features) fragment of

MetaFJig

is a subset of

FJig

[21,20], a

Java-like calculus in the spirit of Featherweight Java [17] (FJ for short), where inheritance has been generalized to the much more exible notion originally proposed in Bracha's Jigsaw framework [7]. Here, for sake of simplicity, we have omitted some

FJig

features which are not relevant for the present work.

The conventional and meta-level features of

MetaFJig

are informally presented

in Section 2.1 and Section 2.2, respectively. Section 3 contains the formal syntax, semantics and type system. Section 4 formally denes checked compile-time execution and states its properties. Finally, Section 5 outlines related and further work. A very preliminary presentation of the ideas in this paper has been given in [19,22].

2

But not other kinds of language terms: in this sense the meta-programming approach is limited.

2

An informal introduction

2.1 In

Primitive composition operators

MetaFJig,

a class declaration associates an expression of type

class name. The simplest form of such an expression is a

class

with a

class constant, which is

similar to a Java class body and contains, besides other components explained later on,

abstract

or dened member (eld or method) declarations.

The following example shows two class declarations where class constants are directly associated to class names.

A = { abstract int m2 () } B = { abstract int m1 () }

3

int m1 (); { return m1 () + 1; } int m2 (); { return 1 + m2 (); }

These two classes are abstract (hence cannot be instantiated).

Compound expressions of type class can be constructed using primitive composition operators. For instance, a concrete class can be obtained from those above by applying the sum operator as follows:

Sum = A + B This declaration is reduced to the following:

Sum = { int m1 () { return 1 + m2 (); } int m2 () { return m1 () + 1; } } Conicting denitions for the same member are not permitted, whereas

abstract

MetaFJig

provides

members with the same name are shared. Besides sum, other three primitive composition operators:

restrict, alias,

and

redirect,

which

take as arguments a class and one or two names. The restrict operator removes a denition, making the corresponding member abstract. The alias operator adds a denition for an either abstract or new member, duplicating that of an existing member. The redirect operator replaces all the internal references (in method bodies or eld initialization expressions) to an abstract member name

4

by a dierent name, and removes its declaration . For instance,

Restrict = Sum [\ m1 ] // restrict m1 in Sum Alias = A [ m1 = m2 ] // alias m2 as m1 in A Redirect = A[ m2 / m1 ] // redirect m1 into m2 in A is reduced to

3 4

To write more readable examples, we assume that the primitive type int and its operations are available. Unless it is a member of a , see later on.

supertype

Restrict = abstract int m2 () } Alias = { int m1 () int m2 () } Redirect = int m2 () }

{ int m1 (); { return m1 () + 1; } { return m1 () + 1; } { return m1 () + 1; } { { return m2 () + 1; }

These four primitive operators are a minimal, yet very expressive set. Sum,

5

restrict and alias are very similar to the trait operators dened in [10] , with the dierence that they uniformly work on elds as well, as shown below. Other trait-based languages [6,25] also include a the

redirect

rename

operator. We prefer to have

operator since it is conceptually more primitive, and it allows to

6

express many dierent forms of renaming, see the examples in Section 2.2. In

MetaFJig,

as in

FJig,

the modier

abstract

applies to elds as well, as

shown by the following example which also illustrates how constructors work.

A1 = { abstract int f1 ; int f2 ; cons ( int x ) { f2 = x ; } int m () { return f1 + f2 ; } } B1 = { int f1 ; abstract int f2 ; cons ( int x ) { f1 = x + 1;} } + A1 A class constant denes one

7 constructor which species a sequence of parame-

ters and a sequence of initialization expressions, one for each non-abstract eld. We assume a default constructor with no parameters for classes having no dened elds. In order to be composed by the sum operator, two classes should provide a constructor with the same parameter list. The eect is that the resulting class provides a constructor with the same parameter list, that executes both the original constructors.

5 6

exclude

Restrict is called in trait literature; here we prefer to stick to the original name in Jigsaw [7]. In MetaFJig we have omitted some FJig features not relevant for the present work. Notably, in Jigsaw and FJig dened members can be , or , whereas here they are all implicitly virtual. As a consequence, MetaFJig does not include the primitive operator which allows to express, e.g., member hiding. Moreover, the operator of FJig, handling maps from names into names, has been replaced by three operators which handle single names (restrict, alias and redirect). They provide the same expressive power and are more convenient for the meta-level. Since, as in FJ and dierently from Java, overloading is not allowed.

freeze reduct

7

virtual frozen local

Classes composed by sum can share the same eld, provided it is abstract in all except (at most) one. Note that this corresponds to

sharing

elds as in, e.g., [5];

however, in our framework we do not need an ad-hoc notion.

MetaFJig

keeps the Java nominal approach, that is, types are class names.

However, desired subtyping relations must be explicitly written by the program-

supertypes C1 . . . Cn

mer, by declaring a sequence of

also used to typecheck occurrences of

this

in a class constant. This is

8

inside method bodies , as illustrated

by the example below.

C = { abstract int m1 (); abstract int m2 (); } D = { { int n ;} ," String " - >{ String n ;} ,...}; class create ( String table ){ 13

To keep the example compact, we do not detail all the classes named in the example, and we simply assume that they are declared elsewhere.

TableStructure structure = DB . getTableStructure ( table ); class result ={}; for ( Row r : structure ) result = result + Rename . apply ( map . get ( r . type ) , $n ,r . name ); return result ; }

}

A class dened by

Foo = DBRecord . create ( " Foo " ); will have the shape of the table

"Foo"

in the DB. That is, the following code:

int m ( Foo x ){ return x . bar ;} will compile only if the table

3

"Foo"

has a eld

bar

of type

int.

The language

3.1

Syntax and reduction rules

In Figure 1 we give the syntax of sequences, e.g.,

d

MetaFJig.

We use the bar notation for

d . We assume innite sets of class variables x .

is a sequence of declarations

names C , (member) names n , and

A meta-program is a sequence of class declarations, where an expression is associated to a class name. A program is a meta-program where all these expressions are class constants. A class constant consists of a constructor, a sequence of (member) declarations, which can be either abstract or non abstract (member denitions), and a sequence of

supertypes.

Members can be elds or methods.

Constructor and member declarations are in the style of FJ, whereas the last component, similar to an of

this

implements

declaration in Java, means that the type

must be a subtype of (the structural type of )

C

for each class name

C

this

in

in the sequence. This information is needed to typecheck occurrences of

method bodies, see [6,21]. There is no constructor overloading, hence a class has only one constructor. However, dierently from FJ, where this unique constructor has a canonical form, there is no a priori relation among the parameter list and the constructor body which is a sequence of

eld expressions

associating

(initialization) expressions to eld names. Sequences of class declarations, declarations, eld expressions, and

this

super-

types are considered as sets, that is, order and repetitions are immaterial. Moreover, in a well-formed (meta-)program, a class name cannot be declared twice, that is, a program is a map from class names to expressions, hence we can safely use the notation

mp(C ).

Analogously, no member can be declared twice in a

class constant. This implies that, dierently from Java, there is no method overloading, and there is no overloading between eld and method names. However, for better readability, we will use the metavariable eld,

m

f

when a name is used for a

for a method. A parameter name cannot be declared twice in a construc-

tor or method header. Finally, a eld name cannot appear twice in a sequence of

mp :: = C =e

meta-program

C =c {k d C } kh{fe} cons(T x ) f =e ad | fd | md abstract fd | abstract mh ; T f; T m(T x ) mh{return e ;}

program class constant constructor constructor header eld expression declaration abstract declaration eld denition method header method denition

p c k kh fe d ad fd mh md

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

T

:: = C | name | class

type

e

:: = x | f | m(e) | e.f | e.m(e) | new C (e) | C (fe) | n | C | c | e1 + e2 | e1 [\e2 ] | e1 [e2 =e3 ] | e1 [e2 /e3 ] :: = f | m

expression (conventional constructs) expression (pre-object) expression (meta-level) (member) name

n

value eld value

v :: = C (fv ) | n | c fv :: = f =v Fig. 1. Syntax

eld expressions, hence we can safely use the notation

fe(f ), and there is exactly

a eld expression in the constructor for each non abstract eld. Types are class names and the primitive types

name of names and class of classes.

Expressions in method bodies include conventional constructs, pre-objects, and meta-expressions. Conventional constructs are similar to those of FJ. We omit cast for simplicity since it is not relevant for our technical treatment; moreover, we distinguish between object

internal

this

eld accesses and method invocations, which have the current

as implicit receiver, and

external

eld accesses and method invoca-

tions which have an explicit receiver. As explained at the end of Section 2.1, internal references are aected by composition operators. Pre-objects are runtime expressions which cannot be written in programmer's code, but are obtained by reducing a constructor invocation. Indeed, since the constructor has no canonical form, we need two dierent syntactic forms [21,20], dierently from FJ. Meta-expressions are names, class names, class constants, or are constructed by the four operators

sum, reduct, alias,

and

redirect.

The behaviour of these

operators will be described when explaining the corresponding reduction rules.

Values are objects, names and class constants. Objects are pre-objects where all eld expressions are (recursively) values. In Figure 2 we give the rules which dene the reduction of an expression the context of a program

p.

e

in

We omit standard contextual closure for brevity.

We use the following notations, whose trivial formal denitions are omitted:

 mbody p (C , m) gives parameters and body of method m in class C in p ;  e˜ is the expression obtained from e by replacing internal references (that is, internal eld accesses and method invocations) by the corresponding external versions with receiver

 names(d ), abs(d ) 

this;

def (d ) is the set of all, abstract and dened names d , respectively; names(p, C ) = names(d ) if p(C ) = {_ d _}; n∈names(d ), then mtype(n, d ) is its type (member types are dened in and

declared in if

Figure 3);

 d kd

0

means that

d

and

d

0

are

non conicting,

0

def (d )∩def (d ) = 0 n∈names(d )∩names(d ), mtype(n, d ) = that is,

∅, and coherent, that is, for all 0 mtype(n, d );  d [\n] is obtained from d by making abstract the non abstract declaration of n , if any, or removing the abstract declaration of n , if any; analogously, fe[\n] is obtained from fe by removing the eld expression for n , if any; these notations are generalized to set of names;

 d [n 0 =n] is obtained from d

by adding a denition for

and removing the abstract declaration for is obtained from

fe

n

0

n0

n, fe[n 0 =n] that for n , if

equal to that for

, if any; analogously,

by adding a eld expression for

n

equal to

any;

 d [n/n 0 ]

is obtained from

n 0 in method n ∈names(d / ). to

d

bodies by

by replacing by replacing internal references

n,

and adding an abstract declaration for

n

if

The rst three rules dene reduction of conventional constructs. There are no reduction rules for variables (parameter names) and internal eld accesses and method invocations since those appearing in a method body are

14 , see (client-invk).

replaced at invocation time Rules

(client-field)

and

(client-invk)

are as in FJ, with the dierence that,

since there is no inheritance, method look-up (modeled by method body Rule

e

is transformed in

(object-creation)

mbody ) is trivial, and

e˜.

is straightforward and reduces a constructor invo-

cation into the pre-object obtained by replacing parameters by corresponding arguments in the constructor's body. Note that only classes with no abstract members can be instantiated. The following rules dene reduction of meta-expressions, that is, expressions of type

class.

Rule

(c-name)

reduces the name of a class declared in the program into the

corresponding denition.

14

Indeed, as explained at the end of Section 2.1, the dierence between, say, f and this.f is only relevant for composition operators, notably redirect.

(client-field)

C (fv ).f −→ p v

(obj-creation)

(c-name)

fv (f )=v

(client-invk)

mbody p (C , m)=x ; e v =C (_)

p(C )={cons(_x1 . . . _xn ){fe} d _} abs(d) = ∅ x =x1 . . . xn

new C (v ) −→ p C (fe[v /x ])

C −→ p c

v .m(v ) −→ ˜[v /x ][v /this] p e

p(C )=c

d 1 kd 2 (sum)

0

{kh{fe 1 } d 1 C 1 } + {kh{fe 2 } d 2 C 2 }

(sum-error)

(restrict)

{kh 1 {_} d 1 _} + {kh 2 {_} d 2 _} −→ p error {kh{fe} d C }[\n] −→ p {kh{fe[\n]} d [\n] C }

(restrict-error)

(alias)

0 0 −→ p {kh{fe 1 fe 2 } d 1 d 2

{_ d _}[\n] −→ p error

(redirect)

{_ d _}[n =n] −→ p error 0

0

{k d C }[n/n 0 ] −→ p {k d C }

(redirect-error)

n∈def (d)

n ∈def / (d)

n∈def (d) n 0 ∈def / (d) n 0 ∈abs(d) implies mtype(n, d)=mtype(n 0 , d)

n ∈def / (d) or n 0 ∈def (d) or mtype(n, d)6=mtype(n 0 , d) n 0 ∈abs(d) n∈names(d) implies mtype(n, d)=mtype(n 0 , d) ( d[n/n 0 ][\n 0 ] if n 0 ∈names(p, / C ) for all C ∈C , 0 d = 0 d[n/n ] otherwise

{_ d C }[n/n ] −→ p error 0

0

d 2 =d 2 [\def (d 1 )]

kh 1 6=kh 2 or d 1 ∦d 2

0 0 {kh{fe} d C }[n 0 =n] −→ p {kh{fe}[n =n] d [n =n] C }

(alias-error)

C 1C 2}

d 1 =d 1 [\def (d 2 )]

n 0 ∈abs(d) / or mtype(n, d)6=mtype(n 0 , d)

Fig. 2. Reduction rules

For each composition operator there are two rules, the latter corresponding to the case when the operator cannot be performed, hence an error is raised. The sum operator merges two class constants, as shown in rule guments must have the same constructor header

(sum).

The ar-

15 , non conicting and coherent

declarations, that is, no member can be dened in both and, if declared in both, it must have the same type. Then, the result has the constructor header of the arguments, the (disjoint) union of the eld expressions, the (disjoint) union of the dened members, and the union of the declared members, which are abstract only if abstract in both arguments. Note that the side conditions ensure wellformedness of the result. If one of the side conditions does not hold, then rule

(sum-error)

is applied.

n by the corresponding abstract n is a eld, its initializiation ex-

The restrict operator replaces the denition of declaration, as shown in rule

(restrict).

pression is removed as well. If

n

If

is not dened, then rule

(restrict-error)

is

applied. The alias operator adds a denition for The name

n

0

n 0,

by duplicating that existing for

n.

can be either new or abstract, in which case the denition replaces

the previous abstract declaration, and the two must be coherent. If

n

is a eld,

then the initialization expression is duplicated as well. Note also that, if method, then recursive internal references to the body is duplicated for

n 0.

If

n

n

n

is a

in its body are not aected when

is not dened, or

declaration is not coherent with the denition of

n,

n0

is already dened, or its

then rule

(alias-error)

is

applied. The redirect operator replaces internal references to abstract member method bodies by declaration for with that of

n 0.

n

n.

If

n

is added. Otherwise, the declaration of

The abstract declaration for

by the assumption that, for all

this,

that is, all members of

C

C ∈C , C

3.2

n0

in

n

must be coherent

is removed, unless it is required

can be safely assumed as supertype for

have a (coherent) declaration in

is not abstract, or the declaration of

(redirect-error)

n0

was not a member yet, then a corresponding abstract

n

d

is not coherent with that of

as well. If

n 0,

n0

then rule

is applied.

Type system

Type environments are dened in Figure 3. A class type environment is a sequence of associations from class names to class types, assumed to be a map. A class type is a 4-tuple, consisting of the constructor type (the sequence of constructor parameter types), the class kind (abstract or non abstract), the class signature, and the supertypes (a sequence of class names). A class signature is a sequence of associations from member names to member types, assumed to be a map. A eld type is just a type, whereas a method type is a pair consisting of the sequence of parameter types and the

15

In order to make equal the constructor header of two classes, FJig [21,20] provides a operator, omitted here for simplicity.

constructor wrapper

∆ CT ck Σ MT Π

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

C :CT T ; ck ; Σ; C a | ¬a n:MT T |T →T x :T

class type environment class type class kind signature member type parameter type environment

Fig. 3. Type environments

result type. Finally, a parameter type environment is a sequence of associations from variables (parameter names) to types, assumed to be a map.

MetaFJig programs: (standard) wellstrong well-typedness. The dierence is illustrated by the following

We distinguish two notions of typing for

typedness

and

example. In the program

D = { int m () { return 0; } } C = { int m () { return new D (). n ();} } the class constant used as denition of

C

is ill-typed, hence the whole program is

ill-typed. However, a similar program where the ill-typed class constant is only used as meta-expression, as the following:

D = { int m () { return 0; } } C = { class m () { return { int m () { return new D (). n ();} } } } is considered well-typed, but not strongly well-typed. We denote the two typing judgments by

0

`

and

?

`,

respectively, to suggest that class constants must denote

well-typed classes in the former case only when used as class denitions (that is, at level

0), in the latter case at anny inner meta-level. Well-typedness is enough to

guarantee (standard) soundness, see Theorem 1. Strong well-typedness is needed to guarantee

meta-level soundness,

an additional important property discussed

later on, see Theorem 7. Formally, the only dierence in the denition of the two judgments is in the rule for typing class constants, whose two versions are given in Figure 4. In order to be a well-typed class meta-expression, the only condition a class constant must satisfy is that class names appearing as

this

supertypes actu-

(class-constant-t0 )

0

∆; _; _; _` {_ _ C }:class

C ⊆dom(∆)

?

(class-constant-t? )

∆`c:CT ?

∆; _; _; _`c:class

Fig. 4. The two typing rules for class constants

(class-constant-t0 ). This condition is necessary perform the check required in rule (redirect), otherwise reduction could stuck. Instead, rule (class-constant-t?) states that a class constant is a

ally exist, as shown in rule to go

strongly well-typed meta-expression if it is well-typed as class.

`

The other rules are given in Figure 5 and Figure 7, where by

0

`

and

?

`,

must be replaced

respectively. We use the following notations:

 Σ is the signature extracted from d , that is, Σ d (n) = mtype(n, d );  CT c is the class type extracted from c , that is, CT c = T1 . . . Tn ; ck ; Σ d ; C d

if

c = {cons(T1 x1 . . . Tn xn ){_} d C },

with

ck = a

if

abs(d )6=∅, ck = ¬a

otherwise;

 ∆p

is the class type environment extacted from

p,

that is,

∆p (C ) = CT c

if

p(C ) = c ;  if ∆(C ) = T ; ck ; Σ; C , then ktype(∆, C ) = T , sig(∆, C ) = Σ , kind (∆, C ) = ck ;  mtype(∆, C , n) = sig(∆, C )(n). ∆ ` p , meaning that program p is ∆, modeling external libraries, and

Rules in Figure 5 dene the typing judgment well-typed w.r.t. the class type environment

the typing judgments for classes, method denitions and constructors. The rules are straightforward. Note the side-condition in rule

(class-t) checking

that the signature of the class is actually a subtype of the signature of all

this

supertypes. The (standard) denitions of the nominal subtyping relation

∆ `

T ≤T 0

and of the structural subtyping relation

∆ ` Σ≤Σ 0

are given in Figure 6.

Also note, comparing the form of typing judgment for expressions explained below with the premis of rule

(cons-t)

neither contain internal references (Σ

that, as expected, eld expressions can

= ∅),

expression

e

has type

T

this (C = ∅). ∆; Σ; Π; C ` e:T , meaning that environment ∆, needed to type-

nor

Rules in Figure 7 dene the typing judgment w.r.t. the class type

check client eld accesses and method invocations, and constructor invocations, the signature

Σ,

needed to typecheck internal eld accesses and method invo-

cations, the parameter type environment the sequence of class names

C,

Π,

needed to typecheck variables, and

needed to typecheck

this

occurrences.

The rules are straightforward. The type system is sound, as formally stated by the following standard theorem.

? 0 Theorem 1 (Soundness). If ∅`0 p , ∆p ; ∅; ∅; ∅`0 e:T , and e −→ p e , then either 0 0 0 00 00 e is a value, or e is error, or e −→ p e for some e .

(program-t)

(class-t)

∆; Σ d ; C ` md ∆; Σ fd ` k ∆ ` {k d C }

(method-t)

(cons-t)

∆∆p ` ci ∀i∈1..n ∆ ` C1 =c1 . . . Cn =cn

d = ad fd md ∆ ` Σ d ≤sig(∆, C ) ∀C ∈C

∆; Σ; x1 :T1 . . . xn :Tn ; C ` e:T 0 ∆; Σ; C ` T m(T1 x1 . . . Tn xn ){return e ;}

∆ ` T 0 ≤T

∆; ∅; x1 :T1 . . . xn :Tn ; ∅ ` ei :Ti0 ∀i∈1..k ∆; Σ ` cons(T1 x1 . . . Tn xn ){f1 = e1 . . . fk = ek }

∆ ` Ti0 ≤Σ(fi ) ∀i∈1..k

Fig. 5. Typing rules for programs and classes

(≤-sig)

∆ ` MT i ≤MT 0i ∀i ∈ 1..h ∆ ` n1 :MT 1 . . . nk :MT k ≤n1 :MT 01 . . . nh :MT 0h

1≤h≤k

0

(≤-method type)

(≤-direct)

∆ ` T ≤T 0 ∆ ` T ≤T 0

∆ ` T → T ≤T → T 0

∆ ` C ≤C 0

∆(C ) = _; _; _; C C 0 ∈C

(≤-refl)

(≤-trans)

Fig. 6. Subtyping

∆ ` T ≤T ∆ ` C ≤C 0 ∆ ` C 0 ≤C 00 ∆ ` C ≤C 00

(var-t)

_; _; Π; _

(int-field-t)

_; Σ; _; _

(client-field-t)

(client-invk-t)

` f :T

∆; Σ; Π; C ` e:C ∆; Σ; Π; C ` e.f :T

_; _; _; C

(int-invk-t)

Σ(f ) = T

∆; Σ; Π; C ` e:C ∆; Σ; Π; C ` e:T

(class-name-t)

∆; Σ; Π; C ` e1 :class ∆; Σ; Π; C ` e2 :class ∆; Σ; Π; C ` e1 + e2 :class

(error-t)

∆; Σ; Π; C ` m(e):T

mtype(∆, C , fi ) = Ti0 ∆ ` Ti ≤Ti0 ∀i∈1..n

∆; _; _; _ ` C :class

(restrict-t)

∆; Σ; Π; C ` e1 :class ∆; Σ; Π; C ` e2 :name ∆; Σ; Π; C ` e3 :name ∆; Σ; Π; C ` e1 [e2 =e3 ]:class

C ∈names(∆)

∆; Σ; Π; C ` e1 :class ∆; Σ; Π; C ` e2 :name ∆; Σ; Π; C ` e1 [\e2 ]:class

(collapse-t)

∆; Σ; Π; C ` e1 :class ∆; Σ; Π; C ` e2 :name ∆; Σ; Π; C ` e3 :name ∆; Σ; Π; C ` e1 [e2 /e3 ]:class

∆; Σ; Π; C ` error:T Fig. 7. Typing rules for expressions

0

Σ(m) = T → T 0 ∆ ` T ≤T

kind(∆, C ) = ¬a 0 ktype(∆, C ) = T 0 ∆ ` T ≤T

∆; Σ; Π; C ` C (f1 =e1 . . . fn =en ):C

(alias-t)

∆; Σ; Π; C ` e:T

mtype(∆, C , m) = T → T 0 ∆ ` T ≤T

∆; Σ; Π; C ` ei :Ti ∀i∈1..n

` n:name

C ∈C

0

∆; Σ; Π; C ` e.m(e):T

_; _; _; _

` this:C

mtype(∆, C , f ) = T

∆; Σ; Π; C ` new C (e):C

(name-t)

(sum-t)

(this-t)

Π(x ) = T

∆; Σ; Π; C ` e:T

(new-t)

(obj-t)

` x :T

As usual, soundness can be derived from progress and subject reduction properties.

Theorem 2 (Progress). If ∅`0 p and ∆p ; ∅; ∅; ∅`0 e:T , then either e is a value, 0 0 or e is error, or e −→ p e for some e . 0 Theorem 3 (Subject reduction). If ∅`0 p , ∆p ; ∅; ∅; ∅`0 e:T , and e −→ p e , then 0 ∆p ; ∅; ∅; ∅` e 0 :T 0 for some T 0 s.t. ∆p ` T 0 ≤T . The proofs are a simplied version of those for FJ. Indeed,

MetaFJig

programs

can be roughly seen as FJ programs with no inheritance and two primitive types.

4

Checked compile-time execution

We consider now

meta-programs,

that is, sequences of class declarations where

arbitrary expressions, rather than class constants, are associated to class names.

compiletime execution, formally modeled by the relation mp −→ mp 0 dened in Figure 8.

A meta-program can be reduced to a program by a process that we call As modeled by

(meta-red),

the right-hand-side of a class declaration can be

reduced in the context of the program part of the current meta-program.

(meta-red)

0 e −→ p e p C =e mp −→ p C =e 0 mp

Fig. 8. Compile-time execution

However, soundness of compile-time execution is not guaranteed, that is, reduction could get stuck, or produce as right-hand-side of a class declaration a value dierent from a class constant, or a class constant denoting an ill-typed class. To prevent these error situations, dierent approaches are possible. In this paper, rather than guaranteeing soundness by (only) static checks, what would require a sophisticated type system with structural types, we propose a simple solution, called

checked compile-time execution, which integrates meta-reduction

with typechecking steps. If typechecking fails, then the program reduces to

errorT.

16 on top

The advantage is that the technique can be modularly dened

of an arbitrary Java-like language. More in detail, during checked compile-time execution each class declaration

C =e

in the meta-program passes throughout the following states:

1. initial state, no check has been performed yet; 2. we have checked that

e

is a well-typed expression of type

be safely reduced, until getting a class costant

16

And implemented, as explained in Section 5.

c;

class; hence, e

can

c

3. we have checked that

denotes a well-typed class.

Checked compile-time execution is formally dened on triples

p , mp

and

mp

0

where

are the class declarations in state (3), (2), and (1), respectively,

hence the initial state for meta-program triples are

p; mp; mp 0

closed,

mp

is

∅; ∅; mp .

We assume that such

that is, only class names which are declared can appear in

expressions. We will use

mp f

to denote either such a triple or

clientship −→p

In the rules we use the

and

error

dependency =⇒p;mp

or

errorT.

relations dened

in Figure 9.

?

c →C 0 C −→p C 0

(client-direct)

(client-trans)

(client-refl)

p(C )=c

C −→p C

C −→p C 0 C 0 −→p C 00 C 0 −→p C 00 0

(depend-direct)

(depend-trans)

e →C 0 C 0 −→p C 00 C =⇒p;mp C 00

mp(C )=e C 00 ∈dom(mp)

C =⇒p;mp C 0 C 0 =⇒p;mp C 00 C =⇒p;mp C 00

Fig. 9. Clientship and dependency relations

Here,

0

e →C

means that (a subexpression of )

0 suggests that occurrences of C account. For instance, if e is

superscript into

e

C

is of form

or

in class constants in

new C (_).

e

The

are not taken

new C (). m ({ D n () { return new D () } }) then

0

e →C

holds, but not

On the other hand,

?

c →C

0

e →D. means that

C

(transitively) uses

C0

c. C 0 if C 0 that C can

occurs in (an inner class constant in)

Clientship is analogous to the same notion in Java. That is,

C

is client of

either as type or as instance generator. Note

occur at any inner level in the class constant dening

C.

Moreover, we assume

that any class is client of itself for technical convenience. In order to determine whether a program be in

p

p

is strongly well-typed, all classes

p

is client of either must

itself or already typechecked. In Java, this relation is indeed used when

the compiler is invoked to determine the full set of classes to be compiled or present in bytecode form. Dependency, instead, is a novel notion, dened on class names in a meta-program. Class

C

may depend on some other class only if its dening expression

constant, that is, needs to be (typecheked and) reduced. In this case,

C

e

is non

depends

on all the classes which must be already reduced and typechecked in order to determine whether

e

is well-typed and of type

class.

Moreover, we use the following abbreviations:

0  closed (p, e)={C 0 |e →C , C −→p C 0 }⊆dom(p), hence we can determine whether

e is a well-typed expression of type class w.r.t ∆p ;  closed (p, p 0 ) if, for all C ∈dom(p 0 ), {C 0 |C −→p 0 C 0 }⊆dom(p p 0 ), hence we can 0 p determine whether or not p is a strongly well-typed program w.r.t ∆ . or not

Rules dening checked compile-time execution are given in Figure 10.

(meta-check)

0

p; mp; C =e mp 0 −→ p; mp C =e; mp 0

(meta-check-error)

(meta-red)

mp(C ) = e 0 closed(p, e) and ∆p ; ∅; ∅; ∅ 6 `e:class or =⇒p 0 ;mp cyclic

0 e −→ p e 0 p; C =e mp; mp −→ p; C =e 0 mp; mp 0

(meta-red-error)

(check)

p; p 0 ; mp −→ errorT

∆p ; ∅; ∅; ∅`e:class

e −→ p error p; C =e mp; mp 0 −→ error ?

p; p 0 mp; mp 0 −→ p p 0 ; mp; mp 0

(check-error)

∆p `p 0

?

p; p 0 mp; mp 0 −→ errorT

closed(p, p 0 ) and ∆p 6 `p 0

Fig. 10. Checked compile-time execution

Each pair of rules models a normal reduction step and the corresponding abnormal termination. In rule

e

(meta-check),

is of type

class

class declaration

(meta-check-error),

C =e and

C =e

passes from state (1) to (2), since

w.r.t. the already typechecked program portion

p.

in state (1) for which we have all the information needed to typecheck

e

e,

is ill-typed, or we detect a cyclic dependency among classes in state (1),

hence there is no hope to be able to typecheck all of them in the future. In rule

(meta-red), C =e

checked program portion

17

makes a meta-reduction step w.r.t. the already type-

p . In rule (meta-red-error), the meta-reduction step

raises a composition error.

17

In rule

a type error is raised in two cases: either there exists

For example C = new C().m();.

In rule

(check),

a program portion

p0

passes from state (2) to (3), since it is

well-typed w.r.t. the already typechecked program portion

error), p 0

p.

In rule

(check-

raises a typechecking error, since we have all the needed information

to typecheck it, and it is ill-typed. We show now some examples illustrating how checked compile-time execution works. First we give an example of successful reduction. We abbreviate by constant

{ int one(){ return 1; } }.

c

the class

The program

∅;∅; C = { class m () { return c ; } } D = { int m () { return new E (). one ();} } E = new C (). m () reduces by two applications of

(meta-check)

to

∅; C = { class m () { return c ; } } D = { int m () { return new E (). one ();} }; E = new C (). m () reduces by

(check)

to

C = { class m () { return c ; } } ; D = { int m () { return new E (). one ();} } ; E = new C (). m () reduces by

(meta-check)

to

C = { class m () { return c ; } } ; D = { int m () { return new E (). one ();} } E = new C (). m (); ∅ reduces by

(meta-red)

to

C = { class m () { return c ; } } ; D = { int m () { return new E (). one ();} } E = { int one () { return 1; } }; ∅ reduces by

(check)

to

C = { class m () { return c ; } } D = { int m () { return new E (). one ();} } E = { int one () { return 1; } } ; ∅;∅; Note that, after checking class depends on class

new C().m()

E

C,

it is not possible to check class

D,

since it

whose denition is not a class costant yet. Hence, expression

is checked to be of type

class.

At this point, reduction of this

expression can take place, and nally the resulting class constant is checked to be well-typed, together with class

D.

The second example shows a case when checked compile-time execution terminates with an

errorT.

∅ ; ∅ ; C = {} D = new C (). k () reduces by

(meta-check)

to

∅ ; C = {}; D = new C (). k () reduces by

(check)

to

C = { }; ∅ ; D = new C (). k () (meta-check-error) to errorT. C is checked, and then expression new C().k() is checked to be of type class. This is not the case, since class C has no method named k. Since new C().k() is closed w.r.t. class C an errorT is raised.

reduces by Class

In the last example we abbreviate by

c0

the class constant

{ int two(){ return new D().one(); } }.

The program

∅; ∅; C = { class m ( class x ) { return x + c ; } } D = new C (). m ( c 0 ) reduces by

(meta-check)

to

∅; C = { class m ( class x) { return x + c ; } }; D = new C (). m ( c 0 ) reduces by

(check)

to

C = { class m ( class x) { return x + c ; } }; ∅; D = new C (). m ( c 0 ) reduces by

(meta-check)

to

C = { class m ( class x ) { return x + c ; } }; D = new C (). m ( c 0 ); ∅ reduces by

(meta-red)

to

C = { class m ( class x ) { return x + c ; } }; D = c0 +c ; ∅ reduces by

(meta-red)

to

C = { class m ( class x ) { return x + c ; } }; D = { int two (){ return new D (). one (); } int one (){ return 1;} }; ∅ reduces by

(check)

to

C = { class m ( class x ) { return x + c ; } } D = { int two (){ return new D (). one (); } int one (){ return 1;} }; ∅;∅

Class

class,

C

new C().m(c 0 ) is checked resulting class D is checked.

is checked, then the expression

and then reduced. Finally, the

to be of type

This example also illustrates why only (standard) typechecking is used in

check).

new D().one() associated to D.

Indeed, the fact that the expression

only be detected when the result of

c0 + c

is

We can state two signicant properties for

MetaFJig

(meta-

is well-typed can

checked compile-time

execution. Theorem 4 states that checked-compile time execution never goes stuck. Theorem 7 states that well-typed meta-code never produces ill-typed code. Whereas the former property is shared with [19,22], the latter is new, and very important, since it allows the programmer to safely use compiled libraries. This is not granted by other approaches like C++ templates . For example in C++ a template instantiation can raise type errors caused by the code of the template itself.

value

We say that

mp f

mp f = p; ∅; ∅.

Moreover,

and analogously

is a

if all class declarations are in state (3), formally

0

∆` mp:class

?

abbreviates

∆`mp:class.

0

∆` e:class

for all _=e in

mp ,

? Theorem 4 (Soundness of checked compile-time execution). If ∅; ∅; mp −→ 0 mp f , then either mp f is a value or mp f = error or mp f = errorT or mp f −→ mp f 0 for some mp f . Soundness of checked compile-time execution can be proved, as usual, as a consequence of progress and subject reduction properties, where in the latter the invariant which is preserved by reduction is that, in in

p

and

mp

p; mp; mp 0 , class declarations

are in state (3) and (2), respectively, where only well-typedness (not

strong well-typedness) is required. Formally, we dene or

mp f = errorT,

or

mp f =

0

0

` mp f

if either

mp f = error,

0 p; mp; mp 0 and ∅` p , ∆p ` mp:class. The judgment

trivially holds in an initial state

∅; ∅; mp .

Theorem 5 (Progress of checked compile-time execution). If `0 mp f , then 0 either mp f is a value or mp f = error or mp f = errorT or mp f −→ mp f for some 0 mp f . Proof. If mp f is neither a value, nor error, p; mp 0 ; mp where mp 0 mp 6= ∅. By cases:



Assume rst that there exists implies



by either

mp f

(check)

mp f

or

into

C

if

e not a 0 e −→ p e ,

(meta-red-error).

value. Since hence

mp f

0

` mp f

reduces

p; p 0 ; mp with p 0 mp 6= ∅. Assume mp = ∅. Then, closed (p, p 0 ) clearly holds, hence mp f reduces by either

(check-error).

Otherwise, consider the graph with nodes

direct).

with

then it has the form

has the form

is closed, or

C =e ∈ mp 0

errorT,

by Theorem 1 we have that

(meta-red)

Otherwise, since



0

∆p ` e:class,

nor

C =⇒p 0 ;mp C

0

dom(mp)

and an edge from

(depend(meta-check-error).

is a direct dependence, that is, holds by

If the graph is cyclic, then

mp f

reduces by

C0





C with no entrant edges. That is, there exists 0 C =e∈mp s.t. the set C≡{C 00 |e →C 0 , C 0 −→p 0 C 00 } is a subset of dom(p p 0 ). Assume C ⊆ dom(p). Then, closed (p, e) holds, hence mp f reduces by either Otherwise, there exists a node

(meta-check)

or

p 00

Otherwise, let

(meta-check-error).

p0

be the maximal subset of

s.t.

dom(p 00 ) ⊆ C .

Clearly

00

closed (p, p ) holds, hence mp f reduces by either (check) or (check-error).

Lemma 1. If ∅`0 p and ∆p `0 p 0 , then ∅`0 p p 0 . Proof.

Easy check.

Theorem 6 (Subject reduction of checked compile-time execution). If 0 0 0 0 ` mp f and mp f −→ mp f then ` mp f . Proof.

   

By cases on the applied rule:

If the applied rule is

(meta-check),

then the thesis follows from the side

condition of the rule. If the applied rule is

(check),

then the thesis follows from the side condition

of the rule by Lemma 1. If the applied rule is

error),

(meta-check-error), (meta-red-error) or (check-

then the thesis trivially holds.

If the applied rule is

(meta-red),

then, since

0

∆p ` e:class

holds, the thesis

follows from Theorem 3.

Theorem 7 (Meta-level soundness). If ∅`? p and ∆p `? mp:class, then ? p; mp; ∅6−→errorT. Meta-level soundness can also be proved by progress and subject reduction properties, with an invariant analogous to that used above. However, here we require

strong

well-typedness. Formally, we dene

mp f = p; mp; ∅

and

?

p ?

∅`p , ∆ `mp:class.

?

`mp f

if either

mp f = error

or

f , then either mp f is a value or Theorem 8 (Meta-level progress). If `? mp 0 0 mp f = error or mp f −→ mp f for some mp f .

Proof.

errorT

Since

?

`mp f

or the thesis holds.

0

` mp f , by Theorem 5 we know that either mp f = ? However, mp f = errorT cannot hold since `mp f.

clearly implies

In order to prove meta-level subject reduction, we need a dierent version, referring to strong well-typedness rather than well-typedness, of the subject reduction property stated in Theorem 3. This property is stated in Theorem 9, and its

proof is based on the following lemmas. In particular, Lemma 4 states that

by (successfully) applying a composition operator to strongly well-typed classes we always get a strongly well-typed class.

Lemma 2 (Weakening). If ∆; Σ; C `? md then ∆, _; Σ, _; C , _`? md . Lemma 3 (Substitution). If ∆; Σ; C `? md then ∆; Σ[n 0 /n]; C `? md [n 0 /n].

Lemma 4. If ∅`? p , ∆`? c1 :CT 1 , and ∆`? c2 :CT 2 , then 1. 2. 3. 4.

c1 + c2 −→ p c implies ∆`c:CT , ? c1 [\n] −→ p c implies ∆`c:CT , ? c1 [n1 /n2 ] −→ p c implies ∆`c:CT , ? c1 [n1 =n2 ] −→ p c implies ∆`c:CT . ?

Proof. {k1 d 1 C 1 } + {k2 d 2 C 2 } −→ p {k d C } with d i = ad i fd i md i . ? ? (class-t), we know that ∆; Σ fd `k1 and ∆; Σ d 1 ; C 1 `md 1 , and analogously for k2 and md 2 . Moreover, since we have applied (sum), d 1 kd 2 holds, hence Σ d 1 Σ d 2 is well-formed, and, by Lemma 2, ? ∆; Σ d 1 Σ d 2 ; C 1 C 2 `md 1 md 2 holds. Premises for (cons-t) on k are the union of the premises for (cons-t) on k1 and k2 . The last side condition of (sum) of the result is the union of the last side conditions of (sum) of the subcomponents. This implies that {k d C } is

1. We have that

Since we have applied

well-typed by

(class-t)

{k1 d 1 C 1 }[\n] −→ {k d C } with d 1 = ad 1 fd 1 md 1 . Since p ? fd ? d we have applied (class-t), we know that ∆; Σ `k1 and ∆; Σ 1 ; C 1 `md 1 . Moreover by (restrict), d is obtained from d 1 by removing a member d d denition, hence Σ = Σ 1 . Then, {k d C } is well-typed by (class-t). We have that {k d 1 C 1 }[n1 /n2 ] −→ p {k d C } with d 1 = ad 1 fd 1 md 1 . Since ? fd ? d we have applied (class-t), we know that ∆; Σ `k1 and ∆; Σ 1 ; C 1 `md 1 .

2. We have that

3.

Method bodies preserve their types by Lemma 3, the redirect operator re-

n1 only if not needed to satisfy the last {k d C } is well-typed by (class-t). We have {k1 d 1 C 1 }[n1 =n2 ] −→ p {k d C } with d 1 = ad 1 fd 1 md 1 . ? fd ? d Since we have applied (class-t), we know that ∆; Σ `k1 and ∆; Σ 1 ; C 1 `md 1 . Moreover, d is obtained from d 1 by adding one member denition. By side d condition of rule (alias), Σ 1 n1 :mtype(n1 , md 1 ) is well-formed, and by ? d Lemma 2 ∆; Σ 1 n1 :mtype(n1 , md 1 ); C 1 `md . The new method/expression n2 is also well-typed since its body is the same of n1 , hence we can conclude that {k d C } is well-typed by (class-t). moves the abstract declaration for side condition of

4.

(class-t),

hence

Theorem 9 (Strong subject reduction). If ∅`? p , ∆p ; ∅; ∅; ∅`? e:T , and e −→ p ? e 0 , then ∆p ; ∅; ∅; ∅`e 0 :T 0 for some T 0 s.t. ∆p ` T 0 ≤T . The proof is analogous to that for Theorem 3, by using Lemma 4.

Lemma 5. 1. If ∅`p and ∆p `p 0 , then ∅`p p 0 . ? ? 2. If ∆p `p 0 :class, then ∆p `p 0 . ?

Proof.

?

?

1. Easy check. 2. Since, for all

∗

?

C =c ∈ p 0 , ∆p `c:class

has been deduced by rule

(class-

constant-t ). 0 Theorem 10 (Meta-level subject reduction). If `? mp f and mp f −→ mp f then ? 0 f . `mp

Proof.

By cases depending on the applied rule:



(meta-check) and (meta-check-error) cannot be applied since `p; mp; mp 0



If the applied rule is

  

?

implies

mp = ∅. (meta-red),

then, since

?

∆p `e:class

holds, the thesis

follows from Theorem 9.

(meta-red-error), then the thesis (check), then the thesis follows from

If the applied rule is

trivially holds.

If the applied rule is

the side condition

of the rule by Lemma 5-(1).

(check-error) implies

5

0

p ? 0

cannot be applied by Lemma 5-(2), since

?

`p; p 0 mp; mp 0

∆ `p :class.

Conclusion

Metaprogramming approaches can be classied by two properties: whether the meta-language coincides with the conventional language (the so-called

circular

meta-

approach), and whether the code generation happens during compila-

tion. MetaML [28], Prolog [27] and OpenJava [29] are meta-circular languages, while C++ [18], D [9], Meta-trait-Java [25] and MorphJ [16] use a specialized

18 Almost any dynamically typed language allows some sort of

meta-language.

meta-circular facility, typically by oering an

eval

function. Such a function al-

lows to run arbitrary code, represented by an input string. Regarding code generation, MetaML and Prolog performs the computation at run time, while C++, D, Meta-trait-Java, MorphJ and OpenJava use compile-time execution. Again, dynamically typed languages providing an

eval

function allow runtime meta-

programming. The work presented in this paper lies in the area of meta-circular compile-time execution. Among the above mentioned approaches, [29] is the one showing more similarities with ours. OpenJava oers the ability to dene new language constructs, on top of Java, using meta-circular compile-time execution. Programmers can dene new constructs by writing

meta-classes, that is, partic-

ular Java classes which instruct the OpenJava compiler on how to perform the type-driven translation. These meta-classes use the reection-based

ject Protocol (MOP)

Meta Ob-

to manipulate the source code and provide its translation.

However, their approach is denitely lower level than ours and we have a very dierent long-term goal: that is, to bring compile-time execution in the realm of an already familiar programming language, rather than to allow programmers to dene their own extensions of an existing language.

18

The latest version of D seems to include a limited form of metacircular compilation.

An important activity we plan is the development of a prototype built on top of Java compilation and execution, hence making eective the modularity of our approach. More precisely:

 

Typechecking steps in checked compile-time execution will be implemented by invocations of the standard Java compiler. Meta-reduction steps in checked compile-time execution will be implemented by invocations of the Java Virtual Machine. Optimization techniques could be investigated to avoid spawning a new JVM each time.

This will imply the extension of the conventional fragment of

MetaFJig

to a

more signicant Java subset, and the denition of a deterministic strategy for checked compile-time execution. On the more foundational side, we plan to investigate an extension of our framework. In the current model, typechecking steps during checked compile-time execution always require code to be

closed, that is, type information on all class

names appearing in code must be available. Hence, typing errors can be detected only at this time. We plan to dene a constraint-based type system, as in [2], where code can be typechecked separately, that is, even in absence of some used class, allowing earlier error detection.

References

1. Jonathan Aldrich, Craig Chambers, and David Notkin. Architectural reasoning in ArchJava. In Boris Magnusson, editor, , number 2374 in Lecture Notes in Computer Science, pages 334367. Springer, 2002. 2. Davide Ancona, Ferruccio Damiani, Sophia Drossopoulou, and Elena Zucca. Polymorphic bytecode: Compositional compilation for Java-like languages. In . ACM Press, January 2005. 3. Davide Ancona, Giovanni Lagorio, and Elena Zucca. Jamdesigning a Java extension with mixins. , 25(5):641712, September 2003. 4. Davide Ancona, Giovanni Lagorio, and Elena Zucca. Flexible type-safe linking of components for Java-like languages. In , volume 4228 of , pages 136154. Springer, 2006. 5. Alexandre Bergel, Stéphane Ducasse, Oscar Nierstrasz, and Roel Wuyts. Stateful traits and their formalization. , 34(2-3):83108, 2008. 6. Viviana Bono, Ferruccio Damiani, and Elena Giachino. On traits and types in a Java-like setting. In . Springer, 2008. 7. Gilad Bracha. . PhD thesis, Department of Comp. Sci., Univ. of Utah, 1992. 8. Krzysztof Czarnecki, Ulrich Eisenecker, Robert Gluck, David Vandevoorde, and Todd Veldhuizen. , pages 2539. Number 1766 in Lecture Notes in Computer Science. Springer, 2000. 9. Digital Mars. D programming language, 2007. http://www.digitalmars.com/.

ECOOP'02 - Object-Oriented Programming

ACM Symp. on Principles of Programming Languages 2005 ACM Transactions on Programming Languages and Systems Conference

JMLC'06 - Joint Modular Languages Lecture Notes in Computer Science

Comput. Lang. Syst. Struct. TCS'08 - IFIP Int. Conf. on Theoretical Computer Science The Programming Language JIGSAW: Mixins, Modularity and Multiple Inheritance Generative programming and active libraries (extended abstract)

10. Stéphane Ducasse, Oscar Nierstrasz, Nathanael Schärli, Roel Wuyts, and Andrew Black. Traits: A mechanism for ne-grained reuse. , 28(2):331388, 2006. 11. Erik Ernst. Family polymorphism. In J.L. Knudsen, editor, , number 2072 in Lecture Notes in Computer Science, pages 303326. Springer, 2001. 12. Erik Ernst. Higher-order hierarchies. In L. Cardelli, editor, , number 2743 in Lecture Notes in Computer Science, pages 303328. Springer, 2003. 13. Robert Bruce Findler and Matthew Flatt. Modular object-oriented programming with units and mixins. In , 1998. 14. Kathleen Fisher and John Reppy. A typed calculus of traits. In , 2004. 15. Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen. Classes and mixins. In , pages 171183. ACM Press, 1998. 16. Shan Shan Huang, David Zook, and Yannis Smaragdakis. Morphing: Safely shaping a class in the image of others. In , pages 399424. Springer, August 2007. 17. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In , pages 132146, November 1999. 18. International Organization for Standardization. . International Organization for Standardization, 2003. 19. Giovanni Lagorio, Marco Servetto, and Elena Zucca. Customizable composition operators for Java-like classes (extended abstract). In , 2009. 20. Giovanni Lagorio, Marco Servetto, and Elena Zucca. Featherweight Jigsaw - a minimal core calculus for modular composition of classes. In Sophia Drossopoulou, editor, , number 5653 in Lecture Notes in Computer Science. Springer, 2009. 21. Giovanni Lagorio, Marco Servetto, and Elena Zucca. Flattening versus direct semantics for Featherweight Jigsaw. In , 2009. 22. Giovanni Lagorio, Marco Servetto, and Elena Zucca. A lightweight approach to customizable composition operators for Java-like classes. , 2009. FACS'09 - International Workshop on Formal Aspects of Component Software. To appear. 23. Luigi Liquori and Arnaud Spiwack. FeatherTrait: A modest extension of Featherweight Java. , 30(2), 2008. 24. Sean McDirmid, Matthew Flatt, and Wilson C. Hsieh. Jiazzi: New age components for old fashioned Java. In . ACM Press, 2001. SIGPLAN Notices. 25. John Reppy and Aaron Turon. Metaprogramming with traits. In Erik Ernst, editor, , number 4609 in Lecture Notes in Computer Science, pages 373398. Springer, 2007.

gramming Languages and Systems Conference on Object-Oriented Programming

ACM Transactions on ProECOOP'01 - European

Oriented Programming

ECOOP'03 - Object-

Intl. Conf. on Functional Programming 1998 FOOL'04 - Intl. Workshop on Foundations of Object Oriented Languages ACM Symp. on Principles of Programming Languages 1998 ECOOP'07 - Object-Oriented Programming

ACM Symp. on Object-Oriented Programming: Systems, Languages and Applications 1999 ISO/IEC 14882:2003: Programming languages  C++ ICTCS'09 - Italian Conf. on Theoretical Computer Science ECOOP 2009 - Object-Oriented Programming

of Object Oriented Languages

FOOL'09 - Intl. Workshop on Foundations

oretical Computer Science

Electronic Notes in The-

ACM Transactions on Programming Languages and Systems

ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2001) ECOOP'07 - Object-Oriented Programming

26. Nathanael Schärli, Stéphane Ducasse, Oscar Nierstrasz, and Andrew P. Black. Traits: Composable units of behaviour. In , volume 2743 of , pages 248274. Springer, 2003. 27. Leon Shapiro and Ehud Y. Sterling. . The MIT Press, April 1994. 28. Walid Taha and Tim Sheard. MetaML and multi-stage programming with explicit annotations. , 248(1-2):211242, 2000. 29. Michiaki Tatsubori, Shigeru Chiba, Marc-Olivier Kilijian, and Kozo Itano. OpenJava: A class-based macro system for Java. In Walter Cazzola, Robert J. Stroud, and Francesco Tisato, editors, , Lecture Notes in Computer Science, pages 117133. Springer, 2000.

ming

Techniques

ECOOP'03 - Object-Oriented ProgramLecture Notes in Computer Science The Art of PROLOG: Advanced Programming

Theoretical Computer Science

Reection and Software Engineering