Constructing Type-Safe Operators for Software Composition^{⋆}

Axel Rauschmayer, Andreas Abel, Alexander Knapp, Martin Wirsing

Institut für Informatik Ludwig-Maximilians-Universität München

         {rauschma,abel,knapp,wirsing}@informatik.uni-muenchen.de

Abstract. Grey-box software composition appears in many areas of software engineering: Mixin layers, aspects and traits are just a few examples and even regular inheritance can be viewed as composition. Operators used for these kinds of composition share two deficiencies: (1) They are monolithic and are thus paradoxically supporting reuse without being implemented in a reusable fashion. (2) There is usually no type system that allows us to check if a composition is legal before performing it. In this publication, we introduce Graft, a small language that aims to “decompose composition” by providing atomic commands for software manipulation that can be combined to express powerful composition operators. Applicability of atomic and composite commands is checked for by a type system. We demonstrate and motivate Graft’s use by looking at mixin layer composition which is fully expressible in Graft.

1 Introduction

Software composition is one of the central mechanisms used in software engineering to enable reuse and structuring in a complex system. Large-scale software composition mainly uses a black box approach, whereas smaller-scale composition usually favors grey boxes as atomic components. With all the hype surrounding large-scale, black-box components such as Enterprise JavaBeans or .NET components, one would think that nobody uses grey-box composition any more. But that is not true: It is the underlying principle of many lower-level reuse infrastructures. Examples are mixin layers [Smaragdakis and Batory, 1998] (which we’ll take a look at in a moment), aspects [Kiczales et al., 2001] and traits [Schärli et al., 2003]. Even regular inheritance can be viewed as grey-box composition. Each of these reuse infrastructures comes with its own set of operators for performing composition. This is where we get to a paradox: Even though these operators enable software composition, they are not, themselves, implemented in a reusable fashion. This would make a lot of sense, though, because most of these operators are very similar and adhere to certain basic principles. Additionally, there is often a need for many variations in performing composition even

⋆ Supported by Deutsche Forschungsgemeinschaft (DFG) project WI 841/6-1 “InOp-Sys”

within the same environment. Being able to express these generically would be very helpful.

Our approach is to “decompose composition”: We want to find out if composition is really a monolithic operator or rather a composite of more basic operators. If the latter is true and we want to prove that a certain property holds for any (legal) composition operator, we only need to prove the property for the atomic operators and for the operator combination mechanism. In Sect. 2, we present one possible set of atomic manipulation operators, a language we call Graft. We also show how Graft can be used to express mixin layer composition. In Sect. 3, we introduce a type system that checks for applicability of any combination of operators and whether such combinations are legal. This allows us to generically express and type grey-box software composition. Sect. 4 gives a more formal explanation of Graft’s type system. The last two sections, 5 and 6, present related work and the conclusions of this document. Consult App. A for a formal specification of the Graft language.

2 Finding Operators for Mixin Layer Composition

To find out more about the issues involved in software composition, we start by looking at one approach to object-oriented software composition: mixin layers. Fig. 1(a), 1(b) and 1(c) introduce our running example: a system consisting of the program base and the mixin layers undo and subonly. A first clue about composition is that applying a layer to a program can be viewed as applying a function to a constant: Take base (Fig. 1(a)) as our base program with the single class Calculator. Then layer undo (Fig. 1(b)) is a “function” that, if applied to the “constant” base produces the new program undoCalc = undo(base) with an incremented version of Calculator: It now contains the new field savedMemory and the new method undo and a statement has been prepended to method add. Layer subonly (Fig. 1(c)) removes one method and adds another one.

Is there a way to create some kind of programming language to express the changes performed by a mixin layer? We first need to find out what kind of data is to be manipulated by such a programming language. This will hopefully lead us to a better understanding of what operators make sense. How can an objectoriented program in general and a base program in particular be represented in an elegant data structure? Looking at a diagram of base (Fig. 2(a)) it is fairly obvious that it is a labeled tree. We often leave the root unlabeled and annotate the arrows with labels because this reflects the data structure for trees that we’ll introduce later. Generally, at every level of encapsulation in an object-oriented program, there is an entity that contains a set of named entities: A class contains a set of methods, a package contains a set of classes etc. (Fig. 2(b)). We call sets of entities collectives (set Coll) and all entities (including collectives) units^{1} (set Unit ⊃ Coll). Another way to look at a labeled tree is as nested records. Then a collective is a record and each of the collective’s members is a field in that

1 We use this term differently from the unit type in type theory!

prog base;
class Calculator {
Int memory;
Calculator() {
  this.memory = new Int();
}
void add(Int i) {
  this.memory.add(i);
}
}

(a) Program base provides the initial version of class Calculator. Calculator contains an internal memory and can add() values of type Int to it.

layer undo;
class Calculator {
Int savedMemory;
@before void add(Int i) {
  this.savedMemory = this.memory;
}
void undo() {
  if (this.savedMemory == null) { } // Exception
  this.memory = this.savedMemory;
  this.savedMemory = null;
}
}

(b) Layer undo introduces the new member variable savedMemory to remember the last value of the memory and method undo() to restore this value. Additionally, we prepend code to method add() to make sure we save the state of memory before changing it. Note that we are using the JSR-175-style attribute [Bloch et al., 2002] @before to denote that method add is to be prepended to an existing method with the same name.

layer subonly;
class Calculator {
@remove add(Int i);
void sub(Int i) {
  this.memory.sub(i);
}
}

(c) Layer subonly removes addition from the calculator and introduces subtraction. We are using the attribute @remove to denote that an existing method add has to be removed.

Fig. 1. Running example.

(a) Looking at the structure of program base, it is obvious that it is a tree.

(b) An object-oriented program p comprises a set of classes which in turn are made up of methods. Representing the system as a labeled tree follows naturally from its structure: The root node has label p, its children the labels C_{1}, C_{2}, C_{3} etc.

Fig. 2. The structure of object-oriented software.

record. We can now draw on well-established ideas from database theory, more specifically, from tuple calculus to help us with the design of a language that operates on our data structure. Any kind of change that a mixin layer performs can be expressed as a sequence of the following operations; think of using a catalog of comparatively small refactoring steps for arbitrary transformations of a program [Fowler, 1999].

– insert : Coll × Name × Unit → Coll adds a named unit to a collective.

– delete : Coll × Name → Coll removes a unit (whose name is given by a parameter) from a collective.

– project : Coll × Name → Unit extracts a unit (whose name is given by a parameter) from a collective.

Let’s use these operators to describe how layer undo increments program base by the before-method add: We first have to project method add out of the program and prepend a new statement to its body. Then we project class Calculator, delete the old version of add and insert the new one. The result has to replace the old Calculator in base in the same fashion. We define update : Coll × Name × Unit → Coll to be a combination of delete and insert: update(v, n, w) := insert(delete(v, n), n, w). We also write projection as the infix ‘.’ (dot) operator and thus get the following meta program.

1 update(v, Calculator,

    2  update(v.Calculator, add,
    3  insert(v.Calculator.add, @before,
    4  this.savedMemory = this.memory;)))

This is what the code does (we explain the lines bottom-up):

– Lines 3 and 4: v.Calculator.add means: Project method add out of class Calculator out of the meta^{2} constant^{3} v (which holds the complete code of

   program base). Then insert the statement “this.savedMemory = this.memory;”

before the (body of) the result of this projection.

– Line 2: Project class Calculator out of v and replace the existing method add with the result from line 3.

– Line 1: Update v with the new Calculator from line 2.

This is a nice demonstration of how we only need a few basic mechanisms to implement the changes performed by mixin layers: line 3 and 2 perform an update on a collective and line 1 inserts a unit into a collective. But it is also apparent that this notation is too complicated and needs improvement! We’ll explain step by step what is wrong with it and how it can be fixed.

Step 1—eliminate the meta constant v: v keeps the meta code from being generic. Instead of running the code like an imperative program that destructively modifies the base program, we’d like to apply the transformation as a true function. We therefore use lambda notation to abstract the implicit parameter v. Then the meta program gets the prefix “λx” and every occurrence of the constant v is replaced by the variable x.

Step 2—make projection implicit: Lambda abstraction also gives us higherorder functions, allowing us to create a more elegant kind of update operation called at : Coll × Name × (Unit → Unit) → Coll. It applies a function to the member unit u (denoted by its name) of a collective and then replaces u with the result. This does away with projection as a full-blown separate^{4} operator and makes our meta code much more readable:

    1 λx. at(x, Calculator,

2  λy. at(y, add,

    3  λz.insert(z, @before, this.savedMemory = this.memory;)))

2 v is a constant in a meta language, that’s why we call it a meta constant. 3 v stands for a (completely reduced) value, as opposed to functions and partially

evaluated terms. 4 It is of course still implicitly present in the at operator.

Here is what happens:

– Line 1: Bind the collective to be modified to variable x. Update member Calculator of x by applying…

– Line 2: … a function that updates member add of its parameter by applying…

– Line 3: … a function that prepends a statement to the collective given as its argument.

Step 3—make parameter variables implicit: If we change at so that the collective to be modified is the last argument, we can use currying and its signature becomes at : Name × (Unit → Unit) → Coll → Coll. Then at is a map from a tuple^{5} (consisting of a Name and a function from Coll to Coll) to a program transformation (i. e., a function from Coll to Coll). Changing the signature of insert in the same manner eliminates the need for lambda notation, because there are no explicit parameters any more:

    at(Calculator,

at(add,

           insert(@before, this.savedMemory = this.memory;)))

Step 4—respect order in a collective: Until now, we assumed that a collective was unordered (i. e., a set). But the sequence of statements in a method^{6} is also a collective, so that we generally need to deal with ordered collectives. This leads to a slightly different set of operators.

at : Name × (Unit → Unit) → Coll → Coll
cons : Name × Unit → Coll → Coll
snoc : Name × Unit → Coll → Coll
delete : Name → Coll → Coll
override : Name × Unit → Coll → Coll

Explanation: cons and snoc are needed for ordered insertion^{7}: cons prepends a unit to a collective, snoc appends it. delete performs the same job as before. Interesting is override as a replacement for update. Whereas update was syntactic sugar for a combined delete/insert operation, we need to think about update differently if nodes in the tree are labeled ordered locations. Then delete removes a unit u and its location. We now cannot insert a new unit u′ to replace u at the old location (unless we remember where the label occurred). Therefore, we

5 We could have used currying for the first two arguments, too, but this signature corresponds more closely to how we use at and is useful in Sect. 4 where we give the formal definition of Graft’s type system.

6 In formal languages that are not used for programming (e. g., markup languages), order is also often significant. Therefore, this step prepares us for future uses of our framework.

7 We do not yet need positional insertion, but can easily add it to a future version of our framework should it be necessary.

need an in-place update and override serves that purpose^{8}. It replaces an existing member of a collective (whose name equals the first argument) with the second argument. Note that cons, snoc and override are always used with Unit literals.

Step 5—allow sequences of modifications: Right now, we can only apply single modifications to a collective, so we’re still missing a mechanism for applying a sequence of operations. As every manipulation is a function, we should obviously draw on function composition. As a slight twist, we don’t use the traditional functional composition operator ‘∘’ that evaluates from right to left: subonly(undo(base)) would become subonly∘undo(base). Instead, we prefer diagrammatic composition with the ‘;’ operator which evaluates from left to right. The previous composition is then written as (base)undo; subonly. This gives the meta language more of an imperative feel and makes meta programs easier to read. At last, we have a very compact notation for performing mixin layer composition. We have now arrived at the final version of Graft and demonstrate its use by implementing layer undo. Operator cons is used with the underscore ‘ ’ as the empty (or anonymous) label. That is, we don’t want to label the statement

“this.savedMemory = this.memory”:
    at(Calculator,
       cons(savedMemory, Int savedMemory);

at(add,

           cons( , this.savedMemory = this.memory));
       snoc(undo, void undo() {. . . }))

3 Motivating the Type System

In this document, software composition means either one of two things: We can (1) apply a function to a constant (i. e., apply a mixin layer to a base program) and we can (2) compose two functions (i. e., compose two layers to produce one combined layer). In either case, we want to know if the composition is possible before performing it. Guaranteeing safety of an operation is usually handled by a type system. But it is not obvious what the type of a layer should be. We will therefore look at a concrete example to find out what we need for checking the the feasibility of a composition:

1. Applying layer undo to a base program v: v cannot be just any program. There are certain constraints imposed on its structure by the operations used in undo. For example, there has to be a class Calculator and it has to contain a method add, otherwise we wouldn’t be able to perform the @before operation.

2. Composing layer undo and subonly: Applying layer undo after subonly will never work, because subonly deletes method add which makes it impossible for undo to prepend the @before code.

8 Another way to look at override is that override(n, v) is “lambda-free” syntactic sugar for at(n, λx.v).

Note that there are two cases of illegal composition that we (for now) do not want to catch:

– Applying subonly after undo disables undo. This is a semantic problem that we don’t treat here.

– The above composed layer, if applied to base, still produces a well-typed program (in the sense of the Java language specification [Gosling et al., 2000]). But what if the delete operation had removed a method that is called by another method. Then the modified program won’t compile any longer. This is basically a dependence problem and subject of current and future research.

What we do want to find out is what constrains the applicability of atomic and composite operations. It turns out that it depends on the presence or absence of nodes in the tree of the base program:

– at : Name × (Unit → Unit): at(n, f) can be applied to a collective c if in c, there is a unit u whose name is n. Additionally, f has to be applicable to u.

– cons : Name × Unit: cons(n, u) can be applied to a collective c if there is no unit in c that has the name n.

– The same constraint holds for snoc.

– delete : Name: We can only perform a delete operation if the name given exists in the collective that is to be modified.

– The same constraint holds for override.

That means that the type system does not need all the information stored in a code tree v to decide if an operation is applicable. It can work with an abstraction abs(v) of v. This abstraction only records the presence of nodes. That is, even though abs(v) is a labeled tree that is isomorphic to v, it is undecorated and unordered. Given a Graft program f, we can use the rules listed above to automatically infer the applicability constraints of f. We encode these constraints in a data structure G that is called guard, because it serves the same purpose as guards in functional programming languages. Applicability is then tested by a guard check operator ‘|’: abs(v) | G holds if and only if f is applicable to v. As guards are matched against abstracted programs, it is natural to also express them as labeled unordered trees. The guard tree is decorated with elements of the set^{9} {⊕, ⊖}. If a node has to exist, we tag it with a plus ⊕. If the node must not exist, we use a minus ⊖. Otherwise, we don’t care about the node and it does not appear in the guard. Fig. 3 shows the guard tree for one instance of snoc and one instance of delete. Constructing the guard for at is a bit more complicated, because it depends on the guard of the second argument. Fig. 4 shows how we construct at’s guard by creating a new root to be the parent of the argument’s guard. The child’s label is given by the Name argument.

Guards make the feasibility check trivial when applying a layer to a base program, but we have not yet figured out how to perform it for compositions

9 For uniformity reasons, we decorate nodes in program abstractions with a ⊕ from now on.

Fig. 3. Guard trees for snoc(undo, …) and delete(add)

Fig. 4. Guard tree for at(Calculator, delete(add)): The guard of delete plus a new root is the composite guard of at.

of layers. Two problems have to be solved: (1) How to check if a layer composition is legal and (2) how to calculate the composite guard for the combined layer. The difficulty with the combined guard is that it is not just the union of the two guards, because the changes effected by the first layer might fulfill some of the preconditions of the second guard. This is the case if we write cons(foo, …); delete(foo)—we are deleting something that we introduced, therefore the precondition of delete that foo has to exist does not have to be propagated to the composite guard. On the other hand, an operation might make subsequent guards impossible to satisfy: In delete(bar); override(bar, …), we remove bar and cannot override it afterwards. The guard can be seen as an abstract interface of a Graft program f. But it has become obvious that, if we are to compute combined guards, this interface should not only describe the prerequisites for, but also the effects of, f. Thus, we express the interface of f as a pair (G, U), where G is the guard and U is a data structure that encodes how f modifies a program. We write f ↑ G ⇝ U to say that f has the interface (G, U). Just like we abstracted code trees, we also abstract the effect of f and are only interested whether it adds or removes nodes. For the same reasons as above, we record U as a labeled unordered tree and call it update tree. An update tree has the same format as a guard. It is, however, interpreted differently: If a node is decorated with ⊕, it means that an operation adds this node, ⊖ indicates a removal. To give an example, we show that the construction of the update tree for at resembles what we have done with guards: We “prepend” a root to the update tree of the argument (Fig. 5). The root is always decorated with a ⊕, because any change inside a collective has to guarantee its existence.

Coming back to our problems, we can solve (2), how to compute the combined guard, if we overload operator ‘;’ for (G, U) pairs. Then, if we compose two operations as f; g where f ↑ G_{1} ⇝ U_{1} and g ↑ G_{2} ⇝ U_{2}, we get the combined guard G′ from (G′, U′) = (G_{1}, U_{1}); (G_{2}, U_{2}). Problem (2), how to check for legal

Fig. 5. Update tree for at(Calculator, delete(add))

layer compositions, is solved by letting the composition operator return undefined if U_{1} and G_{2} are incompatible. This makes composition a partial function.

4 Type System

In this section, we give a more rigorous and formal definition of Graft’s type system. Recall that a transformation f of a typed source program v into a target program w may be unsuccessful for one of the following reasons:

1. One of the operations involved in f fails (e. g., modifying a non-existent method).

2. The transformed program does not compile any more.

3. The target program does not exhibit the expected behavior.

We now develop a type system which helps to detect some of these failures statically (i. e., before actually carrying out the transformation). Errors of category 3 are clearly out of reach for automatic analyses; to ensure preservation of welltypedness (cat. 2) would be desirable, but for now, we only guarantee that all operations can be performed (cat. 1).

4.1 Typing

Our type system results from an abstract interpretation [Cousot, 2001] of programs v, w (as types A, B) and operations f.

\xymatrix{v \ar[r]^{f} \ar[d]^{abs} & w \ar[d]^{abs} \\ A \ar[r]^{abs(f)} & B}

It has the following soundness property: If the abstract operation abs(f) succeeds on the abstract program A, then the concrete operation f also succeeds on the concrete program v. We follow standard programming language theory and introduce these notions:

v : A The program v has type A. From now on, we call the abstraction function from programs to types typeof, therefore A = typeof(v) f : A → B Operation f takes programs of type A to programs of type B. Equiv-

alently, we can say that the abstract operation abs(f) maps an abstract program A to an abstract program B.

In our case, a program v is just a labeled tree with some data d at each node. Its type A abstracts away the stored data and only tells us which nodes exist in the tree. Thus, to get A, we simply replace all data in v by a special symbol ⊕ (Fig. 6). Alternatively, A can be seen as a function from paths p into the set {⊕, ⊖} where A(p) = ⊕ if the path p exists in v, otherwise A(p) = ⊖.

Fig. 6. The abstract interpretation of program prog is a tree. Note that the order of children is not significant.

A well-typed operation f : A → B is applicable to all trees v which have shape A and results in trees of type B. The result type B can be computed from A by performing the abstract version of the operation f on A. For instance,

\overline{cons(n, v) : A → B} if A(n) = ⊖ and B = A[n ↦ typeof(v)]

Here “A(n) = ⊖” says that the singleton path n does not exist in A, and “B = A[n ↦ typeof(v)]” expresses that B results from adding the type of v as a subtree named n to A. For the other operators, we get similar typing rules (see appendix).

A term is either a value (i. e. a program) v or a Graft operation f applied to a value as (v)f. Evaluation of terms is defined using two relations: t ⇓ v means that term t reduces to value v. v −f⟶ w means that applying operation f to value v results in value w.

The type system has the desired properties: each well-typed program transformation can be executed.

Theorem 1 (Type preservation and normalization).

1. If t : A then A ≠ ⊖, t ⇓ v and v : A.

2. If v : A and f : A → B then v −f⟶ w and w : B.

The proof is easy after a complete formalization of the type system (see appendix).

4.2 Type inference

At the current state, we can compute the type A of a tree v and the type B of applying a transformation f to v. This is not yet satisfactory; we want to compute the type of f independently of its argument, because this enables us to type-check each mixin layer f, g individually and then check whether a composition f; g is possible. The problem with the type system so far is that we can assign an infinite number of types A → B to an operation f. (For example, the domain A of operation delete(n) can be any type with A(n) = ⊕.)

In the following, we overcome this problem by specifying an inference system for most general types f ↑ G ⇝ U. A most general type of an operation f consists of a guard G and an update U. Given the most general type, f can be assigned a type A → B if the domain A fulfills guard G, written A | G, and if B results from A updated by U, written B = A[U].

In essence, guards G are partial types, specifying only these parts of the abstract tree of A which it has to contain for an operation to be executed. Formally, guards are partial functions from paths into the set {⊕, ⊖}, or, equivalently, total functions in Path → {⊕, ⊖,?}. Here, G(p) = ? means that does not impose any conditions on path p. If otherwise G(p) ∈ {⊕, ⊖}, then A(p) has to match G(p). This is expressed in the following definition: The relation A | G holds iff for all paths p, A(p) coincides with G(p) unless G(p) = ?.

Updates U are of the same shape as guards. The effect of an update B = A[U] can be described pointwise for all paths p: if U(p) = ?, i. e., no update is specified, then nothing changes and B(p) = A(p); otherwise, the old content is overwritten as specified by U and B(p) = U(p).

We are now ready to give most general types for the basic operations, e. g.

\overline{cons(n, v) ↑ \{n ↦ ⊖\} ⇝ \{n ↦ A\}} where A = typeof(v)

Here, the guard G is a partial function which maps n to ⊖ and is completely undefined elsewhere. The update U specifies that name n should now be mapped to subtree A. By looking at the original typing rule of cons we can immediately verify that this guard/update pair is the most general type of cons(n, v).

A little more work has to be done for composite operators f; g. Assume f ↑ G_{1} ⇝ U_{1} and g ↑ G_{2} ⇝ U_{2}, what should guard G and update U of the composite operation f; g look like? If f and g are disjoint, i. e., modifying different regions of a program, then the common guard G = G_{1} ∪G_{2} is the union of the two partial functions G_{1} and G_{2} (and similar for U). For the case that f and g interfere, the common update is simply given by U = U_{1}[U_{2}], which is defined in the same way as the update on types B = A[U] (see above). In this case, g may override some updates performed by f.

To compute the common guard G, let us first consider that U_{1} does not interfere with G_{2}, i. e., f does not update parts of the tree G_{2} speaks about. The joint guard G is written G_{1} ∨ G_{2} and does not exist if G_{1} contradicts G_{2}. This is, for instance, the case if G_{1} requires some path p to be present and G_{2} requires it to be absent (or the other way round). Otherwise G_{1} ∨ G_{2} = G_{1} ∪ G_{2}. Some type A passes the two single guards, A | G_{1} and A | G_{2}, if and only if the joint guard G = G_{1} ∨ G_{2} is defined and A | G holds.

In some cases the first update U_{1} will fulfill some requirements of the second guard G_{2}. When we compute the joint guard, these requirements can be dropped. To this end, we define a partial simplification operation G \ U with the following behavior: A[U] | G if and only if G′ = G\U is defined and A | G′. The new guard G′ is defined if U does not contradict G, i. e., if G ∨ U is defined. In this case, G′ can be computed pointwise: if the old requirement G(p) if fulfilled by the update U(p), it is dropped and G(p′) = ?, otherwise it is kept and G(p) = G(p′). Now the typing rule for composition should be clear:

\frac{f ↑ G_{1} ⇝ U_{1} g ↑ G_{2} ⇝ U_{2}}{f; g ↑ G_{1} ∨ (G_{2} \ U_{1}) ⇝ U_{1}[U_{2}]} if G_{1} ∨ (G_{2} \ U_{1}) defined

For completeness, we present the rules for the type inference t ↑ A for terms. The typing rule for application of operations f to trees t connects most general types to ordinary types:

\overline{v ↑ typeof(v)}  \frac{v ↑ A  f ↑ G ⇝ U}{(v)f ↑ A[U]} if A | G

It remains to show that type inference is sound, which can be done by inspecting the typing rules, using the fundamental properties of guard and update joining.

Theorem 2 (Soundness of type inference).

1. If t ↑ A then t : A.

2. If f ↑ G ⇝ U and A | G then f : A → A[U].

For a proof and a complete formalization, consult the appendix.

4.3 Example

Let’s demonstrate type inference for the layers subonly and undo and show how typing of the composite operation subonly;undo fails. Layer subonly is implemented in Graft as follows:

    subonly = at(Calculator,

delete(add); snoc(sub, …))

We give the result of type inference for subonly step by step:

delete(add) ↑ {add ↦ ⊕}  ⇝ {add ↦ ⊖}
snoc(sub, …) ↑ {sub ↦ ⊖}  ⇝ {sub ↦ ⊕}
delete(…); snoc(…) ↑ {add ↦ ⊕, sub ↦ ⊖} ⇝ {add ↦ ⊖, sub ↦ ⊕}

 at(Calculator, . . .) ↑ {Calculator ↦ {add ↦ ⊕, sub ↦ ⊖}} =: G_{1}
                  ⇝ {Calculator ↦ {add ↦ ⊖, sub ↦ ⊕}} =: U_{1}

For layer undo we get the guard

G_{2} = {Calculator ↦ {savedMemory ↦ ⊖, add ↦ ⊕, undo ↦ ⊖}}

In the process of calculating the joint guard for (subonly; undo), the simplification operation G_{2} \ U_{1} fails already, since the operands differ on the existence of

the path (Calculator, add):

U_{1}(Calculator, add) = ⊖
G_{2}(Calculator, add) = ⊕

Hence type inference fails for the composition of the two layers, which indicates an inconsistency.

5 Related Work

Related work can be grouped into the following categories:

– Composition paradigms: Each of these paradigms supports one kind of composition. Additionally, and this is similar to Graft, they enable validity checks for their operations. The advantage of concentrating on only one way of composition is that these validity checks are very evolved and well adapted for this one purpose. Graft’s goals for the future are broader: We want a less sophisticated framework (with specialized “plug-ins” for some features) to support several ways of composition and more artifacts than just code. Examples: Detection and resolution of aspect interactions [Douence et al., 2002], invasive composition [Aßmann, 2003], traits [Schärli et al., 2003], composition of class hierarchies [Snelting and Tip, 2002].

– Object-oriented language calculi: This category is even more specialized than the last one, but shares the use of formal methods with Graft. Examples: Reduction semantics for classes and mixins [Flatt et al., 1999], core calculus of classes and mixins [Bono et al., 1999].

– General meta programming: These are full-blown languages which enable many powerful program generation tasks that Graft can’t perform. In contrast, we aim for simplicity and our focus on program transformation is slightly different. Examples: Logic meta programming [Brichau et al., 2002], OpenJava [Tatsubori et al., 2000], multi-stage languages [Calcagno et al., 2003].

– Program transformation: This category has many similarities to the last one and is closely related to Graft. Again, we sacrifice generality for simplicity which makes many consistency checks easier to perform. Examples: Strategic programming [Lämmel et al., 2003], program transformation through the manipulation of semantic graphs [Gosling, 2003].

– Separate compilation: Separate compilation is mainly concerned with providing self-sufficient typing for program fragments. This is an area that is currently completely ignored by Graft. On the other hand, separate compilation is only concerned with composition as linking and other manipulations are—if at all—limited. Examples: Fragment calculus [Drossopoulou et al., 1999], true separate compilation of Java classes [Ancona et al., 2002].

Two publications deserve particular mention, because they are the most similar in nature to Graft:

– Design rule checking [Batory and Geraci, 1997]: Design rules are complementary to our approach. They are manual annotations of units in propositional logic and capture semantics. Whereas Graft relies on syntactic analysis that is performed automatically.

– Reuse contracts: are concerned with step-wise evolution of programs while checking consistency constraints [Mens, 2001]. They also have a well-defined and powerful type system and have already been applied to a wide variety of artifacts [Mens and D’Hondt, 2000]. While our work is currently less ambitious, using trees and a language for their manipulation makes Graft simpler and easier to understand.

6 Conclusions and Future Research

In this paper, we have presented Graft, a simple meta language for generically expressing composition. It is complemented by a type system that allows one to check the applicability of a Graft program before actually applying it. As a practical example, we demonstrated Graft’s ability to express mixin layer composition. The main contributions of our work are Graft’s simplicity, elegance and universality; its rigorous definition (where many composition mechanisms are not that clearly defined); and the type-safety of its programs, which includes the use of inference to save human effort. The intended “end-user” of Graft is not the programmer. Instead, tool implementors will write compilers that translate source code plus annotations into Graft in order to perform checks and verification. Another possible use case is to let small Graft programs execute type-safe refactorings.

We strove to make this first version of Graft a minimal, clean core to help us understand the issues involved in creating a composition language. These attributes make the core a strong foundation for the following future experiments and extensions:

– We have started to implement Graft in Haskell (which, in this case, is the meta meta language). This version of Graft operates on MJ [Bierman et al., 2003], a subset of Java.

– We cannot yet guarantee the well-typedness of a program after it has been manipulated by Graft code. To achieve this, we have experimented with partial types and plan to make them part of a future version of Graft.

– Graft should also support more features of the language that is to be modified (the object language): Reflective features, pre/post conditions, call history enforcement and others come to mind. For that, more of the semantics of the object language has to be made explicit.

– We will investigate what other programming language features (such as conditionals, loops, quantifiers, procedures etc.) make sense for Graft.

– In creating Graft, we lay some groundwork for the future support of artifact types other than code (documentation, UML diagrams etc.). AHEAD [Batory et al., 2003] already gives some ideas how mixin layer composition can be extended to non-code artifacts. Frame-based programming [Bassett, 1996] can also be used to produce all sorts of artifacts and motivated some of Graft’s basic features. We hope that our type system will remain generic enough to be applicable across artifact kinds. Consistency enforcement could then be cross-cutting, too (e. g., if a class is part of the source code, it also has to appear in the UML class diagram).

– Finally, we have to find out how Graft can express other composition mechanisms than mixin layers, such as aspects.

Acknowledgements. Thanks to Jörg Striegnitz for recommending MJ.

A Graft Specification

A.1 Trees

Name ∋ n, m  Names
Path ∋ p ::= n_{1}, …, n_{k} (k ≥ 0) Paths
D ∋ d  Data (tree decoration)
Unit ∋ u ::= n::v  Named units
Coll ∋ c ::= u_{1}, …, u_{k} (k ≥ 0) Collectives
Tree ∋ v, w ::= ⟨d; c⟩  Decorated trees (values)

Collectives can be viewed as partial functions from names to trees resp. as total functions to Tree^{⊖} := Tree ∪ {⊖}.

Coll ⊆ Name → Tree^{⊖}

(\begin{matrix}−⇀ \\ n::v \end{matrix})(m) = v_{i} if m = n_{i}
(\begin{matrix}−⇀ \\ n::v \end{matrix})(m) = ⊖ if m ∉ \begin{matrix}− ⇀ \\ n \end{matrix}

Similarily, trees can be viewed as as total functions from paths into D^{⊖} := D ∪ {⊖}. We extend the domain of this coercion to Tree^{⊖}.

Tree^{⊖} ⊆ Path → D^{⊖}

⊖(p)  = ⊖  empty tree
⟨d; c⟩() = d  empty path
⟨d; c⟩(n, p) = c(n)(p) composite path

A.2 Operations and Terms

Op ∋ f, g ::= cons(n, v)  prepend unit n::v to current collective
| snoc(n, v)  append unit
| override(n, v) replace unit named n by new unit n::v
| delete(n)  delete unit named n from current collective
| at(n, f)  apply operation f to unit named n
| f; g  operation sequence
Term ∋ t ::= v  tree value
| (v)f  (left hand side) application of operation

Transformation of trees v −f⟶ w.

\frac{c −f⟶ c′}{⟨d; c⟩ −f⟶ ⟨d; c′⟩}

Transformation of collectives c −f⟶ c′.

\overline{c −cons(n, v)⟶ n::v, c} if n ∉ c \overline{c −snoc(n, v)⟶ c, n::v} if n ∉ c

c, n::v, c′ −override(n, v′)⟶ c′, n::v′, c′ \overline{c, n::v, c′ −delete(n)⟶ c, c′}

\frac{v −f⟶ v′}{c, n::v, c′ −at(n, f)⟶ c, n::v′, c′}  \frac{c_{1} −f⟶ c_{2}  c_{2} −g⟶ c_{3}}{c_{1} −f; g⟶ c_{3}}

Evaluation t ⇓ v.

\overline{v ⇓ v}  \frac{v −f⟶ w}{(v)f ⇓ w}

A.3 Tree Types and Typing

Type = (Name → Type) ∪ {⊖}
Type ∋ A, B  Types
Type ⊆ Path → {⊕, ⊖}
⊖(p) = ⊖
A() = ⊕ if A ≠ ⊖
A(n, p) = A(n)(p)

On the other hand, for each B ∈ Path → {⊕, ⊖}, there exists an equivalent A ∈ Type: If B(p) = ⊖ for all p ∈ Path, then A := ⊖. Otherwise, let recursively A(n) be the type equivalent to the function B(n, ). By this isomorphism, we can conveniently specify the type of a tree:

typeof ∈ Tree → Type

typeof(v)(p) = ⊖ if v(p) = ⊖
typeof(v)(p) = ⊕ else

Type update A[n ↦ B] ∈ Type.

⊖[n ↦ B] = ⊖
A[n ↦ B](n) = B  if A ≠ ⊖
A[n ↦ B](m) = A(m) if A ≠ ⊖ and m ≠ n

Typing of terms t : A.

\overline{v : typeof(v)}  \frac{v : A  f : A → B}{(v)f : B}

Typing of operations f : A → B.

If A(n) = ⊖ : \frac{v : A′}{cons(n, v) : A → A[n ↦ A′]} \frac{v : A′}{snoc(n, v) : A → A[n ↦ A′]}

If A(n) ≠ ⊖ : \frac{v : A′}{override(n, v) : A → A[n ↦ A′]} \overline{delete(n) : A → A[n ↦ ⊖]}

\frac{f : A(n) → A′}{at(n, f) : A → A[n ↦ A′]} if A(n) ≠ ⊖  \frac{f : A_{1} → A_{2}  g : A_{2} → A_{3}}{f; g : A_{1} → A_{3}}

Theorem 1 (Type preservation and normalization).

1. If t : A then A ≠ ⊖, t ⇓ v and v : A.

2. If v : A and f : A → B then v −f⟶ w and w : B.

Proof. Simultaneously by structural induction on the judgments t : A and f : A → B.

A.4 Guards and Updates

G ∈ Guard = Path → {⊕, ⊖,?} conditions on types
U ∈ Update = Path → {⊕, ⊖,?} modifications of types

Guard checking A | G.

A | G ⟺ A(p) | G(p) for all p ∈ Path where
a | g ⟺ g = ? or a = g

Applying updates U_{1}[U_{2}] ∈ Update. (Defines also P [U] ∈ Type since Type ⊆ Update.)

U_{1}[U_{2}](p) = U_{1}(p)[U_{2}(p)] where
u_{1}[u_{2}] = u_{1}  if u_{2} = ?
u_{1}[u_{2}] = u_{2}  else

Lemma 1 (Associativity). U_{1}[U_{2}][U_{3}] = U_{1}[U_{2}[U_{3}]].

Guard joining G_{1} ∨ G_{2} ∈ Guard (symmetric partial operation).

(G_{1} ∨ G_{2})(p) = G_{1}(p) ∨ G_{2}(p) where
g_{1} ∨ g_{2}  = g_{1}  if g_{1} = g_{2} or g_{2} = ?
g_{1} ∨ g_{2}  = g_{2}  if g_{1} = ?
g_{1} ∨ g_{2}  = undefined  otherwise

G_{1} ∨ G_{2} is only defined if G_{1}(p) ∨ G_{2}(p) is defined for all p ∈ Path.

Lemma 2 (Joint guard checking). A | G_{1} and A | G_{2} iff G_{12} := G_{1} ∨ G_{2} is defined and A | G_{12}.

Guard updates G \ U ∈ Guard (partial operation).

(G \ U)(p) = G(p) \ U(p) where
g \ u  = g  if g = ? or u = ?
g \ u  = ?  if g = u
g \ u  = undefined  otherwise

Lemma 3 (Updated guard checking). A[U] | G iff G′ := G \ U is defined and A | G′.

A.5 Type Inference

Type inference t ↑ A.

\overline{v ↑ typeof(v)}  \frac{v ↑ A  f ↑ G ⇝ U}{(v)f ↑ A[U]} if A | G

Most general types for operations f ↑ G ⇝ U.

\frac{v ↑ A}{cons(n, v) ↑ \{n ↦ ⊖\} ⇝ \{n ↦ A\}}  \frac{v ↑ A}{snoc(n, v) ↑ \{n ↦ ⊖\} ⇝ \{n ↦ A\}}

\frac{v ↑ A}{override(n, v) ↑ \{n ↦ ⊕\} ⇝ \{n ↦ A\}}  \overline{delete(n) ↑ \{n ↦ ⊕\} ⇝ \{n ↦ ⊖\}}

\frac{f ↑ G ⇝ U}{at(n, f) ↑ \{n ↦ G\} ⇝ \{n ↦ U\}}

\frac{f_{1} ↑ G_{1} ⇝ U_{1} f_{2} ↑ G_{2} ⇝ U_{2}}{f_{1}; f_{2} ↑ G_{1} ∨ (G_{2} \ U_{1}) ⇝ U_{1}[U_{2}]} if G_{1} ∨ (G_{2} \ U_{1}) defined

Theorem 2 (Soundness of type inference).

1. If t ↑ A then t : A.

2. If f ↑ G ⇝ U and A | G then f : A → A[U].

Proof. Simultaneously by structural induction on the judgments t ↑ A and f ↑ G ⇝ U.

References

Davide Ancona, Giovanni Lagorio, and Elena Zucca. True separate compilation of Java classes. In Proc. 4^{th} Conf. Principles and Practice of Declarative Programming (PPDP), pages 189–200. ACM Press, 2002.

Uwe Aßmann. Invasive Software Composition. Springer, 2003. Paul G. Bassett. Framing Software Reuse: Lessons From the Real World. Pren-

tice Hall, 1996. Don Batory and Bart J. Geraci. Composition Validation and Subjectivity in

GenVoca Generators. IEEE Trans. Software Engineering, 23(2):67–82, 1997. Don Batory, Jack Sarvela, and Axel Rauschmayer. Scaling Step-Wise Refine-

ment. In Proc. 25^{st} IEEE Int. Conf. Software Engineering (ICSE). IEEE, 2003.

Gavin M. Bierman, Matthew J. Parkinson, and Andrew M. Pitts. MJ: An imperative core calculus for Java and Java with effects. Technical Report 563, University of Cambridge, 2003.

Joshua Bloch et al. A Metadata Facility for the Java Programming Language,

2002. URL http://www.jcp.org/en/jsr/detail?id=175. Java Specification

Request 175. Viviana Bono, Amit Patel, and Vitaly Shmatikov. A Core Calculus of Classes

and Mixins. In Rachid Guerraoui, editor, Proc. 13^{th} Europ. Conf. Object-Oriented Programming (ECOOP), volume 1628 of Lect. Notes Comp. Sci., pages 43–66. Springer, 1999.

Johan Brichau, Kim Mens, and Kris De Volder. Building Composable Aspect-Specific Languages with Logic Metaprogramming. In Proc. 1^{st} Conf. Generative Programming and Component Engineering (GPCE), volume 2487 of Lect. Notes Comp. Sci., pages 110–127, October 2002.

Cristiano Calcagno, Walid Taha, Liwen Huang, and Xavier Leroy. Implementing

Multi-Stage Languages Using ASTs, Gensym, and Reflection. 2003. Patrick Cousot. Abstract Interpretation Based Formal Methods and Future

Challenges. In Reinhard Wilhelm, editor, Informatics—10 Years Back, 10 Years Ahead, volume 2000 of Lect. Notes Comp. Sci., pages 138–156. Springer, 2001.

Rémi Douence, Pascal Fradet, and Mario Südholt. A Framework for the Detection and Resolution of Aspect Interactions. In Don S. Batory, Charles Consel, and Walid Taha, editors, Proc. 1^{st} Conf. Generative Programming and Component Engineering (GPCE), volume 2487 of Lect. Notes Comp. Sci., pages 173–188, 2002.

Sophia Drossopoulou, Susan Eisenbach, and David Wragg. A Fragment Calculus Towards a Model of Separate Compilation, Linking and Binary Compatibility. In Proc. 14^{th} IEEE Symp. Logic in Computer Science, pages 147–156. IEEE, 1999.

Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen. A Programmer’s Reduction Semantics for Classes and Mixins. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lect. Notes Comp. Sci., pages 241–269. Springer, 1999.

Martin Fowler. Refactoring. Addison Wesley, 1999. James Gosling. Program Transformations Through the Manipulation of Se-

mantic Graphs, January 2003. URL http://www.sigs.de/kongresse/oop_

2003/key_gosling.zip. Keynote SIGS-DATACOM Conf. Object-Oriented Programming (OOP 2003).

James Gosling, Bill Joy, Guy Steele, and Gilad Bracha. The Java Language

Specification. Addison Wesley, 2000. Gregor Kiczales, Erik Hilsdale, Jim Hugunin, Mik Kersten, Jeffrey Palm, and

William G. Griswold. An Overview of AspectJ. In Jørgen Lindskov Knudsen, editor, Proc. 15^{th} Europ. Conf. Object-Oriented Programming (ECOOP), volume 2072 of Lect. Notes Comp. Sci., pages 327–353. Springer, 2001.

Ralf Lämmel, Eelco Visser, and Joost Visser. Strategic Programming Meets Adaptive Programming. In Proc. 2^{nd} Conf. Aspect-Oriented Software Development (AOSD). ACM Press, 2003.

Tom Mens. A Formal Foundation for Object-Oriented Software Evolution. In

Proc. Int. Conf. Software Maintenance (ICSM), pages 549–552. IEEE, 2001. Tom Mens and Theo D’Hondt. Automating Support for Software Evolution in

UML. Automated Software Engineering, 7(1):39–59, 2000. Nathanael Schärli, Stéphane Ducasse, Oscar Nierstrasz, and Andrew Black.

Traits: Composable Units of Behavior. In Proc. 17^{th} Europ. Conf. Object-Oriented Programming (ECOOP). Springer, 2003. To appear.

Yannis Smaragdakis and Don Batory. Implementing Layered Design with Mixin Layers. In Eric Jul, editor, Proc. 12^{th} Europ. Conf. Object-Oriented Programming (ECOOP), volume 1445 of Lect. Notes Comp. Sci., pages

550–570, 1998. URL http://www.cs.utexas.edu/users/schwartz/pub.
htm#ecoop-templates.

Gregor Snelting and Frank Tip. Semantics-Based Composition of Class Hierarchies. In Proc. 16^{th} Europ. Conf. Object-Oriented Programming (ECOOP), volume 2374 of Lect. Notes Comp. Sci., pages 562–584. Springer, 2002.

Michiaki Tatsubori, Shigeru Chiba, Marc-Olivier Killijian, and Kozo Itano. OpenJava: A Class-Based Macro System for Java. In Walter Cazzola, Robert J. Stroud, and Francesco Tisato, editors, Reflection and Software Engineering, volume 1826 of Lect. Notes Comp. Sci., pages 117–133. Springer, 2000.