different. To this end, one needs four variants of the class (and module) modeling the memory model. This is achieved (in Delta-ABS) by manually copying the class `Memory` to four modules `MemoryInternal`, and creating two copies of the class `DevicePair` in two modules `DeviceInternal`.

* **AISCO (Adaptive Information System for Charity Organizations)** is a modular web portal supporting the business processes (information, reporting, spending, expenditure) of charity organizations.
There are two versions of AISCO. The first, referred to as AISCO-1 (Setyautami et al., 2019), consists of an SPL is implemented in Delta-ABS. Its variability reflects differing legal and operational requirements of the supported organizations. Interoperability is not supported, hence variability is encoded using multiple copies of classes.

The second version, referred to as AISCO-2 (Setyautami and Hähnle, 2021), is implemented in Java. It supports some of the functionalities of VMs by relying on an external tool, also written in Java: Different variants of a module are generated by the runtime structure, using the external tool on top of the Java implementation, see Section 12.4 for details. The code is used in production at https://amanah.cs.ui.ac.id/.

By refactoring the above models to ABS-VM, we illustrate different aspects in using VMs to model interoperable variants:

**VMs vs. Traits.** In FormbaR-2, implemented in Delta-Trait-ABS, traits<fnref n="16" /> are used to reduce code duplication across class definitions implementing variants of the same infrastructure element. In the refactoring of FormbaR-2, written in Delta-Trait-ABS, to ABS-VM we show how the relevant parts of FormbaR are re-modeled using VMs.

**VMs vs. Delta-oriented SPLs.** In the refactoring of WMMF-2, written in Delta-ABS, to ABS-VM we show that in the latter there is no need to manually duplicate modules.

**VMs vs. External tool chain.** We compare AISCO-2, which uses an external mechanism implemented in Java to provide VM functionality,<fnref n="17" /> with our re-implementation in ABS-VM.

*Experiment design.* **RQ 1** is addressed by manually refactoring the FormbaR-2, WMMF-2, and AISCO-2 model to ABS-VM and comparing *conceptually* the legacy implementation with the ABS-VM implementation. **RQ 2** is addressed by comparing the number of lines of code (LoC) before and after refactoring.

### 11.2.2. Experiment design and subject for RQ 3 and RQ 4

For the remaining two research questions we perform experiments on the three models introduced in **RQ 1**, **RQ 2**. For each model we compare the times needed to complete the following tasks: checking normal form and type uniformity, checking applicability consistency, checking pre-typing, performing overall flattening, and performing flattening.

Additionally, for **RQ 3**, we run two experiments on synthetic data sets: We generate programs with random feature models and compare the time needed to check applicability consistency with the time needed to perform overall flattening (Synthetic Experiment 1 below) and we measure the time needed to check applicability consistency (Synthetic Experiment 2).

All experiments are performed on an Ubuntu 20.04 system running on a quadcore i7-8565U CPU @ 1.80 GHz with 32 GB RAM.

**Synthetic Experiment 1.** We generate for $n \in [1... 12]$ a module with $n$ features, each feature associated with one delta adding one method $m_n$ to the sole interface of the module. The module then declares one variable for each of the $2^n$ variants.

**Synthetic Experiment 2.** To evaluate applicability checking on non-trivial feature models we modify the above scenario: We generate random feature models and application conditions using the random formula generator by Roffe and Calderon (2021). Additionally, each delta now either adds, removes or modifies a method from the interface. We run this experiment for $n \in [1... 50]$.

### 11.3. Results for RQ1

#### 11.3.1. Formbar

The partial refactoring of FormbaR-2 to ABS-VM, referred to as FormbaR-3, has one VM with five features: PoV for points of visibility (of signals, etc.), Speed for signals that announce a speed restriction, Signal for general signals, Main for signals placed at the point, where the signaled aspect holds, and Pre for signals that announce a point where the signaled aspect holds. Hence, the VM contains features (Main, Pre, Speed, Signal, PoV) plus deltas for the five re-modeled kinds of signal.<fnref n="18" />

FormbaR-2 uses traits to reduce code duplication in the implementation of the different kinds of signals. FormbaR-3 has no need for traits: a set of operations is encapsulated in a delta and applied to a base TrackElement class. The feature model connects these operations explicitly with products corresponding to relevant infrastructure elements.

*Results.* The drawbacks of using an intra-product code reuse mechanism (like traits) to implement variants are discussed in Section 3. In consequence, FormbaR-3 is (i) shorter than FormbaR-2 (in terms of LoC), because in the latter there is a separate class for each kind of signal (see Section 11.4 for details). (ii) FormbaR-3 is also more comprehensible. For once, its feature model makes constraints explicit that were only implicit in FormbaR-2 (for example, that certain traits should not be used in a class at the same time). In addition, it declaratively connects code variability to the domain model. For example, in FormbaR-3 the feature model expresses that a pre-signal has features Pre and Signal in a semantic manner in terms of a general Signal that announces its aspect Pre.

#### 11.3.2. WMMF

In WMMF-2 we need potentially four different memory models. The Delta-ABS implementation requires to copy the memory model module *including all deltas* four times. Furthermore, the device module had to be copied twice. Essentially, we perform *manually* part of the VM flattening until we can rely on standard module operations.

Instead, the ABS-VM model, referred to as WMMF-3, contains one VM for `Memory` and one for `DevicePair` (i.e., pairs of memory models). While WMMF-3 has six features for `Memory` and eight for `DevicePair`, WMMF-2 has 40.

*Results.* VMs permit concise modeling of interoperable variants, as compared to modeling them explicitly with one product line and manual copying. In particular, the possibility to directly use products as type references removes the necessity to declare all possible products in advance and to decide upfront on the number of variants to be generated: ABS-VM does not require a known bound on the number of copies and can handle encapsulation using the VM mechanism.

<footnote n="16">16 Traits (Schärli et al., 2003; Ducasse et al., 2006) are sets of methods that can be added to a class. The ABS-VM implementation supports traits. Since traits are orthogonal to the notion of VM we have not included them in the fragment of ABS-VM formalized in this paper. We refer to Damiani et al. (2017a) for a presentation of the notion of traits supported by ABS.</footnote>

<footnote n="17">17 The VM concept was first developed and implemented for ABS (Damiani et al., 2021), then partially adapted and implemented in the Java runtime library (Setyautami and Hähnle, 2021).</footnote>

<footnote n="18">18 Main signal, pre-signal, speed limiter, pre-speed limiters, and point of visibility (Kamburjan et al., 2018).</footnote>
### 11.3.3. AISCO

The requirements stipulate co-existence of multiple variants of the same feature, for example, different formats for financial reports. This is not supported in current SPL approaches, including Delta-ABS.

In AISCO-1, implemented in Delta-ABS, interoperability of multiple variants is not supported and this kind of variability is encoded using multiple copies of classes whose inclusion is regulated by the variability model. For example, financial reports may be for expense purposes, for income, or for general reporting. The distinction among these variants is embodied in three different, all classes implementing interface *Entity*. The creation of the classes is managed using deltas. This hampers inter-product code reuse. In the words of the AISCO developers, the disadvantages are that "[...], it cannot be modeled that different product variants from the same product line co-exist and interoperate within one and the same application. This leads to suboptimal code reuse." (Setyautami and Hähnle, 2021, referring to AISCO-1).

In AISCO-2, implemented in Java with the help of an external tool and supporting some aspects of VMs, different report variants are implemented by a VM containing a class *Report*. The variants of this VM correspond to the different classes defined explicitly in AISCO-1. The auxiliary concept of an *Entity* is not needed any longer.

For the ABS-VM model, referenced to as AISCO-3, the main aspects of AISCO-1/AISCO-2 were re-implemented in ABS-VM in 160 LoC: One VM with four features and five deltas for financial reporting. All variants can interoperate within one and the same program generated from the ABS-VM code, instead of relying on an external framework, as in AISCO-2, that is intertwined with the generated program.<fnref n="19" />

*Results.* The AISCO-2 implementation is distributed between Java and external tools that weave interoperable variants together in the desired manner. This approach has two major drawbacks: first, in contrast to AISCO-3, the various sanity, compliance, and type checks discussed in Section 9 cannot be easily realized. Even for a concrete generated program type-safety cannot be fully statically checked, because the VM implementation mechanism of Setyautami and Hähnle (2021) relies on reflection. Second, the distribution of configuration knowledge to different places in the implementation makes maintenance harder and more error-prone than in AISCO-3.

A Java-specific limitation also present in AISCO-2 is the impossibility to remove the implementation (method, class) of a functionality, one can only override it. As the VM concept is based on DOP, this is not an issue for AISCO-3.

The AISCO case study reinforces the experimental evidence that VMs are a suitable concept to simplify heterogeneous applications by modeling variability and co-existence of variants within a single, coherent language.

### 11.4. Results for RQ 2

We discuss the quantitative aspects of the VM refactorings to address **RQ 2**. The AISCO-1 and AISCO-2 models are unsuitable for a quantitative comparison, as AISCO-2 is not written in ABS and AISCO-1 contains external aspects (like frontend routing).

#### 11.4.1. FormbaR

Compared to FormbaR-2, the FormbaR-3 VM version reduces the total number of LoC needed for the signal products from 241 to 180 (–25%). Excluding code required only for variability modeling (configuration knowledge and delta headers), the re-modeled part has 163 LoC (–33%). There are various effects that lead to a reduced number of LoC:

* FormbaR-2 declares one interface and one class per infrastructure kind<fnref n="20" /> In contrast, FormbaR-3 declares a single interface *Specific*, which is then transformed by deltas concurrently with its corresponding class. This reduces the header for interface declarations, in particular, when the interface needs not be changed (for example, the interface for *PoV* contains no methods and is only declared to provide a type). This means that one uses, for example, *Specific with [PoV]* instead of *IPoV*.

* By using deltas, in FormbaR-3 we can share not merely methods (through traits), but also fields. Additionally, using a core class, we can share the *init* block of classes which is common to most classes.

* In FormbaR-3, instead of using trait expressions inside class definitions (with the *uses* declaration Damiani et al., 2017a), we rely on selection of the infrastructure type at the type reference, which is external to the class.

It is worth observing that all these improvements allow more concise modeling *without* changing the underlying class model of ABS, which is specifically designed to simplify deductive verification and static analysis (Hähnle, 2013).

#### 11.4.2. WMMF

The WMMF-3 model has 485 LoC, of which 440 LoC are the two variable modules. The WMMF-2 model has 1322 LoC (+272%), of which 620 LoC are concerned with deltas and variability and 582 are the core product of the modules for memory models and devices. We refrained from reducing code duplication through traits to illustrate that product line systems without native support of interoperable variants can only replicate this behavior through massive code duplication.

If a module has *p* products, then in ABS-VM only *p* configurations are declared, for *any* number of used variants. Another observation is that to connect *n* variants, one needs to declare *p*ⁿ products: one for each combination. Hence, in addition to the additional delta declarations, this blows up the feature model unreasonably.

### 11.5. Results for RQ 3 and RQ 4

#### 11.5.1. Experiments on the FormbaR, WMMF, and AISCO case study
To answer **RQ 3** and **RQ 4**, for each of the models FormbaR-3, WMMF-3, and AISCO-3 (listed in Table 1), we compare:

* The time needed to perform the family-based static normal form, type uniformity,<fnref n="21" /> applicability and pre-typing checks,

* the time needed to perform overall flattening and flattening.<fnref n="22" />

Family-based static checking succeeds for all three models. The results are shown in Table 2 (all times are in seconds). These experiments show for all considered case studies that checking normal form, type uniformity, and applicability is faster than

<footnote n="19">¹⁹ For example, routing of the frontend of the web application is located in the external tool.</footnote>

<footnote n="20">²⁰ One cannot remove the interfaces, because classes are not types in ABS.</footnote>

<footnote n="21">²¹ The time for checking type uniformity includes the time for building the family signature of the program (Definition 22).</footnote>

<footnote n="22">²² Without checking whether the generated program is well typed.</footnote>
### 11.3.3. AISCO

The requirements stipulate co-existence of multiple variants of the same feature, for example, different formats for financial reports. This is not supported in current SPL approaches, including Delta-ABS.

In AISCO-1, implemented in Delta-ABS, interoperability of multiple variants is not supported and this kind of variability is encoded using multiple copies of classes whose inclusion is regulated by the variability model. For example, financial reports may be for expense purposes, for income, or for general reporting. The distinction among these variants is embodied in three different, all classes implementing interface *Entity*. The creation of the classes is managed using deltas. This hampers inter-product code reuse. In the words of the AISCO developers, the disadvantages are that "[...], it cannot be modeled that different product variants from the same product line co-exist and interoperate within one and the same application. This leads to suboptimal code reuse." (Setyautami and Hähnle, 2021, referring to AISCO-1).

In AISCO-2, implemented in Java with the help of an external tool and supporting some aspects of VMs, different report variants are implemented by a VM containing a class *Report*. The variants of this VM correspond to the different classes defined explicitly in AISCO-1. The auxiliary concept of an *Entity* is not needed any longer.

For the ABS-VM model, referenced to as AISCO-3, the main aspects of AISCO-1/AISCO-2 were re-implemented in ABS-VM in 160 LoC: One VM with four features and five deltas for financial reporting. All variants can interoperate within one and the same program generated from the ABS-VM code, instead of relying on an external framework, as in AISCO-2, that is intertwined with the generated program.<fnref n="19" />

*Results.* The AISCO-2 implementation is distributed between Java and external tools that weave interoperable variants together in the desired manner. This approach has two major drawbacks: first, in contrast to AISCO-3, the various sanity, compliance, and type checks discussed in Section 9 cannot be easily realized. Even for a concrete generated program type-safety cannot be fully statically checked, because the VM implementation mechanism of Setyautami and Hähnle (2021) relies on reflection. Second, the distribution of configuration knowledge to different places in the implementation makes maintenance harder and more error-prone than in AISCO-3.

A Java-specific limitation also present in AISCO-2 is the impossibility to remove the implementation (method, class) of a functionality, one can only override it. As the VM concept is based on DOP, this is not an issue for AISCO-3.

The AISCO case study reinforces the experimental evidence that VMs are a suitable concept to simplify heterogeneous applications by modeling variability and co-existence of variants within a single, coherent language.

### 11.4. Results for RQ 2

We discuss the quantitative aspects of the VM refactorings to address **RQ 2**. The AISCO-1 and AISCO-2 models are unsuitable for a quantitative comparison, as AISCO-2 is not written in ABS and AISCO-1 contains external aspects (like frontend routing).

#### 11.4.1. FormbaR

Compared to FormbaR-2, the FormbaR-3 VM version reduces the total number of LoC needed for the signal products from 241 to 180 (–25%). Excluding code required only for variability modeling (configuration knowledge and delta headers), the re-modeled part has 163 LoC (–33%). There are various effects that lead to a reduced number of LoC:

* FormbaR-2 declares one interface and one class per infrastructure kind<fnref n="20" /> In contrast, FormbaR-3 declares a single interface *Specific*, which is then transformed by deltas concurrently with its corresponding class. This reduces the header for interface declarations, in particular, when the interface needs not be changed (for example, the interface for *PoV* contains no methods and is only declared to provide a type). This means that one uses, for example, *Specific with [PoV]* instead of *IPoV*.

* By using deltas, in FormbaR-3 we can share not merely methods (through traits), but also fields. Additionally, using a core class, we can share the *init* block of classes which is common to most classes.

* In FormbaR-3, instead of using trait expressions inside class definitions (with the *uses* declaration Damiani et al., 2017a), we rely on selection of the infrastructure type at the type reference, which is external to the class.

It is worth observing that all these improvements allow more concise modeling *without* changing the underlying class model of ABS, which is specifically designed to simplify deductive verification and static analysis (Hähnle, 2013).

#### 11.4.2. WMMF

The WMMF-3 model has 485 LoC, of which 440 LoC are the two variable modules. The WMMF-2 model has 1322 LoC (+272%), of which 620 LoC are concerned with deltas and variability and 582 are the core product of the modules for memory models and devices. We refrained from reducing code duplication through traits to illustrate that product line systems without native support of interoperable variants can only replicate this behavior through massive code duplication.

If a module has *p* products, then in ABS-VM only *p* configurations are declared, for *any* number of used variants. Another observation is that to connect *n* variants, one needs to declare *p*<sup>n</sup> products: one for each combination. Hence, in addition to the additional delta declarations, this blows up the feature model unreasonably.

### 11.5. Results for RQ 3 and RQ 4

#### 11.5.1. Experiments on the FormbaR, WMMF, and AISCO case study

* The time needed to perform the family-based static normal form, type uniformity,<fnref n="21" /> applicability and pre-typing checks,

* the time needed to perform overall flattening and flattening.<fnref n="22" />

Family-based static checking succeeds for all three models. The results are shown in Table 2 (all times are in seconds). These experiments show for all considered case studies that checking normal form, type uniformity, and applicability is faster than

<footnote n="19">¹⁹ For example, routing of the frontend of the web application is located in the external tool.</footnote>

<footnote n="20">²⁰ One cannot remove the interfaces, because classes are not types in ABS.</footnote>

<footnote n="21">²¹ The time for checking type uniformity includes the time for building the family signature of the program (Definition 22).</footnote>

<footnote n="22">²² Without checking whether the generated program is well typed.</footnote>
<table><caption>**Table 1**
Number of features and variants for each VM in the case studies.</caption><thead><tr><th>Model</th><th>VM</th><th># of features</th><th># of products</th></tr></thead><tbody><tr><td>FormbaR-3</td><td>TrackElements</td><td>5</td><td>5</td></tr><tr><td rowspan="2">WMMF-3</td><td>Mem</td><td>6</td><td>64</td></tr><tr><td>Devices</td><td>8</td><td>255</td></tr><tr><td>AISCO-3</td><td>FinancialReport</td><td>4</td><td>12</td></tr></tbody></table>

<figure><img src="image_11.png" /><figcaption>**Fig. 11.** Results for Synthetic Experiment 2.</figcaption></figure>

performing overall flattening (answering **RQ 3**) and flattening (answering **RQ 4**). Just the time for checking pre-typing is nearly the same as the time for overall flattening in WMMF-3, while it is one other of magnitude higher than the time for overall flattening in FormbaR-3 and AISCO-3, and one order of magnitude higher than the time for flattening in all the three case studies.

### 11.5.2. Experiments on synthetic data sets

To answer **RQ 3** we perform two additional experiments on synthetic data sets (Synthetic Experiment 1 and 2, see Section 11.2.2). The results of Synthetic Experiment 1 are shown in Table 3 (all times are in seconds). Family-based static checks are run on programs with an empty main block, to subtract artifacts from the exponentially growing main block. In Synthetic Experiment 1 overall flattening shows exponential growth and from $n = 8$ onward it is faster to perform the static checks.

Fig. 11 shows the timings for Synthetic Experiment 2: they are nearly constant at, on average, 0.7 s. In both, Synthetic Experiment 1 and 2, the time for applicability checking is nearly constant. We refrain from increasing *n* further in Synthetic Experiment 1, because overall flattening becomes infeasible.

Our synthetic experiments show that applicability checking scales compared to either flattening or overall flattening. In fact, the timings are near constant for our experiments. We conjecture that (i) SAT solving is efficient enough to handle formulas with the resulting number of variables and that (ii) the formulas have a structure that is easy to solve.

## 11.6. Threats to validity

**External validity.** A threat to generalization of our results is that all code used in the case studies has been re-modeled by the authors themselves and consists of only 840 LoC. It should be noted that in two of the three case studies, the non-variable context was not considered (for example, in FormbaR less than 10% of the code was re-modeled). On the other hand, any reasonable product line is bound to have a substantial degree of commonality and there is no point to look at the invariant aspects of an application for the present evaluation.

Another threat is that, while VMs are a general concept for product lines, we only investigated its use for DOP, and only for the ABS language. We consider this to be unproblematic,

because (i) DOP is a fairly general SPL approach that encompasses FOP (Schaefer and Damiani, 2010) and (ii) the ABS implementation of DOP follows general DOP principles (Schaefer and Damiani, 2010) and closely resembles other implementations, such as DOP in Java (Koscielny et al., 2014).

**Internal validity.** A threat concerning our conclusions is that, due to our aim of reusing code from the existing flattening and type checker implementation, we rely on pre-existing code and design choices for both flattening and applicability: we reuse the Choco solver part of the ABS compiler and do not optimize the flattening mechanisms.

Another threat is that the applicability checks take constant time due to the design of our examples. We mitigated this by using random feature models to exclude artifacts stemming from the structure of the feature model.

# 12. Related work

We focus on the approaches most relevant and closest to the VM concept. We refer to Apel et al. (2013) for a systematic introduction to feature-oriented SPLs, to Schaefer et al. (2012) for an overview of diverse system developments, to Thüm et al. (2014) for a classification and survey of analysis strategies for SPLs, and to Holl et al. (2012) for a systematic and expert survey on capabilities supporting MPLs.

## 12.1. Programming constructs for MPLs and variant interoperability

Schröter et al. (2013a) advocate the use of suitable interfaces to support compositional analysis of MPLs, consisting of FOP SPLs of Java programs, during different stages of the development process. Damiani et al. (2014b) informally outlined an extension of DOP to implement MPLs of Java programs by proposing linguistic constructs for defining an MPL as an SPL that imports other SPLs. In their proposal the feature model and artifact base of the importing SPL is entwined with the feature models and artifact bases of the imported SPLs. Therefore, in contrast to VM, the proposal does not support encapsulation at SPL level. More recently, Damiani et al. (2019) formalized an extension of DOP to implement MPLs in terms of a core calculus where products are written in an imperative version of Featherweight Java (Igarashi et al., 1999, 2001). Their idea is to lift to the SPL level the use of dependent feature models to capture MPLs, as advocated by Schröter et al. (2016, 2013b). Like the earlier paper (Damiani et al., 2014b), the SPL construct proposed by Damiani et al. (2019) models dependencies among different SPLs at the feature model level: to use two (or more) SPLs together, one must compose their feature models. In contrast, the VM concept does not require feature model composition.

None of the proposals mentioned above support variant interoperability (Damiani et al., 2018b). Setyautami et al. (2018) address variant interoperability at the level of static UML class diagrams. In this paper we consider executable Java-like code.

Variant interoperability in terms of ABS code is addressed in our previous work (Damiani et al., 2018b), where we consider a set of product lines, each comprising a set of modules. However, in that proposal, encapsulation is not realized by mechanisms at the module level (as in VMs): unique declarations are supported (unsatisfactorily) by common modules (which is not fine-grained enough), and the concepts of modularity (through modules) and variability (through product lines) are intertwined. In contrast, the VM concept proposed in this paper unifies modules and product lines by adding the capability to model variability directly to modules: each module is a product line, each product line is a module. This drastically simplifies the language, yet allows more far-reaching reuse of the DOP mechanism natively supported by ABS. Furthermore, VMs ease the cognitive burden of variability modeling, extending a common module framework, instead of adding another layer on top.
<table><caption>**Table 1**
Number of features and variants for each VM in the case studies.</caption><thead><tr><th>Model</th><th>VM</th><th># of features</th><th># of products</th></tr></thead><tbody><tr><td>FormbaR-3</td><td>TrackElements</td><td>5</td><td>5</td></tr><tr><td rowspan="2">WMMF-3</td><td>Mem</td><td>6</td><td>64</td></tr><tr><td>Devices</td><td>8</td><td>255</td></tr><tr><td>AISCO-3</td><td>FinancialReport</td><td>4</td><td>12</td></tr></tbody></table>

<figure><img src="image_10.png" /><figcaption>**Fig. 11.** Results for Synthetic Experiment 2.</figcaption></figure>

performing overall flattening (answering **RQ 3**) and flattening (answering **RQ 4**). Just the time for checking pre-typing is nearly the same as the time for overall flattening in WMMF-3, while it is one other of magnitude higher than the time for overall flattening in FormbaR-3 and AISCO-3, and one order of magnitude higher than the time for flattening in all the three case studies.

### 11.5.2. Experiments on synthetic data sets

To answer **RQ 3** we perform two additional experiments on synthetic data sets (Synthetic Experiment 1 and 2, see Section 11.2.2). The results of Synthetic Experiment 1 are shown in Table 3 (all times are in seconds). Family-based static checks are run on programs with an empty main block, to subtract artifacts from the exponentially growing main block. In Synthetic Experiment 1 overall flattening shows exponential growth and from $n = 8$ onward it is faster to perform the static checks.

Fig. 11 shows the timings for Synthetic Experiment 2: they are nearly constant at, on average, 0.7 s. In both, Synthetic Experiment 1 and 2, the time for applicability checking is nearly constant. We refrain from increasing *n* further in Synthetic Experiment 1, because overall flattening becomes infeasible.

Our synthetic experiments show that applicability checking scales compared to either flattening or overall flattening. In fact, the timings are near constant for our experiments. We conjecture that (i) SAT solving is efficient enough to handle formulas with the resulting number of variables and that (ii) the formulas have a structure that is easy to solve.

## 11.6. Threats to validity

**External validity.** A threat to generalization of our results is that all code used in the case studies has been re-modeled by the authors themselves and consists of only 840 LoC. It should be noted that in two of the three case studies, the non-variable context was not considered (for example, in FormbaR less than 10% of the code was re-modeled). On the other hand, any reasonable product line is bound to have a substantial degree of commonality and there is no point to look at the invariant aspects of an application for the present evaluation.

Another threat is that, while VMs are a general concept for product lines, we only investigated its use for DOP, and only for the ABS language. We consider this to be unproblematic,

because (i) DOP is a fairly general SPL approach that encompasses FOP (Schaefer and Damiani, 2010) and (ii) the ABS implementation of DOP follows general DOP principles (Schaefer and Damiani, 2010) and closely resembles other implementations, such as DOP in Java (Koscielny et al., 2014).

**Internal validity.** A threat concerning our conclusions is that, due to our aim of reusing code from the existing flattening and type checker implementation, we rely on pre-existing code and design choices for both flattening and applicability: we reuse the Choco solver part of the ABS compiler and do not optimize the flattening mechanisms.

Another threat is that the applicability checks take constant time due to the design of our examples. We mitigated this by using random feature models to exclude artifacts stemming from the structure of the feature model.

# 12. Related work

We focus on the approaches most relevant and closest to the VM concept. We refer to Apel et al. (2013) for a systematic introduction to feature-oriented SPLs, to Schaefer et al. (2012) for an overview of diverse system developments, to Thüm et al. (2014) for a classification and survey of analysis strategies for SPLs, and to Holl et al. (2012) for a systematic and expert survey on capabilities supporting MPLs.

## 12.1. Programming constructs for MPLs and variant interoperability

Schröter et al. (2013a) advocate the use of suitable interfaces to support compositional analysis of MPLs, consisting of FOP SPLs of Java programs, during different stages of the development process. Damiani et al. (2014b) informally outlined an extension of DOP to implement MPLs of Java programs by proposing linguistic constructs for defining an MPL as an SPL that imports other SPLs. In their proposal the feature model and artifact base of the importing SPL is entwined with the feature models and artifact bases of the imported SPLs. Therefore, in contrast to VM, the proposal does not support encapsulation at SPL level. More recently, Damiani et al. (2019) formalized an extension of DOP to implement MPLs in terms of a core calculus where products are written in an imperative version of Featherweight Java (Igarashi et al., 1999, 2001). Their idea is to lift to the SPL level the use of dependent feature models to capture MPLs, as advocated by Schröter et al. (2016, 2013b). Like the earlier paper (Damiani et al., 2014b), the SPL construct proposed by Damiani et al. (2019) models dependencies among different SPLs at the feature model level: to use two (or more) SPLs together, one must compose their feature models. In contrast, the VM concept does not require feature model composition.

None of the proposals mentioned above support variant interoperability (Damiani et al., 2018b). Setyautami et al. (2018) address variant interoperability at the level of static UML class diagrams. In this paper we consider executable Java-like code.

Variant interoperability in terms of ABS code is addressed in our previous work (Damiani et al., 2018b), where we consider a set of product lines, each comprising a set of modules. However, in that proposal, encapsulation is not realized by mechanisms at the module level (as in VMs): unique declarations are supported (unsatisfactorily) by common modules (which is not fine-grained enough), and the concepts of modularity (through modules) and variability (through product lines) are intertwined. In contrast, the VM concept proposed in this paper unifies modules and product lines by adding the capability to model variability directly to modules: each module is a product line, each product line is a module. This drastically simplifies the language, yet allows more far-reaching reuse of the DOP mechanism natively supported by ABS. Furthermore, VMs ease the cognitive burden of variability modeling, extending a common module framework, instead of adding another layer on top.
<table><caption>**Table 2**
Results for the experiments in the case studies.</caption><thead><tr><th rowspan="2">Model</th><th colspan="3">Family-based static checking</th><th rowspan="2">Overall flattening</th><th rowspan="2">Flattening</th></tr><tr><th>Normal form + type uniformity</th><th>Applicability</th><th>Pre-typing</th></tr></thead><tbody><tr><td>FormbaR-3</td><td>&lt;0.01</td><td>&lt;0.01</td><td>0.2</td><td>0.03</td><td>0.02</td></tr><tr><td>WMMF-3</td><td>&lt;0.01</td><td>&lt;0.01</td><td>0.9</td><td>1.1</td><td>0.05</td></tr><tr><td>AISCO-3</td><td>&lt;0.01</td><td>&lt;0.01</td><td>0.3</td><td>0.08</td><td>0.03</td></tr></tbody></table>

<table><caption>**Table 3**
Results for synthetic Experiment 1. Comparison of family-based static checking with overall flattening (times in seconds). Relative change is computed as $\frac{\text{total time for static checking}}{\text{time for overall flattening}}$.</caption><thead><tr><th rowspan="2"># of features</th><th colspan="3">Family-based static checking</th><th rowspan="2">Overall flattening</th><th rowspan="2">Relative change</th></tr><tr><th>Normal form + type uniformity</th><th>Applicability</th><th>Pre-typing</th></tr></thead><tbody><tr><td>7</td><td>&lt;0.01</td><td>0.05</td><td>0.07</td><td>0.07</td><td>41%</td></tr><tr><td>8</td><td>&lt;0.01</td><td>0.05</td><td>0.08</td><td>0.20</td><td>-54%</td></tr><tr><td>9</td><td>&lt;0.01</td><td>0.05</td><td>0.10</td><td>0.49</td><td>-227%</td></tr><tr><td>10</td><td>&lt;0.01</td><td>0.06</td><td>0.08</td><td>1.63</td><td>-1064%</td></tr><tr><td>11</td><td>&lt;0.01</td><td>0.09</td><td>0.09</td><td>5.44</td><td>-2922%</td></tr><tr><td>12</td><td>&lt;0.01</td><td>0.08</td><td>0.11</td><td>27.27</td><td>-14252%</td></tr></tbody></table>

## 12.2. Family-based checking for SPLs of java-like programs

According to Thüm et al. (2014), the approaches to the analysis of SPLs can be classified into three main categories: *product-based analyses*, which operate only on generated variants (or models of variants); *family-based analyses*, which operate only on the artifact base by exploiting the feature model and configuration knowledge to obtain results about all variants; and *feature-based analyses*, which operate on the building blocks of the different variants (feature modules in FOP and deltas in DOP) in isolation (without using the feature model and configuration knowledge) to derive results on all variants. We refer to Thüm et al. (2014) for a survey on SPL type checking. Here we review type checking approaches for FOP and DOP that are close to our proposal.

Thaker et al. (2007) informally illustrate the implementation of a family-based type checking for the AHEAD system (Batory et al., 2004). It comprises: (i) A family-feature-based step that computes for each class a stub (according to the terminology used in Section 9.1, these stubs represent a type uniform signature for the SPL) and compiles each feature module in the context of all stubs (thus performing checks corresponding to type uniformity and partial typing in our terminology) and (ii) a family-based step that infers a set of constraints that are combined with the feature model to generate a formula (modeling applicability and dependency) whose satisfiability should imply that all variants can be generated and successfully compile.

Delaware et al. (2009) formalize feature-family-based type checking for the Lightweight Feature Java (LFJ) calculus, which models FOP for the Lightweight Java (LJ) calculus by Strniša et al. (2007). It comprises: (i) A feature-based step that uses a constraint-based type system for LFJ to analyze each feature module in isolation and infer a set of constraints for each feature module and (ii) a family-based step where the feature model and the inferred constraints are used to generate a formula whose satisfiability implies that all variants can be generated and type check.

Bettini et al. (2013a) proposed a type checking approach for DOP. It comprises: (i) A feature-based analysis that uses a constraint-based type system for IFJ (a core calculus formalizing DOP for SPLs of Featherweight Java programs) to infer a type abstraction for each delta and (ii) a product-based step that uses these type abstractions to generate, for each product of the SPL, a type abstraction (of the associated variant) that is checked to establish whether the associated variant type checks. This approach has been enhanced by introducing a family-based step that builds a product family generation tree which is then

traversed in order to perform optimized generation and check of type abstractions of all variants (Damiani and Schaefer, 2012), and has been partially implemented in a branch of the ABS tool chain (Damiani et al., 2017b).

Damiani and Lienhardt (2016) formalize, by means of IFJ, a feature-family-based type checking approach for DOP inspired by the approach for FOP by Thaker et al. (2007) and Delaware et al. (2009). It enforces type uniformity and comprises partial typing, applicability analysis and dependency analysis. Being feature-family-based, it represents an improvement over the previous type checking approaches for DOP, because it does not require to iterate over the set of all products. The family-based checks presented in this paper extend to ABS-VM the corresponding family-based type checks for IFJ (Damiani and Lienhardt, 2016).

## 12.3. Variability-aware module systems

Kästner et al. (2012b) propose a variability-aware module system (called VAMS in the following). Like in our proposal, each VAMS module is an SPL, however, VAMS and the VM concept differ fundamentally:

* VAMS is defined on top of the procedural system programming language C and the annotative approach (see Section 3) to SPL implementation (C, through its preprocessor directives #define and #ifdef, has built-in support for annotative SPLs).

* VMs are defined on top of the object-oriented modeling language ABS and the transformational (specifically, delta-oriented) approach to SPL implementation (ABS has built-in support for delta-oriented SPLs).

Due to this difference, also the design of VAMS and VM programs differs fundamentally. Therefore, it is not meaningful to compare both approaches directly in terms of examples and concrete case studies. Instead, we present a detailed comparison, where we focus on the four most important conceptual differences between the two approaches.

(i) VAMS does not encapsulate variability (Section 6): Modules import function declarations without specifying the modules from which they should be imported. To generate a variant VAMS requires the user to write a composition expression, which lists all modules to be composed and resolves dependencies and ambiguities (such as when a module imports a function that is defined in two different modules) by specifying how functions are renamed or hidden (and how features are renamed, selected or deselected). Hence,
<table><caption>**Table 2**
Results for the experiments in the case studies.</caption><thead><tr><th rowspan="2">Model</th><th colspan="3">Family-based static checking</th><th rowspan="2">Overall flattening</th><th rowspan="2">Flattening</th></tr><tr><th>Normal form + type uniformity</th><th>Applicability</th><th>Pre-typing</th></tr></thead><tbody><tr><td>FormbaR-3</td><td>&lt;0.01</td><td>&lt;0.01</td><td>0.2</td><td>0.03</td><td>0.02</td></tr><tr><td>WMMF-3</td><td>&lt;0.01</td><td>&lt;0.01</td><td>0.9</td><td>1.1</td><td>0.05</td></tr><tr><td>AISCO-3</td><td>&lt;0.01</td><td>&lt;0.01</td><td>0.3</td><td>0.08</td><td>0.03</td></tr></tbody></table>

<table><caption>**Table 3**
Results for synthetic Experiment 1. Comparison of family-based static checking with overall flattening (times in seconds). Relative change is computed as $\frac{\text{total time for static checking}}{\text{time for overall flattening}}$.</caption><thead><tr><th rowspan="2"># of features</th><th colspan="3">Family-based static checking</th><th rowspan="2">Overall flattening</th><th rowspan="2">Relative change</th></tr><tr><th>Normal form + type uniformity</th><th>Applicability</th><th>Pre-typing</th></tr></thead><tbody><tr><td>7</td><td>&lt;0.01</td><td>0.05</td><td>0.07</td><td>0.07</td><td>41%</td></tr><tr><td>8</td><td>&lt;0.01</td><td>0.05</td><td>0.08</td><td>0.20</td><td>-54%</td></tr><tr><td>9</td><td>&lt;0.01</td><td>0.05</td><td>0.10</td><td>0.49</td><td>-227%</td></tr><tr><td>10</td><td>&lt;0.01</td><td>0.06</td><td>0.08</td><td>1.63</td><td>-1064%</td></tr><tr><td>11</td><td>&lt;0.01</td><td>0.09</td><td>0.09</td><td>5.44</td><td>-2922%</td></tr><tr><td>12</td><td>&lt;0.01</td><td>0.08</td><td>0.11</td><td>27.27</td><td>-14252%</td></tr></tbody></table>

## 12.2. Family-based checking for SPLs of java-like programs

According to Thüm et al. (2014), the approaches to the analysis of SPLs can be classified into three main categories: product-based analyses, which operate only on generated variants (or models of variants); family-based analyses, which operate only on the artifact base by exploiting the feature model and configuration knowledge to obtain results about all variants; and feature-based analyses, which operate on the building blocks of the different variants (feature modules in FOP and deltas in DOP) in isolation (without using the feature model and configuration knowledge) to derive results on all variants. We refer to Thüm et al. (2014) for a survey on SPL type checking. Here we review type checking approaches for FOP and DOP that are close to our proposal.

Thaker et al. (2007) informally illustrate the implementation of a family-based type checking for the AHEAD system (Batory et al., 2004). It comprises: (i) A family-feature-based step that computes for each class a stub (according to the terminology used in Section 9.1, these stubs represent a type uniform signature for the SPL) and compiles each feature module in the context of all stubs (thus performing checks corresponding to type uniformity and partial typing in our terminology) and (ii) a family-based step that infers a set of constraints that are combined with the feature model to generate a formula (modeling applicability and dependency) whose satisfiability should imply that all variants can be generated and successfully compile.

Delaware et al. (2009) formalize feature-family-based type checking for the Lightweight Feature Java (LFJ) calculus, which models FOP for the Lightweight Java (LJ) calculus by Strniša et al. (2007). It comprises: (i) A feature-based step that uses a constraint-based type system for LFJ to analyze each feature module in isolation and infer a set of constraints for each feature module and (ii) a family-based step where the feature model and the inferred constraints are used to generate a formula whose satisfiability implies that all variants can be generated and type check.

Bettini et al. (2013a) proposed a type checking approach for DOP. It comprises: (i) A feature-based analysis that uses a constraint-based type system for IFJ (a core calculus formalizing DOP for SPLs of Featherweight Java programs) to infer a type abstraction for each delta and (ii) a product-based step that uses these type abstractions to generate, for each product of the SPL, a type abstraction (of the associated variant) that is checked to establish whether the associated variant type checks. This approach has been enhanced by introducing a family-based step that builds a product family generation tree which is then

traversed in order to perform optimized generation and check of type abstractions of all variants (Damiani and Schaefer, 2012), and has been partially implemented in a branch of the ABS tool chain (Damiani et al., 2017b).

Damiani and Lienhardt (2016) formalize, by means of IFJ, a feature-family-based type checking approach for DOP inspired by the approach for FOP by Thaker et al. (2007) and Delaware et al. (2009). It enforces type uniformity and comprises partial typing, applicability analysis and dependency analysis. Being feature-family-based, it represents an improvement over the previous type checking approaches for DOP, because it does not require to iterate over the set of all products. The family-based checks presented in this paper extend to ABS-VM the corresponding family-based type checks for IFJ (Damiani and Lienhardt, 2016).

## 12.3. Variability-aware module systems

Kästner et al. (2012b) propose a variability-aware module system (called VAMS in the following). Like in our proposal, each VAMS module is an SPL, however, VAMS and the VM concept differ fundamentally:

* VAMS is defined on top of the procedural system programming language C and the annotative approach (see Section 3) to SPL implementation (C, through its preprocessor directives #define and #ifdef, has built-in support for annotative SPLs).

* VMs are defined on top of the object-oriented modeling language ABS and the transformational (specifically, delta-oriented) approach to SPL implementation (ABS has built-in support for delta-oriented SPLs).

Due to this difference, also the design of VAMS and VM programs differs fundamentally. Therefore, it is not meaningful to compare both approaches directly in terms of examples and concrete case studies. Instead, we present a detailed comparison, where we focus on the four most important conceptual differences between the two approaches.

(i) VAMS does not encapsulate variability (Section 6): Modules import function declarations without specifying the modules from which they should be imported. To generate a variant VAMS requires the user to write a composition expression, which lists all modules to be composed and resolves dependencies and ambiguities (such as when a module imports a function that is defined in two different modules) by specifying how functions are renamed or hidden (and how features are renamed, selected or deselected). Hence,
VAMS is not concerned with explicit dependencies between
modules, which are crucial to usability and central to the
PEV introduced in this work. By exploiting PEV, the VM con-
cept achieves simplicity: configuring a single VM M triggers
automatic generation of all required variants of M and other
VMs.

(ii) The design of VAMS does not target variant interoperability (Kästner et al. (2012b) do not mention this issue). Making two variants of the same module co-exist, requires to create a copy of the module and to rename (possibly by using the module composition language provided in VAMS) all its features and all its exported functions. In contrast, providing usable support to variant interoperability is a central design goal of VM.

(iii) Variability in VAMS is achieved explicitly by using an annotative approach: code elements (import/export declarations and function declarations) are annotated with presence conditions (propositional formulas over features). In VM variability is achieved explicitly by DOP for class/interface declarations and implicitly for export/import declarations.

(iv) VAMS is formalized by building on a calculus in the spirit of Cardelli's module system formalization (Cardelli, 1997) for procedural programming languages, where a module consists of a set of imported typed function declarations and a list of typed function definitions, and is implemented as a module system for C code. Therefore, VAMS is tailored to procedural languages, where the interface of each module describes names and types of imported and exported functions, and there is a global function name space. Moreover, even though each module has its own feature model, there is a global feature name space. In contrast, the VM concept targets Java-like languages, it is based on the module system of ABS (Hähnle, 2013; Johnsen et al., 2010) (a fairly standard module system close to Java and Haskell), and implemented as an extension of the ABS module system. Each VM has a local name space (which reduces overhead), also features are local to VMs.

12.4. *Variability modules in java*

Setyautami and Hähnle (2021) suggest that the VM concept
can be implemented on top of any Java-like language with modest
effort. The solution presented there takes a different approach
from the present account: it dispenses with explicit language
constructs to model variability, but uses only standard Java con-
structs. This is achieved with an architectural pattern: delta appli-
cation is realized by decorators, the name space is managed with
abstract factories, and each product is a module declaration in
itself. The sole reliance on standard Java constructs comes with
limitations: unique class/interface declarations are not directly
supported (but can be achieved by suitable **final** annotations).
In consequence, the PEV is not enforced. Open product declara-
tions are not supported. Unsoundness of a product might only
be detected at runtime, because reflection is used for module
name resolution instead of flattening. Therefore, Setyautami and
Hähnle (2021) does not feature a formal semantics of VM and
family-based checking.

13. Conclusion and future work

This article introduced variability modules, a novel approach
to implement MPLs consisting of DOP SPLs of Java-like programs,
where different, possibly interdependent, variants of the same
SPL can co-exist and interoperate.

Central to the design of VM are simplicity and usability,
specifically the PEV that makes dependencies on variants explicit,

so that a simple Java- or Haskell-like module concept is sufficient.

We formalized the syntax and semantics of variability mod-
ules as an extension of the ABS language called ABS-VM. The
semantics is given in terms of flattening rules that transform an
ABS-VM program into a set of ABS modules. This made it possible
to implement an ABS-VM compiler as a front-end to the ABS tool
chain.

In addition to compilation, we defined and implemented PEV-
compliance, type uniformity, pre-typing and applicability consis-
tency as family-based checks for ABS-VM programs.

We evaluated the VM concept and our implementation of it
quantitatively and qualitatively by case studies that were partly
taken from industrial code used in production.

We are currently formalizing and implementing an extended
analysis called dependence consistency checking: it aims to fully
support family-based checking of type-safety (see the discussion
at the beginning of Section 9). The extended tool chain will be
subjected to validation by novel and even larger case studies.

Declaration of competing interest

The authors declare that they have no known competing finan-
cial interests or personal relationships that could have appeared
to influence the work reported in this paper.

Data availability

Code linked from article.

Acknowledgments

We thank the anonymous SPLC 2021 and the JSS reviewers for
insightful comments and suggestions that helped to improve this
paper. This work was partially supported by the Research Council
of Norway via SIRIUS (237898) and PeTWIN (294600).

**Appendix A. Rules for delta application**

We present the rules describing the application of an ordered
sequence of deltas DIT to a sequence of interface/class defini-
tions Defn. The rules, given in Fig. A.12, fall into the following
categories:

* Rules for a Sequence of Deltas describe how to apply each of the deltas in a sequence. D:EMPTY removes the delta if no operations are left to execute. Rules D:INTER and D:CLASS extract the first interface/class operation from the delta and apply it to the list of definitions. D:END concludes the application process when the sequence of the deltas to be applied is empty.

* Rules for a Delta describe how to apply the actions specified by a delta to a whole class or interface definition. Rule D:ADDSI adds an interface by adding its definition to the list of definitions. Rule D:REMSI removes an interface by looking up its definition using the name from the delta modifier. The rules for classes, D:ADDS and D:REMSC are analogous. Rules D:MODI and D:MODC modify an interface or class by applying the rules for interface modifiers (or class modifiers).

* Rules for Extends/Implements Clauses modify the *extends* clauses of interfaces and *implements* clauses of classes by removing (D:EM:REMS) or adding (D:EM:ADDS) an interface name. Rule D:EM:EMPTY is triggered when all modifications of the clause were applied.
VAMS is not concerned with explicit dependencies between
modules, which are crucial to usability and central to the
PEV introduced in this work. By exploiting PEV, the VM con-
cept achieves simplicity: configuring a single VM M triggers
automatic generation of all required variants of M and other
VMs.

(ii) The design of VAMS does not target variant interoperability (Kästner et al. (2012b) do not mention this issue). Making two variants of the same module co-exist, requires to create a copy of the module and to rename (possibly by using the module composition language provided in VAMS) all its features and all its exported functions. In contrast, providing usable support to variant interoperability is a central design goal of VM.

(iii) Variability in VAMS is achieved explicitly by using an annotative approach: code elements (import/export declarations and function declarations) are annotated with presence conditions (propositional formulas over features). In VM variability is achieved explicitly by DOP for class/interface declarations and implicitly for export/import declarations.

(iv) VAMS is formalized by building on a calculus in the spirit of Cardelli's module system formalization (Cardelli, 1997) for procedural programming languages, where a module consists of a set of imported typed function declarations and a list of typed function definitions, and is implemented as a module system for C code. Therefore, VAMS is tailored to procedural languages, where the interface of each module describes names and types of imported and exported functions, and there is a global function name space. Moreover, even though each module has its own feature model, there is a global feature name space. In contrast, the VM concept targets Java-like languages, it is based on the module system of ABS (Hähnle, 2013; Johnsen et al., 2010) (a fairly standard module system close to Java and Haskell), and implemented as an extension of the ABS module system. Each VM has a local name space (which reduces overhead), also features are local to VMs.

12.4. *Variability modules in java*

Setyautami and Hähnle (2021) suggest that the VM concept
can be implemented on top of any Java-like language with modest
effort. The solution presented there takes a different approach
from the present account: it dispenses with explicit language
constructs to model variability, but uses only standard Java con-
structs. This is achieved with an architectural pattern: delta appli-
cation is realized by decorators, the name space is managed with
abstract factories, and each product is a module declaration in
itself. The sole reliance on standard Java constructs comes with
limitations: unique class/interface declarations are not directly
supported (but can be achieved by suitable **final** annotations).
In consequence, the PEV is not enforced. Open product declara-
tions are not supported. Unsoundness of a product might only
be detected at runtime, because reflection is used for module
name resolution instead of flattening. Therefore, Setyautami and
Hähnle (2021) does not feature a formal semantics of VM and
family-based checking.

13. Conclusion and future work

This article introduced variability modules, a novel approach
to implement MPLs consisting of DOP SPLs of Java-like programs,
where different, possibly interdependent, variants of the same
SPL can co-exist and interoperate.

Central to the design of VM are simplicity and usability,
specifically the PEV that makes dependencies on variants explicit,

so that a simple Java- or Haskell-like module concept is sufficient.

We formalized the syntax and semantics of variability mod-
ules as an extension of the ABS language called ABS-VM. The
semantics is given in terms of flattening rules that transform an
ABS-VM program into a set of ABS modules. This made it possible
to implement an ABS-VM compiler as a front-end to the ABS tool
chain.

In addition to compilation, we defined and implemented PEV-
compliance, type uniformity, pre-typing and applicability consis-
tency as family-based checks for ABS-VM programs.

We evaluated the VM concept and our implementation of it
quantitatively and qualitatively by case studies that were partly
taken from industrial code used in production.

We are currently formalizing and implementing an extended
analysis called dependence consistency checking: it aims to fully
support family-based checking of type-safety (see the discussion
at the beginning of Section 9). The extended tool chain will be
subjected to validation by novel and even larger case studies.

Declaration of competing interest

The authors declare that they have no known competing finan-
cial interests or personal relationships that could have appeared
to influence the work reported in this paper.

Data availability

Code linked from article.

Acknowledgments

We thank the anonymous SPLC 2021 and the JSS reviewers for
insightful comments and suggestions that helped to improve this
paper. This work was partially supported by the Research Council
of Norway via SIRIUS (237898) and PeTWIN (294600).

**Appendix A. Rules for delta application**

We present the rules describing the application of an ordered
sequence of deltas DIT to a sequence of interface/class defini-
tions Defn. The rules, given in Fig. A.12, fall into the following
categories:

* Rules for a Sequence of Deltas describe how to apply each of the deltas in a sequence. D:EMPTY removes the delta if no operations are left to execute. Rules D:INTER and D:CLASS extract the first interface/class operation from the delta and apply it to the list of definitions. D:END concludes the application process when the sequence of the deltas to be applied is empty.

* Rules for a Delta describe how to apply the actions specified by a delta to a whole class or interface definition. Rule D:ADDSI adds an interface by adding its definition to the list of definitions. Rule D:REMSI removes an interface by looking up its definition using the name from the delta modifier. The rules for classes, D:ADDS and D:REMSC are analogous. Rules D:MODI and D:MODC modify an interface or class by applying the rules for interface modifiers (or class modifiers).

* Rules for Extends/Implements Clauses modify the *extends* clauses of interfaces and *implements* clauses of classes by removing (D:EM:REMS) or adding (D:EM:ADDS) an interface name. Rule D:EM:EMPTY is triggered when all modifications of the clause were applied.
## Rules for a Sequence of Deltas

D:EMPTY
 delta D; Dlt, Defn) → ( Dlt, Defn)

D:END
 (ε, Defn) → Defn

D:CLASS
 (delta D; CO CO IO Dlt, Defn) → (delta D; CO IO Dlt, ((D;CO) • Defn)

D:INTER
 (delta D; IO IO Dlt, Defn) → (delta D; IO Dlt, (D;IO) • Defn)

## Rules for a Delta

D:ADDSI
 name(ID) ⊈ name( Defn)
 (D; adds ID) • Defn → ID Defn

D:REMSI
 name(ID) = I
 (D; removes I) • (ID Defn) → Defn

D:MODSI
 (D; modifies interface I EM { HO }) • (interface I extends IR { MH } Defn)
 → (interface I extends (EM • IR) { HO • MH } Defn)

D:ADDSC
 name(CD) ⊈ name( Defn)
 (D; adds CD) • Defn → CD Defn

D:REMSC
 name(CD) = C
 (D; removes C) • (CD Defn) → Defn

D:MODSC
 (D; modifies class C EM { AO }) • (class C implements IR { FD MD } Defn)
 → (class C implements (EM • IR) { (D;AO) • ( FD MD ) } Defn)

## Rules for Extends/Implements Clauses

D:EM:EMPTY
 ε • IR → IR
 D:EM:ADDS
 (adds IR' EM) • IR → EM • ( IR IR' )

D:EM:REMS
 (removes IR) • ( IR' ) → IR' \ IR

## Rules for Interfaces

D:I:EMPTY
 ε • MH → MH
 D:I:ADDS
 name(MH) ⊈ name( MH )
 (adds MH HO) • MH → HO • (MH MH)

D:I:REMS
 (removes MH HO) • (MH MH) → HO • MH

## Rules for Classes

D:C:EMPTY
 ε • ( FD MD ) → FD MD
 D:C:ADDSF
 name(FD) ⊈ name( FD )
 (D;adds FD AO) • ( FD MD ) → (D; AO) • ( FD FD MD )

D:C:ADDSM
 name(MD) ⊈ name( MD )
 (D; adds MD AO ) • ( FD MD ) → (D; AO • ( FD MD MD )

D:C:REMSF
 (removes FD AO ) • ( FD FD MD ) → (D; AO) • ( FD MD )

D:C:REMSM
 (D; removes MH AO ) • ( FD MH { S return E;} MD ) → (D;) AO ) • ( FD MD )

D:C:MODS
 name(MH) = name(MH') = m S'' = S [Dm /original]
 E'' = E [Dm /original] MH'' = MH' [Dm /m]
 (D; modifies MH { S return E;} AO ) • ( FD MH' { S' return E';} MD )
 → (D; AO ) • ( FD MH { S'' return E'';} MH'' { S' return E';} MD )

<caption>Fig. A.12. Delta application rules.</caption>

* Rules for Interfaces modify interfaces. Rule D:I:EMPTY is applicable when no further modification is requested on the given interface, so that the result is the interface itself. Rule D:I:ADDS adds the specified method header to the interface (provided no header with this name is already present). Rule D:I:REMS removes an existing method header from the interface.

* Rules for Classes modify classes. They are very similar to the ones for interfaces, with two exceptions: first, manipulation

of method headers is replaced by manipulation of fields (rules D:C:ADDSF and D:C:REMSF) and method implementations (rules D:C:ADDSM and D:C:REMSM). Second, methods may be modified using rule D:C:MODS. This rule replaces the method implementation, but keeps the old implementation with a fresh name. If the new implementation contains an original statement, then this statement is replaced by a call to the old implementation.
## Rules for a Sequence of Deltas

D:EMPTY
 delta D; Dlt, Defn) → ( Dlt, Defn)

D:END
 (ε, Defn) → Defn

D:CLASS
 (delta D; CO CO IO Dlt, Defn) → (delta D; CO IO Dlt, ((D;CO) • Defn)

D:INTER
 (delta D; IO IO Dlt, Defn) → (delta D; IO Dlt, (D;IO) • Defn)

## Rules for a Delta

D:ADDSI
 name(ID) ⊈ name( Defn)
 (D; adds ID) • Defn → ID Defn

D:REMSI
 name(ID) = I
 (D; removes I) • (ID Defn) → Defn

D:MODSII
 (D; modifies interface I EM { HO }) • (interface I extends IR { MH } Defn)
 → (interface I extends (EM • IR) { HO • MH } Defn)

D:ADDSC
 name(CD) ⊈ name( Defn)
 (D; adds CD) • Defn → CD Defn

D:REMSC
 name(CD) = C
 (D; removes C) • (CD Defn) → Defn

D:MODSC
 (D; modifies class C EM { AO }) • (class C implements IR { FD MD } Defn)
 → (class C implements (EM • IR) { (D;AO) • ( FD MD ) } Defn)

## Rules for Extends/Implements Clauses

D:EM:EMPTY
 ε • IR → IR
 D:EM:ADDS
 (adds IR' EM) • IR → EM • ( IR IR' )

D:EM:REMS
 (removes IR) • ( IR' ) → IR' \ IR

## Rules for Interfaces

D:I:EMPTY
 ε • MH → MH
 D:I:ADDS
 name(MH) ⊈ name( MH )
 (adds MH HO) • MH → HO • (MH MH)

D:I:REMS
 (removes MH HO) • (MH MH) → HO • MH

## Rules for Classes

D:C:EMPTY
 ε • ( FD MD ) → FD MD
 D:C:ADDSF
 name(FD) ⊈ name( FD )
 (D;adds FD AO) • ( FD MD ) → (D; AO) • ( FD FD MD )

D:C:ADDSM
 name(MD) ⊈ name( MD )
 (D; adds MD AO ) • ( FD MD ) → (D; AO • ( FD MD MD )

D:C:REMSF
 (removes FD AO ) • ( FD FD MD ) → (D; AO ) • ( FD MD )

D:C:REMSM
 (D; removes MH AO ) • ( FD MH { S return E;} MD ) → (D;) AO ) • ( FD MD )

D:C:MODS
 name(MH) = name(MH') = m S'' = S [Dm /original]
 E'' = E [Dm /original] MH'' = MH' [Dm /m]
 (D; modifies MH { S return E;} AO ) • ( FD MH' { S' return E';} MD )
 → (D; AO ) • ( FD MH { S'' return E'';} MH'' { S' return E';} MD )

<caption>Fig. A.12. Delta application rules.</caption>

* Rules for Interfaces modify interfaces. Rule D:I:EMPTY is applicable when no further modification is requested on the given interface, so that the result is the interface itself. Rule D:I:ADDS adds the specified method header to the interface (provided no header with this name is already present). Rule D:I:REMS removes an existing method header from the interface.

* Rules for Classes modify classes. They are very similar to the ones for interfaces, with two exceptions: first, manipulation

of method headers is replaced by manipulation of fields (rules D:C:ADDSF and D:C:REMSF) and method implementations (rules D:C:ADDSM and D:C:REMSM). Second, methods may be modified using rule D:C:MODS. This rule replaces the method implementation, but keeps the old implementation with a fresh name. If the new implementation contains an original statement, then this statement is replaced by a call to the old implementation.
## Variability-free ABS module typing

<figure><img src="image_12.png" /></figure>

## Class definition typing

<figure><img src="image_13.png" /></figure>

## Method definition typing

<figure><img src="image_14.png" /></figure>

## Statement sequence typing

<figure><img src="image_15.png" /></figure>

## Statement typing

<figure><img src="image_16.png" /></figure>

<figure><img src="image_17.png" /></figure>

<figure><img src="image_18.png" /></figure>

## Expression typing

<figure><img src="image_19.png" /></figure>

<figure><img src="image_20.png" /></figure>

<figure><img src="image_21.png" /></figure>

## Interface definition typing

<figure><img src="image_22.png" /><figcaption>Fig. B.13. Variability-free ABS module typing rules.</figcaption></figure>

## Appendix B. Rules for Vf-ABS module typing

We present the rules of the type system for variability-free ABS modules. The rules, given in Fig. B.13, use the following lookup function for retrieving the type of an attribute M.N.a in the program signature table PrgS (recall that an attribute can be either a method or a field):

$$ aType(M.N.a) = \begin{cases} PrgS(M)(N)(a) & \text{if } a \in \text{dom}(PrgS(M)(N)) \\ aType(M'.I.a) & \text{if } a \notin \text{dom}(PrgS(M)(N)), \\ M'.I \in PrgS(M)(N) & \text{(super)} \end{cases} $$

For sake of simplicity, in the rule premises we use typing a sequence of elements as a shorthand for the implicit list of typing each element (in T:MODULE, T:CLASS, T:INVK). The rules fall into the following categories.

* **Variability-free ABS module typing** Rule T:MODULE is fairly standard: each class/interface declaration in the module is typed relative to the signature of the program and the name of the module. The sequence of statements in the (optional) init-block is typed relative to the signature of the program, the name of the module and the empty typing environment (environment Γ is discarded). No checks on the import- and export-clauses are performed, because these are subsumed by the assumption that the signature PrgS is well-formed.

* **Class definition typing** Rule T:CLASS is fairly standard. No checks on the field declarations and on the implements-clause are performed, because these are subsumed by the assumption that the signature PrgS is well-formed.

* **Method definition typing** Rule T:METH is fairly standard. First, it types the statements and the returned expression e in the
## Variability-free ABS module typing

<figure><img src="image_11.png" /></figure>

## Class definition typing

<figure><img src="image_12.png" /></figure>

## Method definition typing

<figure><img src="image_13.png" /></figure>

## Statement sequence typing

<figure><img src="image_14.png" /></figure>

## Statement typing

<figure><img src="image_15.png" /></figure>

<figure><img src="image_16.png" /></figure>

<figure><img src="image_17.png" /></figure>

## Expression typing

<figure><img src="image_18.png" /></figure>

<figure><img src="image_19.png" /></figure>

<figure><img src="image_20.png" /></figure>

## Interface definition typing

<figure><img src="image_21.png" /><figcaption>Fig. B.13. Variability-free ABS module typing rules.</figcaption></figure>

## Appendix B. Rules for Vf-ABS module typing

We present the rules of the type system for variability-free ABS modules. The rules, given in Fig. B.13, use the following lookup function for retrieving the type of an attribute M.N.a in the program signature table PrgS (recall that an attribute can be either a method or a field):

$$ aType(M.N.a) = \begin{cases} PrgS(M)(N)(a) & \text{if } a \in \text{dom}(PrgS(M)(N)) \\ aType(M'.I.a) & \text{if } a \notin \text{dom}(PrgS(M)(N)), \\ M'.I \in PrgS(M)(N) & \text{(super)} \end{cases} $$

For sake of simplicity, in the rule premises we use typing a sequence of elements as a shorthand for the implicit list of typing each element (in T:MODULE, T:CLASS, T:INVK). The rules fall into the following categories.

* **Variability-free ABS module typing** Rule T:MODULE is fairly standard: each class/interface declaration in the module is typed relative to the signature of the program and the name of the module. The sequence of statements in the (optional) init-block is typed relative to the signature of the program, the name of the module and the empty typing environment (environment Γ is discarded). No checks on the import- and export-clauses are performed, because these are subsumed by the assumption that the signature PrgS is well-formed.

* **Class definition typing** Rule T:CLASS is fairly standard. No checks on the field declarations and on the implements-clause are performed, because these are subsumed by the assumption that the signature PrgS is well-formed.

* **Method definition typing** Rule T:METH is fairly standard. First, it types the statements and the returned expression e in the
## VM pre-typing

<figure><img src="image_23.png" /></figure>

**Condition1:**

Each class/interface being modified/removed in a delta in `Dlt` is declared in `Defn` or added by some delta in `Dlt`.

**Condition2:**

Each attribute being modified in/removed from a class `C` by a delta in `Dlt` is declared in `C` in `Defn` or declared/added in `C` by some delta in `Dlt`.

**Condition3:**

Each method signature being removed from an interface `I` by a delta in `Dlt` is declared in `I` in `Defn` or declared/added in `I` by some delta in `Dlt`.

<caption>**Fig. C.14.** VM pre-typing rule.</caption>

body of the method with respect to the appropriate typing environments. Then it checks that the type of `e` is a subtype of return type of the method.

* **Statement sequence typing** Rule T:SEQ is fairly standard: a sequence of $n \ge 0$ statements is typed relative to the signature of the program, the name of the module, and a typing environment $\Gamma_0$. The $i$th ($i \ge 1$) statement of the sequence is typed relative to $\Gamma_i$ and produces $\Gamma_{i+1}$. The rule produces a typing environment $\Gamma_n$ that is augmented by the type assumptions for the variables declared by the statements in the sequence.

* **Statement typing** These rules are fairly standard: a statement is typed relative to the signature of the program, the name of the module, a typing environment. Each rule produces a typing environment that is either augmented by the type assumption for the variable declared by the statement (if the statement is a local variable declaration) or unchanged (otherwise).

* **Expression typing** These rules are fairly standard: each expression is typed relative to the signature of the program, the name of the module, and a typing environment $\Gamma$ that assigns a variable basic type to each variable that may occur in the expression and, whenever the expression occurs in the body of a method of a class `C`, assigns type `C` to this. We just point out that: fields can only be accessed through this (see rule T:FIELD), and methods cannot be invoked in new-expressions (rules T:NEW and T:INVK).

* **Interface definition typing** The assumption that the signature `PrgS` (of the program which contains the module `M` where the interface declaration `ID` occurs) is well-formed (Definition 18) entails that the interface declaration `ID` is well typed. Therefore, rule T:INTERFACE performs no checks.

## Appendix C. Rules for VM pre-typing

We present the pre-typing rules for VMs. The rules, given in Figs. C.14–C.16 use the following lookup function for retrieving the type of an attribute `M.N.a` in the family program signature table `FPrgS`:

$$ aType(M.N.a) = \begin{cases} FPrgS(M)(N)(a) & \text{if } a \in \text{dom}(FPrgS(M)(N)) \\ aType(M'.I.a) & \text{if } a \notin \text{dom}(FPrgS(M)(N)) \text{ and} \\ & M'.I[\text{with...}] \in FPrgS(M)(N) \text{ (super)} \end{cases} $$

Rule PT:VM in Fig. C.14 first checks three consistency conditions, then it pre-types each interface/class definition in the module core part (Fig. C.15), the sequence of statements in the (optional) `init-block`, and each delta in the module delta part (Fig. C.16). No checks on configuration knowledge are performed, because these are subsumed by the assumption that the family program signature `FPrgS` is type uniform.

The rules in Fig. C.15 are a straightforward adaptation of the typing rules for variability-free ABS classes an interfaces (Fig. B.13) and fall into corresponding categories: *Interface definition pre-typing*, *Expression pre-typing* (Rule PT:ORIGINAL is for pre-typing the *original* method invocation, which may occur in a method addition operation), *Statement pre-typing*, *Statement sequence pre-typing*, *Method definition pre-typing*, *Class definition pre-typing*.

The rules in Fig. C.16 fall into the following categories:

* **Delta pre-typing** Rule PT:DELTA simply pre-types each class operation. No checks are performed on interface operations, because these are subsumed by the assumption that the family program signature `FPrgS` is type uniform.

* **Class operation pre-typing** Rule PT:ADDS-CLASS simply pre-types the added class definition relying on rule PT:CLASS of Fig. C.15. Similar as before, rule PT:REMOVES-CLASS performs no checks, because these are subsumed by the assumption that the family program signature `FPrgS` is type uniform. Rule PT:MODIFIES-CLASS pre-types each attribute operation.

* **Attribute operation pre-typing** Rule PT:ADDS-METH simply pre-types the added method definition relying on rule PT:METH of Fig. C.15. Rules PT:ADDS-FIELD, PT:REMOVES-ATTR perform no checks, because these are subsumed by the assumption that the family program signature `FPrgS` is type uniform. Rule PT:MODIFIES-METH is similar to rule PT:ADDS-METH, however, it pre-types the body of the modified method relative to an environment that assigns to *original* the type of the method being modified. This makes it possible to use rule PT:ORIGINAL of Fig. C.15 during pre-typing of `S`.
## VM pre-typing

<figure><img src="image_22.png" /></figure>

**Condition1:**

Each class/interface being modified/removed in a delta in `Dlt` is declared in `Defn` or added by some delta in `Dlt`.

**Condition2:**

Each attribute being modified in/removed from a class `C` by a delta in `Dlt` is declared in `C` in `Defn` or declared/added in `C` by some delta in `Dlt`.

**Condition3:**

Each method signature being removed from an interface `I` by a delta in `Dlt` is declared in `I` in `Defn` or declared/added in `I` by some delta in `Dlt`.

<caption>**Fig. C.14.** VM pre-typing rule.</caption>

body of the method with respect to the appropriate typing environments. Then it checks that the type of `e` is a subtype of return type of the method.

* **Statement sequence typing** Rule T:SEQ is fairly standard: a sequence of $n \ge 0$ statements is typed relative to the signature of the program, the name of the module, and a typing environment $\Gamma_0$. The $i$th ($i \ge 1$) statement of the sequence is typed relative to $\Gamma_i$ and produces $\Gamma_{i+1}$. The rule produces a typing environment $\Gamma_n$ that is augmented by the type assumptions for the variables declared by the statements in the sequence.

* **Statement typing** These rules are fairly standard: a statement is typed relative to the signature of the program, the name of the module, a typing environment. Each rule produces a typing environment that is either augmented by the type assumption for the variable declared by the statement (if the statement is a local variable declaration) or unchanged (otherwise).

* **Expression typing** These rules are fairly standard: each expression is typed relative to the signature of the program, the name of the module, and a typing environment $\Gamma$ that assigns a variable basic type to each variable that may occur in the expression and, whenever the expression occurs in the body of a method of a class `C`, assigns type `C` to this. We just point out that: fields can only be accessed through this (see rule T:FIELD), and methods cannot be invoked in new-expressions (rules T:NEW and T:INVK).

* **Interface definition typing** The assumption that the signature `PrgS` (of the program which contains the module `M` where the interface declaration `ID` occurs) is well-formed (Definition 18) entails that the interface declaration `ID` is well typed. Therefore, rule T:INTERFACE performs no checks.

## Appendix C. Rules for VM pre-typing

We present the pre-typing rules for VMs. The rules, given in Figs. C.14–C.16 use the following lookup function for retrieving the type of an attribute `M.N.a` in the family program signature table `FPrgS`:

$$ \begin{aligned} \texttt{aType(M.N.a)} \\ = \left\{ \begin{array}{ll} \texttt{FPrgS(M)(N)(a)} & \text{if } a \in \text{dom}(\texttt{FPrgS(M)(N)}) \\ \texttt{aType(M'.I.a)} & \text{if } a \notin \text{dom}(\texttt{FPrgS(M)(N)}) \text{ and} \\ & \quad M'.I[\text{with...}] \in \texttt{FPrgS(M)(N)} (\text{super}) \end{array} \right. \end{aligned} $$

Rule PT:VM in Fig. C.14 first checks three consistency conditions, then it pre-types each interface/class definition in the module core part (Fig. C.15), the sequence of statements in the (optional) `init-block`, and each delta in the module delta part (Fig. C.16). No checks on configuration knowledge are performed, because these are subsumed by the assumption that the family program signature `FPrgS` is type uniform.

The rules in Fig. C.15 are a straightforward adaptation of the typing rules for variability-free ABS classes an interfaces (Fig. B.13) and fall into corresponding categories: *Interface definition pre-typing*, *Expression pre-typing* (Rule PT:ORIGINAL is for pre-typing the original method invocation, which may occur in a method addition operation), *Statement pre-typing*, *Statement sequence pre-typing*, *Method definition pre-typing*, *Class definition pre-typing*.

The rules in Fig. C.16 fall into the following categories:

* **Delta pre-typing** Rule PT:DELTA simply pre-types each class operation. No checks are performed on interface operations, because these are subsumed by the assumption that the family program signature `FPrgS` is type uniform.

* **Class operation pre-typing** Rule PT:ADDS-CLASS simply pre-types the added class definition relying on rule PT:CLASS of Fig. C.15. Similar as before, rule PT:REMOVES-CLASS performs no checks, because these are subsumed by the assumption that the family program signature `FPrgS` is type uniform. Rule PT:MODIFIES-CLASS pre-types each attribute operation.

* **Attribute operation pre-typing** Rule PT:ADDS-METH simply pre-types the added method definition relying on rule PT:METH of Fig. C.15. Rules PT:ADDS-FIELD, PT:REMOVES-ATTR perform no checks, because these are subsumed by the assumption that the family program signature `FPrgS` is type uniform. Rule PT:MODIFIES-METH is similar to rule PT:ADDS-METH, however, it pre-types the body of the modified method relative to an environment that assigns to original the type of the method being modified. This makes it possible to use rule PT:ORIGINAL of Fig. C.15 during pre-typing of `S`.
## Class definition pre-typing

$$ \begin{array}{c} \texttt{PT:CLASS} \\ \qquad \texttt{FPrgS: M; { this:M.C } \dot{\equiv} \overline{MD: MT}} \\ \qquad \texttt{FPrgS: M \dot{\equiv} \text{class C [ implements I I ] } \{ FD MD \}} \end{array} $$

## Method definition pre-typing

$$ \begin{array}{c} \texttt{PT:METH} \\ \qquad \texttt{FPrgS: M; { this:M.C, $\overline{VT x}$ } \dot{\equiv} \overline{S: \Gamma'} FPrgS: M; \Gamma' \dot{\equiv} E: ET strip(ET) <: strip(VT)} \\ \qquad \texttt{FPrgS: M; { this:M.C } \dot{\equiv} VT m (VT x) \{ S return E \} : (VT) \to VT} \end{array} $$

## Statement sequence pre-typing

$$ \begin{array}{c} \texttt{PT:SEQ} \\ \qquad n \ge 0 \quad \texttt{FPrgS: M; $\Gamma_{i-1} \dot{\equiv} S_i : VT_i; \Gamma_i$ (for all $i \in \{1...n\}$)} \\ \qquad \qquad \texttt{FPrgS: M; $\Gamma_0 \dot{\equiv} S_1;...S_n$; $\Gamma_n$} \end{array} $$

## Statement pre-typing

$$ \begin{array}{c} \texttt{PT:LOCVARDEC} \\ \qquad \texttt{FPrgS: M; $\Gamma \dot{\equiv} E: ET strip(ET) <: strip(VT)} \\ \qquad \texttt{FPrgS: M; $\Gamma \dot{\equiv} VT x = E: VT; \Gamma \dot{\supset} \{x:VT\}$} \end{array} $$

$$ \begin{array}{c} \texttt{PT:LOCVARASSIGN} \\ \qquad \texttt{$\Gamma(x) = VT$ FPrgS: M; $\Gamma \dot{\equiv} E: ET strip(ET) <: strip(VT)$} \\ \qquad \texttt{FPrgS: M; $\Gamma \dot{\equiv} x = E: VT; \Gamma$} \end{array} $$

$$ \begin{array}{c} \texttt{PT:FIELDASSIGN} \\ \qquad $\Gamma(\texttt{this})=M.C$ FPrgS(M)(C)(f) = VT FPrgS: M; $\Gamma \dot{\equiv} E: ET strip(ET) <: strip(VT)$ \\ \qquad \texttt{FPrgS: M; $\Gamma \dot{\equiv} this.f = E: VT; \Gamma$} \end{array} $$

## Expression pre-typing

$$ \begin{array}{c} \texttt{PT:VAR} \\ \qquad \texttt{FPrgS: M; $\Gamma \dot{\equiv} x : \Gamma(x)$} \end{array} $$

$$ \begin{array}{c} \texttt{PT:FIELD} \\ \qquad $\Gamma(\texttt{this})=M.C$ FPrgS(M)(C)(f) = VT \\ \qquad \texttt{FPrgS: M; $\Gamma \dot{\equiv} this.f : VT$} \end{array} $$

$$ \begin{array}{c} \texttt{PT:INVK} \\ \qquad \texttt{FPrgS: M; $\Gamma \dot{\equiv} E: M'.I [with ...]$ aType(M'.I.m) = (\overline{VT}) \to VT} \\ \qquad \texttt{FPrgS: M; $\Gamma \dot{\equiv} E: \overline{VT'}$ strip( $\overline{VT'}$) <: strip( $\overline{VT}$)} \\ \qquad \texttt{FPrgS: M; $\Gamma \dot{\equiv} E.m(E) : VT$} \end{array} $$

$$ \begin{array}{c} \texttt{PT:NEW} \\ \qquad \texttt{C \in dom(FPrgS(M'))} \\ \qquad \texttt{FPrgS: M; $\Gamma \dot{\equiv} new M'.C() [with KE] : M'.C [with KE]$} \end{array} $$

$$ \begin{array}{c} \texttt{PT:ORIGINAL} \\ \qquad $\Gamma(\texttt{original}) = (\overline{VT}) \to VT$ FPrgS: M; $\Gamma \dot{\equiv} E: \overline{VT'}$ strip( $\overline{VT'}$) <: strip( $\overline{VT}$) \\ \qquad \texttt{FPrgS: M; $\Gamma \dot{\equiv} original(E) : VT$} \end{array} $$

## Interface definition pre-typing

$$ \begin{array}{c} \texttt{PT:INTERFACE} \\ \qquad \texttt{FPrgS: M \dot{\equiv} ID} \end{array} $$

<caption>Fig. C.15. Class/interface pre-typing rules.</caption>

## Delta pre-typing

$$ \begin{array}{c} \texttt{PT:DELTA} \\ \qquad \texttt{FPrgS: M \dot{\equiv} \overline{CO}} \\ \qquad \texttt{FPrgS: M \dot{\equiv} delta D; CO IO} \end{array} $$

## Class operation pre-typing

$$ \begin{array}{c} \texttt{PT:ADDS-CLASS} \\ \qquad \texttt{FPrgS: M \dot{\equiv} CD} \\ \qquad \texttt{FPrgS: M \dot{\equiv} adds CD} \end{array} $$

$$ \begin{array}{c} \texttt{PT:REMOVES-CLASS} \\ \qquad \texttt{FPrgS: M \dot{\equiv} removes C} \end{array} $$

$$ \begin{array}{c} \texttt{PT:MODIFIES-CLASS} \\ \qquad \texttt{FPrgS: M; { this:M.C } \dot{\equiv} \overline{AO}} \\ \qquad \texttt{FPrgS: M \dot{\equiv} modifies class C [adds IR IR] [removes IR IR]} \{ AO \} \end{array} $$

## Attribute operation pre-typing

$$ \begin{array}{c} \texttt{PT:ADDS-METH} \\ \qquad \texttt{FPrgS: M; { this:M.C } \dot{\equiv} MD: MT} \\ \qquad \texttt{FPrgS: M; { this:M.C } \dot{\equiv} adds MD} \end{array} $$

$$ \begin{array}{c} \texttt{PT:ADDS-FIELD} \\ \qquad \texttt{FPrgS: M \dot{\equiv} adds FD} \end{array} $$

$$ \begin{array}{c} \texttt{PT:REMOVES-ATTR} \\ \qquad \texttt{FPrgS: M \dot{\equiv} removes AD} \end{array} $$

$$ \begin{array}{c} \texttt{PT:MODIFIES-METH} \\ \qquad \texttt{FPrgS: M; { this:M.C, original:($\overline{VT}$) $\to$ VT, $\overline{VT x}$ } \dot{\equiv} \overline{S: \Gamma'} strip(ET) <: strip(VT)} \\ \qquad \texttt{FPrgS: M; $\Gamma' \dot{\equiv} E: ET$} \\ \qquad \texttt{FPrgS: M; { this:M.C } \dot{\equiv} modifies VT m (VT x) \{ S return E \}} \end{array} $$

<caption>Fig. C.16. Delta pre-typing rules.</caption>
## Class definition pre-typing

$$ \begin{array}{l} \texttt{PT:CLASS} \\ \qquad \texttt{FPrgS: M; { this:M.C } \dot{\lor} MD: MT} \\ \qquad \texttt{FPrgS: M \dot{\lor} class C [ implements I I ] { FD MD }} \end{array} $$

## Method definition pre-typing

$$ \begin{array}{l} \texttt{PT:METH} \\ \quad \texttt{FPrgS: M; { this:M.C, $\overline{VT}$ x } \dot{\lor} S: $\Gamma'$ FPrgS: M; $\Gamma' \dot{\lor} E: ET$ strip(ET) <: strip(VT)} \\ \quad \texttt{FPrgS: M; { this:M.C } \dot{\lor} VT m (VT x) { S return E } : (VT) \to VT} \end{array} $$

## Statement sequence pre-typing

$$ \begin{array}{l} \texttt{PT:SEQ} \\ \quad n \ge 0 \quad \texttt{FPrgS: M; $\Gamma_{i-1} \dot{\lor} S_i$: VT; $\Gamma_i$ (for all $i \in \{1...n\}$)} \\ \quad \texttt{FPrgS: M; $\Gamma_0 \dot{\lor} S_1;...S_n$: $\Gamma_n$} \end{array} $$

## Statement pre-typing

$$ \begin{array}{l} \texttt{PT:LOCVARDEC} \\ \quad \texttt{FPrgS: M; $\Gamma \dot{\lor} E$: ET strip(ET) <: strip(VT)} \\ \quad \texttt{FPrgS: M; $\Gamma \dot{\lor} VT$ x = E: VT; $\Gamma \dot{\lor} \{x:VT\}$} \end{array} $$

$$ \begin{array}{l} \texttt{PT:LOCVARASSIGN} \\ \quad \Gamma(x) = VT \quad \texttt{FPrgS: M; $\Gamma \dot{\lor} E$: ET strip(ET) <: strip(VT)} \\ \quad \texttt{FPrgS: M; $\Gamma \dot{\lor} x$ = E: VT; $\Gamma$} \end{array} $$

$$ \begin{array}{l} \texttt{PT:FIELDASSIGN} \\ \quad \Gamma(\texttt{this})=M.C \quad \texttt{FPrgS(M)(C)(f) = VT} \quad \texttt{FPrgS: M; $\Gamma \dot{\lor} E$: ET strip(ET) <: strip(VT)} \\ \quad \texttt{FPrgS: M; $\Gamma \dot{\lor} this.f$ = E: VT; $\Gamma$} \end{array} $$

## Expression pre-typing

$$ \begin{array}{l} \texttt{PT:VAR} \\ \quad \texttt{FPrgS: M; $\Gamma \dot{\lor} x$: $\Gamma(x)$} \end{array} $$

$$ \begin{array}{l} \texttt{PT:FIELD} \\ \quad \frac{\Gamma(\texttt{this})=M.C}{\texttt{FPrgS: M; $\Gamma \dot{\lor} this.f$: VT}} \end{array} $$

$$ \begin{array}{l} \texttt{PT:INVK} \\ \quad \texttt{FPrgS: M; $\Gamma \dot{\lor} E$: M'.I [with ...]} \quad \texttt{aType(M'.I.m) = (VT)} \to VT \\ \quad \texttt{FPrgS: M; $\Gamma \dot{\lor} E$: $\overline{VT'}$ strip($\overline{VT'}$) <: strip($\overline{VT}$)} \\ \quad \texttt{FPrgS: M; $\Gamma \dot{\lor} E$.m(E): VT} \end{array} $$

$$ \begin{array}{l} \texttt{PT:NEW} \\ \quad \frac{C \in \text{dom}(\texttt{FPrgS(M')})}{\texttt{FPrgS: M; $\Gamma \dot{\lor} new M'.C()$ [with KE]: $M'.C$ [with KE]}} \end{array} $$

$$ \begin{array}{l} \texttt{PT:ORIGINAL} \\ \quad \frac{\Gamma(\texttt{original}) = (\overline{VT}) \to VT}{\texttt{FPrgS: M; $\Gamma \dot{\lor} E$: $\overline{VT'}$ strip($\overline{VT'}$) <: strip($\overline{VT}$)}} \\ \quad \texttt{FPrgS: M; $\Gamma \dot{\lor} original(E)$: VT} \end{array} $$

## Interface definition pre-typing

$$ \begin{array}{l} \texttt{PT:INTERFACE} \\ \quad \texttt{FPrgS: M \dot{\lor} ID} \end{array} $$

<caption>Fig. C.15. Class/interface pre-typing rules.</caption>

## Delta pre-typing

$$ \begin{array}{l} \texttt{PT:DELTA} \\ \quad \frac{\texttt{FPrgS: M \dot{\lor} CO}}{\texttt{FPrgS: M \dot{\lor} delta D; CO IO}} \end{array} $$

## Class operation pre-typing

$$ \begin{array}{l} \texttt{PT:ADDS-CLASS} \\ \quad \frac{\texttt{FPrgS: M \dot{\lor} CD}}{\texttt{FPrgS: M \dot{\lor} adds CD}} \end{array} $$

$$ \begin{array}{l} \texttt{PT:REMOVES-CLASS} \\ \quad \texttt{FPrgS: M \dot{\lor} removes C} \end{array} $$

$$ \begin{array}{l} \texttt{PT:MODIFIES-CLASS} \\ \quad \frac{\texttt{FPrgS: M; { this:M.C } \dot{\lor} AO}}{\texttt{FPrgS: M \dot{\lor} modifies class C [adds IR IR] [removes IR IR] { AO }} \end{array} $$

## Attribute operation pre-typing

$$ \begin{array}{l} \texttt{PT:ADDS-METH} \\ \quad \texttt{FPrgS: M; { this:M.C } \dot{\lor} MD: MT} \\ \quad \texttt{FPrgS: M; { this:M.C } \dot{\lor} adds MD} \end{array} $$

$$ \begin{array}{l} \texttt{PT:ADDS-FIELD} \\ \quad \texttt{FPrgS: M \dot{\lor} adds FD} \end{array} $$

$$ \begin{array}{l} \texttt{PT:REMOVES-ATTR} \\ \quad \texttt{FPrgS: M \dot{\lor} removes AD} \end{array} $$

$$ \begin{array}{l} \texttt{PT:MODIFIES-METH} \\ \quad \texttt{FPrgS: M; { this:M.C, original:($\overline{VT}$) $\to$ VT, $\overline{VT}$ x } \dot{\lor} S: $\Gamma'$ strip(ET) <: strip(VT)} \\ \quad \texttt{FPrgS: M; { this:M.C } \dot{\lor} modifies VT m (VT x) { S return E }} \end{array} $$

<caption>Fig. C.16. Delta pre-typing rules.</caption>
## Appendix D. Rules for applicability constraint inference

We present the rules for computing the applicability constraint of an ABS program. The rules parse a normal form ABS-VM program Prg from left to right. They assume the list of deltas in Prg is in an order compatible with the configuration knowledge CK.

All statements in the focus of the rules have the form $C \vdash G : \Theta, \Phi$, where (i) G is the syntax element being parsed according to Fig. 6, (ii) C stores relevant context information (the currently parsed module's name, the currently parsed delta's activation condition or **true** when parsing the module core part, the input declaration presence mapping), (iii) $\Theta$ is the output declaration presence mapping (from the analysis of G), (iv) $\Phi$ is the output applicability constraint (from the analysis of G). Elements $\Phi$ and $\Theta$ are defined simultaneously. At each stage $\Phi$ contains information about current applicability of deltas in products, while $\Theta$ collects information about the presence of G in products.

The first applicability rule is for programs:

$$ \begin{array}{l} \textbf{A:PRG} \\ \textbf{Prg} = \text{Mdl}_1 \cdots \text{Mdl}_n \\ \vdash \text{Prg} : \bigcup_{1 \le i \le n} \Theta_i, \bigwedge_{1 \le i \le n} \Phi_i \end{array} \quad \vdash \text{Mdl}_i : \Theta_i, \Phi_i $$

The rule runs through each module declaration Mdlᵢ, collecting presence and applicability information. According to Fig. 6, each class/interface operation C0/I0 declares the *unqualified* class/interface name C/I on which it intends to act. If the operation is in module M then, in accordance with the flattening rules, it is (implicitly) qualified by M. Therefore, deltas cannot declare operations outside of the scope of their module, so no module can modify presence conditions in other modules.

The next rule is for modules. The initial domain of the presence mapping $\Theta_0$ is set to **false**. This domain includes the names of all interfaces, classes, and attributes extracted from the module by fsig.

$$ \begin{array}{l} \textbf{A:MODULE} \\ \Theta_0 = [Q \mapsto \textbf{false}]_{Q \in \text{dom}(M)} \quad M, \Theta_{i-1}, \textbf{true} \vdash \text{Defn}_i : \Theta_i, \Phi_i \quad (1 \le i \le n) \\ M, \Theta_{i-1} \vdash \text{Dlt}_i : \Theta_i, \Phi_i \quad (n+1 \le i \le m) \\ \vdash \left( \begin{array}{@{}l@{}} \text{module M;} \\ \quad [ \text{export tC; } ] \quad \text{import tC from M;} \quad [ \text{features F with } \Phi; ] \quad \overline{KD} \overline{PD} \\ \text{Defn}_1 \cdots \text{Defn}_n \quad [ \text{init } \{ \overline{S} \} ] \quad \text{Dlt}_{n+1} \cdots \text{Dlt}_m \quad \text{CK} \end{array} \right) : \Theta_m, \bigwedge_{1 \le i \le m} \Phi_i \end{array} $$

The judgments for class and interface declarations have an additional constraint **true** on the left-hand side: it allows to reuse the rules for deltas adding declarations where we set **true** as activation condition. The applicability constraint of the module is the conjunction of all $\Phi_i$, while the presence mapping is updated sequentially.

The next two rules handle class/interface declarations uniformly, whether they come from the core part or from deltas (see rule [A:ADDC] below).

$$ \begin{array}{l} \textbf{A:CLASS} \\ \text{M.C, } \Theta_{i-1}, \Phi \vdash \text{FD}_i : \Theta_i, \Phi_i \quad (1 \le i \le n) \quad \text{M.C, } \Theta_{i-1}, \Phi \vdash \text{MD}_i : \Theta_i, \Phi_i \quad (n+1 \le i \le m) \\ \qquad \Theta' = \Theta_m[\text{M.C} \mapsto \Theta_m(\text{M.C}) \lor \Phi] \quad \Phi' = (\bigwedge_{1 \le i \le m} \Phi_i) \land (\Phi \to \neg \Theta_m(\text{M.C})) \\ \text{M, } \Theta_0, \Phi \vdash [\text{unique}] \quad \text{class C implements } \text{IR}_1 \cdots \text{IR}_r \quad \{ \text{FD}_1 \cdots \text{FD}_n, \text{MD}_{n+1} \cdots \text{MD}_m \} : \Theta', \Phi' \end{array} $$

$$ \begin{array}{l} \textbf{A:INTERFACE} \\ \text{M.I, } \Theta_{i-1}, \Phi \vdash \text{MH}_i : \Theta_i, \Phi_i \quad (1 \le i \le m) \\ \qquad \Theta' = \Theta_m[\text{M.I} \mapsto \Theta_m(\text{M.I}) \lor \Phi] \quad \Phi' = (\bigwedge_{1 \le i \le m} \Phi_i) \land (\Phi \to \neg \Theta_m(\text{M.I})) \\ \text{M, } \Theta_0, \Phi \vdash [\text{unique}] \quad \text{interface I extends IR}_1 \cdots \text{IR}_r \quad \{ \text{MH}_1 \cdots, \text{MH}_m \} : \Theta', \Phi' \end{array} $$

We do not collect information about the presence of implements/extends, because these clauses can be always added/removed, so they do not influence delta applicability and flattening.

The rules for fields, methods, and method headers collect the expected information.

$$ \textbf{A:FIELD} \\ \text{M.C, } \Theta, \Phi \vdash T x; \quad \Theta[\text{M.C.x} \mapsto \Theta(\text{M.C.x}) \lor \Phi], \Phi \Rightarrow (\neg \Theta(\text{M.C.x})) $$

$$ \textbf{A:METH} \\ \frac{\text{M.C, } \Theta, \Phi \vdash \text{MH} : \Theta', \Phi'}{\text{M.C, } \Theta, \Phi \vdash \text{MH} \{ \overline{S} \text{ return E;} \} : \Theta', \Phi'} $$

$$ \textbf{A:MHEADER} \\ \text{M.N, } \Theta, \Phi \vdash T m(\overline{T x}) : \Theta[\text{M.N.m} \mapsto \Theta(\text{M.N.m}) \lor \Phi], \Phi \Rightarrow (\neg \Theta(\text{M.N.m})) $$

The next rule parses deltas. It traverses the class/interface operations, using information about the application condition M.D on the left-hand side.

$$ \begin{array}{l} \textbf{A:DELTA} \\ \text{M, } \Theta_{i-1}, \text{M.D} \vdash \text{C0}_i : \Theta_i, \Phi_i \quad (1 \le i \le n) \quad \text{M, } \Theta_{i-1}, \text{M.D} \vdash \text{IO}_i : \Theta_i, \Phi_i \quad (n+1 \le i \le m) \\ \qquad \text{M, } \Theta_0 \vdash \text{delta M.D; C0}_1 \cdots C0_n IO_{n+1} \cdots IO_m : \Theta_m, \bigwedge_{1 \le i \le m} \Phi_i \end{array} $$

The rule for adding a class simply forwards to the class declaration rule:
## Appendix D. Rules for applicability constraint inference

We present the rules for computing the applicability constraint of an ABS program. The rules parse a normal form ABS-VM program Prg from left to right. They assume the list of deltas in Prg is in an order compatible with the configuration knowledge CK.

All statements in the focus of the rules have the form $C \vdash G : \Theta, \Phi$, where (i) G is the syntax element being parsed according to Fig. 6, (ii) C stores relevant context information (the currently parsed module's name, the currently parsed delta's activation condition or **true** when parsing the module core part, the input declaration presence mapping), (iii) $\Theta$ is the output declaration presence mapping (from the analysis of G), (iv) $\Phi$ is the output applicability constraint (from the analysis of G). Elements $\Phi$ and $\Theta$ are defined simultaneously. At each stage $\Phi$ contains information about current applicability of deltas in products, while $\Theta$ collects information about the presence of G in products.

The first applicability rule is for programs:

$$ \begin{array}{l} \textbf{A:PRG} \\ \textbf{Prg} = \text{Mdl}_1 \cdots \text{Mdl}_n \\ \vdash \text{Prg} : \bigcup_{1 \le i \le n} \Theta_i, \bigwedge_{1 \le i \le n} \Phi_i \end{array} \quad \vdash \text{Mdl}_i : \Theta_i, \Phi_i $$

The rule runs through each module declaration Mdl<sub>i</sub>, collecting presence and applicability information. According to Fig. 6, each class/interface operation C0/I0 declares the *unqualified* class/interface name C/I on which it intends to act. If the operation is in module M then, in accordance with the flattening rules, it is (implicitly) qualified by M. Therefore, deltas cannot declare operations outside of the scope of their module, so no module can modify presence conditions in other modules.

The next rule is for modules. The initial domain of the presence mapping $\Theta_0$ is set to **false**. This domain includes the names of all interfaces, classes, and attributes extracted from the module by fsig.

$$ \begin{array}{l} \textbf{A:MODULE} \\ \Theta_0 = [Q \mapsto \textbf{false}]_{Q \in \text{dom}(M)} \quad M, \Theta_{i-1}, \textbf{true} \vdash \text{Defn}_i : \Theta_i, \Phi_i \quad (1 \le i \le n) \\ M, \Theta_{i-1} \vdash \text{Dlt}_i : \Theta_i, \Phi_i \quad (n+1 \le i \le m) \\ \vdash \left( \begin{array}{@{}l@{}} \text{module M;} \\ \quad [ \text{export tC; } ] \quad \text{import tC from M;} \quad [ \text{features F with } \Phi; ] \quad \overline{KD} \overline{PD} \\ \quad \text{Defn}_1 \cdots \text{Defn}_n \quad [ \text{init } \{ \overline{S} \} ] \quad \text{Dlt}_{n+1} \cdots \text{Dlt}_m \quad \text{CK} \end{array} \right) : \Theta_m, \bigwedge_{1 \le i \le m} \Phi_i \end{array} $$

The judgments for class and interface declarations have an additional constraint **true** on the left-hand side: it allows to reuse the rules for deltas adding declarations where we set **true** as activation condition. The applicability constraint of the module is the conjunction of all $\Phi_i$, while the presence mapping is updated sequentially.

The next two rules handle class/interface declarations uniformly, whether they come from the core part or from deltas (see rule [A:ADDC] below).

$$ \begin{array}{l} \textbf{A:CLASS} \\ \text{M.C, } \Theta_{i-1}, \Phi \vdash \text{FD}_i : \Theta_i, \Phi_i \quad (1 \le i \le n) \quad \text{M.C, } \Theta_{i-1}, \Phi \vdash \text{MD}_i : \Theta_i, \Phi_i \quad (n+1 \le i \le m) \\ \qquad \Theta' = \Theta_m[\text{M.C} \mapsto \Theta_m(\text{M.C}) \lor \Phi] \quad \Phi' = (\bigwedge_{1 \le i \le m} \Phi_i) \land (\Phi \to \neg \Theta_m(\text{M.C})) \\ \text{M, } \Theta_0, \Phi \vdash [\text{unique}] \quad \text{class C implements } \text{IR}_1 \cdots \text{IR}_r \quad \{ \text{FD}_1 \cdots \text{FD}_n, \text{MD}_{n+1} \cdots \text{MD}_m \} : \Theta', \Phi' \end{array} $$

$$ \begin{array}{l} \textbf{A:INTERFACE} \\ \text{M.I, } \Theta_{i-1}, \Phi \vdash \text{MH}_i : \Theta_i, \Phi_i \quad (1 \le i \le m) \\ \qquad \Theta' = \Theta_m[\text{M.I} \mapsto \Theta_m(\text{M.I}) \lor \Phi] \quad \Phi' = (\bigwedge_{1 \le i \le m} \Phi_i) \land (\Phi \to \neg \Theta_m(\text{M.I})) \\ \text{M, } \Theta_0, \Phi \vdash [\text{unique}] \quad \text{interface I extends IR}_1 \cdots \text{IR}_r \quad \{ \text{MH}_1 \cdots, \text{MH}_m \} : \Theta', \Phi' \end{array} $$

We do not collect information about the presence of implements/extends, because these clauses can be always added/removed, so they do not influence delta applicability and flattening.

The rules for fields, methods, and method headers collect the expected information.

$$ \textbf{A:FIELD} \\ \text{M.C, } \Theta, \Phi \vdash \text{T x;} : \Theta[\text{M.C.x} \mapsto \Theta(\text{M.C.x}) \lor \Phi], \Phi \Rightarrow (\neg \Theta(\text{M.C.x})) $$

$$ \textbf{A:METH} \\ \frac{\text{M.C, } \Theta, \Phi \vdash \text{MH} : \Theta', \Phi'}{\text{M.C, } \Theta, \Phi \vdash \text{MH} \{ \overline{S} \text{ return E;} \} : \Theta', \Phi'} $$

$$ \textbf{A:MHEADER} \\ \text{M.N, } \Theta, \Phi \vdash \text{T m(\overline{T x})} : \Theta[\text{M.N.m} \mapsto \Theta(\text{M.N.m}) \lor \Phi], \Phi \Rightarrow (\neg \Theta(\text{M.N.m})) $$

The next rule parses deltas. It traverses the class/interface operations, using information about the application condition M.D on the left-hand side.

$$ \begin{array}{l} \textbf{A:DELTA} \\ \text{M, } \Theta_{i-1}, \text{M.D} \vdash \text{C0}_i : \Theta_i, \Phi_i \quad (1 \le i \le n) \quad \text{M, } \Theta_{i-1}, \text{M.D} \vdash \text{IO}_i : \Theta_i, \Phi_i \quad (n+1 \le i \le m) \\ \qquad \text{M, } \Theta_0 \vdash \text{delta M.D; C0}_1 \cdots C0_n IO_{n+1} \cdots IO_m : \Theta_m, \bigwedge_{1 \le i \le m} \Phi_i \end{array} $$

The rule for adding a class simply forwards to the class declaration rule:
$$ \begin{array}{c} A:ADDC \\ \frac{M, \Theta, \Phi \vdash \text{CD} : \Theta', \Phi}{M, \Theta, \Phi \vdash \text{adds CD} : \Theta', \Phi} \end{array} $$

The rule for removing a class first states, in the constraint $\Phi'$, that for this operation to be valid the class M.C must be already be declared. It then updates the mapping $\Theta$ into $\Theta'$, stating that M.C, its fields, methods and subtype declarations are only present when that remove operation (triggered by the constraint in $\Phi$) is not activated.

$$ \begin{array}{c} A:REMC \\ \frac{\Phi' = (\Phi \Rightarrow \Theta(M.C)) \quad \Theta' = \Theta[M.C \mapsto \Theta(M.C) \wedge (\neg \Phi)][M.C.a \mapsto \Theta(M.C.a) \wedge (\neg \Phi)][M.C.a \in \text{dom}(\Theta)]}{M, \Theta, \Phi \vdash \text{removes class C} : \Theta', \Phi'} \end{array} $$

The rule for class modification ignores added/removed interfaces to implement, because this is always allowed. It generates the applicability constraint $\Phi'$ by accumulating the constraints $\Phi_i$ (all added elements must not be present before and all removed element must be present), and adding the constraint that the class M.C must be present.

$$ \begin{array}{c} A:MODC \\ \frac{M.C, \Theta_{i-1}, \Phi \vdash AO_i : \Theta_i, \Phi_i \quad (1 \le i \le n) \quad \Phi' = (\bigwedge_{1 \le i \le n} \Phi_i) \wedge (\Phi \Rightarrow \Theta(M.C))}{M, \Theta_0, \Phi \vdash \text{modifies class C adds } IR_1 \cdots IR_q \text{ removes } IR_1 \cdots IR_r \text{ {AO}_1 \cdots AO_n}} : \Theta_n, \Phi' \end{array} $$

The rule for adding attributes forwards to the rule for attribute definition:

$$ \begin{array}{c} A:ADDA \\ \frac{M.C, \Theta, \Phi \vdash \text{AD} : \Theta', \Phi'}{M.C, \Theta, \Phi \vdash \text{adds AD} : \Theta', \Phi'} \end{array} $$

The two following rules, for removing a field or a method, build a constraint $\Phi'$ ensuring that, whenever the activation condition $\Phi$ of the delta containing the operation becomes **true**, then the attribute is present ($\Theta(M.C.x)$ holds). Moreover, they update $\Theta'$ to store the information that the attribute is no longer available after the operation is applied.

$$ \begin{array}{c} A:REMFD \\ \frac{\Phi' = (\Phi \Rightarrow \Theta(M.N.x)) \quad \Theta' = \Theta[M.N.x \mapsto \Theta(M.N.x) \wedge (\neg \Phi)]}{M.N, \Theta, \Phi \vdash \text{removes } VT \ x; : \Theta', \Phi'} \end{array} $$

$$ \begin{array}{c} A:REMMH \\ \frac{\Phi' = (\Phi \Rightarrow \Theta(M.C.m)) \quad \Theta' = \Theta[M.C.m \mapsto \Theta(M.C.m) \wedge (\neg \Phi)]}{M.C, \Theta, \Phi \vdash \text{removes } VT \ m(\overline{VT} \ x) : \Theta', \Phi'} \end{array} $$

The rule for modifying a method requires in the applicability constraint $\Phi'$ that the method must already be present (when activation condition $\Phi$ holds), but leaves the presence mapping unchanged:

$$ \begin{array}{c} A:ModM \\ \frac{\Phi' = (\Phi \Rightarrow \Theta(M.C.m))}{M.C, \Theta, \Phi \vdash \text{modifies } VT \ m(\overline{VT} \ x) \text{ {S return E; }} : \Theta, \Phi'} \end{array} $$

The rules for delta operations on interfaces are similar to those for class operations:

$$ \begin{array}{c} A:ADDI \\ \frac{M, \Theta, \Phi \vdash \text{ID} : \Theta', \Phi}{M, \Theta, \Phi \vdash \text{adds ID} : \Theta', \Phi} \end{array} $$

$$ \begin{array}{c} A:REMI \\ \frac{\Phi' = (\Phi \Rightarrow \Theta(M.I)) \quad \Theta' = \Theta[M.I \mapsto \Theta(M.I) \wedge (\neg \Phi)][M.I.a \mapsto \Theta(M.I.a) \wedge (\neg \Phi)][M.I.a \in \text{dom}(\Theta)]}{M, \Theta, \Phi \vdash \text{removes interface I} : \Theta', \Phi'} \end{array} $$

$$ \begin{array}{c} A:ModI \\ \frac{M.I, \Theta_{i-1}, \Phi \vdash HO_i : \Theta_i, \Phi_i \quad \Phi' = (\bigwedge_{1 \le i \le n} \Phi_i) \wedge (\Phi \Rightarrow \Theta(M.I))}{M, \Theta_0, \Phi \vdash \text{modifies interface I adds } IR_1 \cdots IR_q \text{ removes } IR'_1 \cdots IR'_r \text{ {HO}_1 \cdots HO_n}} : \Theta_n, \Phi' \end{array} $$

$$ \begin{array}{c} A:ADDMH \\ \frac{M.I, \Theta, \Phi \vdash \text{MH} : \Theta', \Phi'}{M.I, \Theta, \Phi \vdash \text{adds MH} : \Theta', \Phi'} \end{array} $$
$$A:ADDC \frac{M, \Theta, \Phi \vdash CD : \Theta', \Phi}{M, \Theta, \Phi \vdash \text{adds } CD : \Theta', \Phi}$$

The rule for removing a class first states, in the constraint $\Phi'$, that for this operation to be valid the class M.C must be already be declared. It then updates the mapping $\Theta$ into $\Theta'$, stating that M.C, its fields, methods and subtype declarations are only present when that remove operation (triggered by the constraint in $\Phi$) is not activated.

$$A:REMC \frac{\Phi' = (\Phi \Rightarrow \Theta(M.C)) \quad \Theta' = \Theta[M.C \mapsto \Theta(M.C) \wedge (\neg \Phi)][M.C.a \mapsto \Theta(M.C.a) \wedge (\neg \Phi)][M.C.a \in \text{dom}(\Theta)]}{M, \Theta, \Phi \vdash \text{removes class } C : \Theta', \Phi'}$$

The rule for class modification ignores added/removed interfaces to implement, because this is always allowed. It generates the applicability constraint $\Phi'$ by accumulating the constraints $\Phi_i$ (all added elements must not be present before and all removed element must be present), and adding the constraint that the class M.C must be present.

$$A:MODC \frac{M.C, \Theta_{i-1}, \Phi \vdash AO_i : \Theta_i, \Phi_i \quad (1 \le i \le n) \quad \Phi' = (\bigwedge_{1 \le i \le n} \Phi_i) \wedge (\Phi \Rightarrow \Theta(M.C))}{M, \Theta_0, \Phi \vdash \text{modifies class } C \text{ adds } IR_1 \cdots IR_q \text{ removes } IR_1 \cdots IR_r \{ AO_1 \cdots AO_n \} : \Theta_n, \Phi'}$$

The rule for adding attributes forwards to the rule for attribute definition:

$$A:ADDA \frac{M.C, \Theta, \Phi \vdash AD : \Theta', \Phi'}{M.C, \Theta, \Phi \vdash \text{adds } AD : \Theta', \Phi'}$$

The two following rules, for removing a field or a method, build a constraint $\Phi'$ ensuring that, whenever the activation condition $\Phi$ of the delta containing the operation becomes **true**, then the attribute is present ($\Theta(M.C.x)$ holds). Moreover, they update $\Theta'$ to store the information that the attribute is no longer available after the operation is applied.

$$A:REMFD \frac{\Phi' = (\Phi \Rightarrow \Theta(M.N.x)) \quad \Theta' = \Theta[M.N.x \mapsto \Theta(M.N.x) \wedge (\neg \Phi)]}{M.N, \Theta, \Phi \vdash \text{removes } VT x; : \Theta', \Phi'}$$

$$A:REMMH \frac{\Phi' = (\Phi \Rightarrow \Theta(M.C.m)) \quad \Theta' = \Theta[M.C.m \mapsto \Theta(M.C.m) \wedge (\neg \Phi)]}{M.C, \Theta, \Phi \vdash \text{removes } VT m(\overline{VT x}) : \Theta', \Phi'}$$

The rule for modifying a method requires in the applicability constraint $\Phi'$ that the method must already be present (when activation condition $\Phi$ holds), but leaves the presence mapping unchanged:

$$A:ModM \frac{\Phi' = (\Phi \Rightarrow \Theta(M.C.m))}{M.C, \Theta, \Phi \vdash \text{modifies } VT m(\overline{VT x}) \{ \text{S return E} \} : \Theta, \Phi'}$$

The rules for delta operations on interfaces are similar to those for class operations:

$$A:ADDI \frac{M, \Theta, \Phi \vdash ID : \Theta', \Phi}{M, \Theta, \Phi \vdash \text{adds } ID : \Theta', \Phi}$$

$$A:REMI \frac{\Phi' = (\Phi \Rightarrow \Theta(M.I)) \quad \Theta' = \Theta[M.I \mapsto \Theta(M.I) \wedge (\neg \Phi)][M.I.a \mapsto \Theta(M.I.a) \wedge (\neg \Phi)][M.I.a \in \text{dom}(\Theta)]}{M, \Theta, \Phi \vdash \text{removes interface } I : \Theta', \Phi'}$$

$$A:ModI \frac{M.I, \Theta_{i-1}, \Phi \vdash HO_i : \Theta_i, \Phi_i \quad \Phi' = (\bigwedge_{1 \le i \le n} \Phi_i) \wedge (\Phi \Rightarrow \Theta(M.I))}{M, \Theta_0, \Phi \vdash \text{modifies interface } I \text{ adds } IR_1 \cdots IR_q \text{ removes } IR_1 \cdots IR_r \{ HO_1 \cdots HO_n \} : \Theta_n, \Phi'}$$

$$A:ADDMH \frac{M.I, \Theta, \Phi \vdash MH : \Theta', \Phi'}{M.I, \Theta, \Phi \vdash \text{adds } MH : \Theta', \Phi'}$$
## Appendix E. Proof of Theorem 2

The following lemmas analyze the applicability consistency rules. Rules are grouped according to the properties they ensure.

### E.1. Attributes

**Lemma 3 (Adding Attributes to Classes/interfaces).** Let Prg be a normal form ABS-VM program, let M be a module of Prg, and let Θ have domain ddom(M). Let M.N be a class/interface such that M.N, Θ, Φ ⊢ G : Θ', Φ' holds, where G ∈ {FD, MD, MH, adds AD, adds MH} (see Fig. 6). Let a be the attribute G is adding to M.N and let π be a product of M. Then, the following holds:

1. eval(π, Φ', Prg) = true if and only if eval(π, Φ, Prg) = true implies eval(π, Θ (M.N. a), Prg) = false.

2. eval(π, Θ' (M.N. a), Prg) = true if and only if either eval(π, Θ (M.N. a), Prg) = true or eval(π, Φ, Prg) = true. Moreover, Θ'(x) = Θ(x), for all x ∈ ddom(M) such that x ≠ M.N. a.

**Proof.** In these rules Φ is an activation condition (true for adding to the core), while Φ' is an applicability constraint. The proof is by verifying the statements for rules [A:FIELD], [A:METH], [A:MHEADER], [A:ADDA], [A:ADDMH]. □

**Lemma 4 (Removing Attributes from Classes/interfaces).** Let Prg be a normal form ABS-VM program, let M be a module of Prg, and let Θ have domain ddom(M). Let M.N be a class/interface such that M.N, Θ, Φ ⊢ G : Θ', Φ' holds, where G ∈ {removes HD, removes MH} (see Fig. 6). Let a be the attribute that G removes from M.N and let π be a product of M. Then, the following holds:

1. eval(π, Φ', Prg) = true if and only if eval(π, Φ, Prg) = true implies eval(π, Θ (M.N. a), Prg) = true.

2. eval(π, Θ' (M.N. a), Prg) = true if and only if both eval(π, Θ (M.N. a), Prg) = true and eval(π, Φ, Prg) = false. Moreover, Θ'(x) = Θ(x) for all x ∈ ddom(M) such that x ≠ M.N. a.

**Proof.** As before Φ is an activation condition (removing is never done in the core), while Φ' is an applicability constraint. The proof is by verifying the statements for the rules [A:REMD] and [A:REMMH]. □

**Lemma 5 (Modifying Methods in Classes).** Let Prg be a normal form ABS-VM program, let M be a module of Prg, and let Θ have domain ddom(M). Let M.C be a class such that M.C, Θ, Φ ⊢ modifies VT m (VT ϖ) { S return E; } : Θ', Φ' holds. If π is a product of M then the following holds:

1. eval(π, Φ', Prg) = true if and only if eval(π, Φ, Prg) = true implies eval(π, Θ (M.N.m), Prg) = true.

2. Θ' = Θ.

**Proof.** Here Φ is the activation condition of a delta. The proof is by verifying the statements for rule [A:MODM]. □

### E.2. Classes/interfaces

**Lemma 6 (Adding Classes/interfaces to Modules).** Let Prg be a normal form ABS-VM program, let M be a module of Prg, and let Θ have domain ddom(M). Assume M, Θ, Φ ⊢ G : Θ', Φ' holds, where G ∈ {CD, ID, adds CD, adds ID} (see Fig. 6). Let N be the class/interface that G is adding to M and let π be a product of M.

Consider {Z₁, ..., Zₘ}, where Zᵢ ∈ {FD, MD, MH} is the body of N, such that in the derivation of G above there are sub-derivations of M.I, Θᵢ₋₁, Φ ⊢ Zᵢ : Θᵢ, Φᵢ for 1 ≤ i ≤ m. Then, the following holds:

1. eval(π, Φ', Prg) = true if and only if eval(π, Λ₁₋ᵢ ≤ m Φᵢ, Prg) = true and eval(π, Φ, Prg) = true both imply that eval(π, Θ (M.N), Prg) = false.

2. eval(π, Θ' (M.N), Prg) = true if and only if either eval(π, Θ (M.N), Prg) = true or eval(π, Φ, Prg) = true. Moreover, Θ'(x) = Θₘ(x) for all x ∈ ddom(M) such that x ≠ M.N.

**Proof.** As before, Φ is an activation condition (and true in the core). The proof uses Lemma 3 on the derivation ending by rule applications [A:CLASS], [A:INTERFACE], [A:ADDC], [A:ADDI]. □

**Lemma 7 (Removing Classes/interfaces from Modules).** Let Prg be a normal form ABS-VM program, let M be a module of Prg, and let Θ have domain ddom(M). Assume M, Θ, Φ ⊢ G : Θ', Φ' holds, where G ∈ {removes class N, removes interface N}. Let N be the class/interface that G removes from M and let π be a product of M. Then, the following holds:

1. eval(π, Φ', Prg) = true if and only if eval(π, Φ, Prg) = true implies eval(π, Θ (M.N), Prg) = true.

2. eval(π, Θ' (M.N), Prg) = true if and only if both eval(π, Θ (M.N), Prg) = true and eval(π, Φ, Prg) = false.

3. For all M.N. q ∈ dom(Θ):
   eval(π, Φ' (M.N. q), Prg) = true if and only if both eval(π, Θ (M.N. q), Prg) = true and eval(π, Φ, Prg) = false. Moreover, for all x ∈ ddom(M) with x ∉ M.N ∪ {M.N.q | M.N.q ∈ dom(Θ)} we have Θ'(x) = Θₘ(x).

**Proof.** As before, Φ is an activation condition (no removal in the core). The proof is by verifying the statements for rules [A:REMC] and [A:REMI]. □

**Lemma 8 (Modifying Classes/interfaces in Modules).** Let Prg be a normal form ABS-VM program, M a module of Prg, and let Θ have domain ddom(M). Assume

$$M, \Theta, \Phi \vdash \underset{\text{interface } N}{\text{modifies}} \underset{\text{class } N}{\text{class } N} \quad [\text{adds...}][\text{removes...}] \\ \times \{\text{Op}_1 \cdots \text{Op}_n\} : \Theta', \Phi'$$

holds, where Opᵢ ∈ {AO, SO}. In the premise of this derivation are sub-derivations of M.I, Θᵢ₋₁, Φ ⊢ Opᵢ : Θᵢ, Φᵢ for 1 ≤ i ≤ m. If π is a product of M then the following holds:

1. eval(π, Φ', Prg) = true if and only if eval(π, Λ₁₋ᵢ ≤ n Φᵢ, Prg) = true and eval(π, Φ, Prg) = true both imply that eval(π, Θ (M.N), Prg) = true.

2. Θ' = Θₘ.

**Proof.** Here Φ is the activation condition of a delta. The proof uses Lemmas 3-5 on the derivation ending in applications of rules [A:MODC] and [A:MODI]. □

### E.3. Deltas and modules

**Lemma 9 (Applying Deltas, Building Modules).** Let Prg be a normal form ABS-VM program, let M be a module of Prg, and let Θ₀ have domain ddom(M). Assume one of the following cases applies:

* M, Θ₀ ⊢ delta M.D; CO₁···COₙ IOₙ₊₁···IOₘ : Θ', Φ' holds. Therefore, in the premises of this derivation we have M, Θᵢ₋₁, M.D ⊢ COᵢ : Θᵢ, Φᵢ for 1 ≤ i ≤ n and M, Θᵢ₋₁, M.D ⊢ IOᵢ : Θᵢ, Φᵢ for n + 1 ≤ i ≤ m.
# Appendix E. Proof of Theorem 2

The following lemmas analyze the applicability consistency rules. Rules are grouped according to the properties they ensure.

## E.1. Attributes

**Lemma 3 (Adding Attributes to Classes/interfaces).** Let Prg be a normal form ABS-VM program, let M be a module of Prg, and let $Θ$ have domain $ddom(M)$. Let $M.N$ be a class/interface such that $M.N, Θ, Φ ⊢ G : Θ', Φ'$ holds, where $G ∈ \{\text{FD}, \text{MD}, \text{MH}, \text{adds AD}, \text{adds MH}\}$ (see Fig. 6). Let a be the attribute $G$ is adding to $M.N$ and let $π$ be a product of M. Then, the following holds:

1. eval($π, Φ', Prg$) = true if and only if eval($π, Φ, Prg$) = true implies eval($π, Θ(M.N.a), Prg$) = false.

2. eval($π, Θ'(M.N.a), Prg$) = true if and only if either eval($π, Θ(M.N.a), Prg$) = true or eval($π, Φ, Prg$) = true. Moreover, $Θ'(x) = Θ(x)$, for all $x ∈ ddom(M)$ such that $x \neq M.N.a$.

**Proof.** In these rules $Φ$ is an activation condition (true for adding to the core), while $Φ'$ is an applicability constraint. The proof is by verifying the statements for rules [A:FIELD], [A:METH], [A:MHEADER], [A:ADDA], [A:ADDMH]. □

**Lemma 4 (Removing Attributes from Classes/interfaces).** Let Prg be a normal form ABS-VM program, let M be a module of Prg, and let $Θ$ have domain $ddom(M)$. Let $M.N$ be a class/interface such that $M.N, Θ, Φ ⊢ G : Θ', Φ'$ holds, where $G ∈ \{\text{removes HD}, \text{removes MH}\}$ (see Fig. 6). Let a be the attribute that $G$ removes from $M.N$ and let $π$ be a product of M. Then, the following holds:

1. eval($π, Φ', Prg$) = true if and only if eval($π, Φ, Prg$) = true implies eval($π, Θ(M.N.a), Prg$) = true.

2. eval($π, Θ'(M.N.a), Prg$) = true if and only if both eval($π, Θ(M.N.a), Prg$) = true and eval($π, Φ, Prg$) = false. Moreover, $Θ'(x) = Θ(x)$ for all $x ∈ ddom(M)$ such that $x \neq M.N.a$.

**Proof.** As before $Φ$ is an activation condition (removing is never done in the core), while $Φ'$ is an applicability constraint. The proof is by verifying the statements for the rules [A:REMD] and [A:REMMH]. □

**Lemma 5 (Modifying Methods in Classes).** Let Prg be a normal form ABS-VM program, let M be a module of Prg, and let $Θ$ have domain $ddom(M)$. Let $M.C$ be a class such that $M.C, Θ, Φ ⊢ modifies VTm(VT$\bar{V}$$\bar{V}$) { S return E; } : Θ', Φ' holds. If $π$ is a product of M then the following holds:

1. eval($π, Φ', Prg$) = true if and only if eval($π, Φ, Prg$) = true implies eval($π, Θ(M.N.m), Prg$) = true.

2. $Θ' = Θ$.

**Proof.** Here $Φ$ is the activation condition of a delta. The proof is by verifying the statements for rule [A:MODM]. □

## E.2. Classes/interfaces

**Lemma 6 (Adding Classes/interfaces to Modules).** Let Prg be a normal form ABS-VM program, let M be a module of Prg, and let $Θ$ have domain $ddom(M)$. Assume $M, Θ, Φ ⊢ G : Θ', Φ'$ holds, where $G ∈ \{\text{CD}, \text{ID}, \text{adds CD}, \text{adds ID}\}$ (see Fig. 6). Let N be the class/interface that $G$ is adding to M and let $π$ be a product of M.

Consider $\{Z_1, \dots, Z_m\}$, where $Z_i \in \{\text{FD}, \text{MD}, \text{MH}\}$ is the body of $N$, such that in the derivation of $G$ above there are sub-derivations of $M.I, Θ_{i-1}, Φ \vdash Z_i : Θ_i, Φ_i$ for $1 \le i \le m$. Then, the following holds:

1. eval($π, Φ', Prg$) = true if and only if eval($π, \bigwedge_{1 \le i \le m} Φ_i, Prg$) = true and eval($π, Φ, Prg$) = true both imply that eval($π, Θ(M.N), Prg$) = false.

2. eval($π, Θ'(M.N), Prg$) = true if and only if either eval($π, Θ(M.N), Prg$) = true or eval($π, Φ, Prg$) = true. Moreover, $Θ'(x) = Θ_m(x)$ for all $x \in ddom(M)$ such that $x \neq M.N$.

**Proof.** As before, $Φ$ is an activation condition (and true in the core). The proof uses Lemma 3 on the derivation ending by rule applications [A:CLASS], [A:INTERFACE], [A:ADDC], [A:ADDI]. □

**Lemma 7 (Removing Classes/interfaces from Modules).** Let Prg be a normal form ABS-VM program, let M be a module of Prg, and let $Θ$ have domain $ddom(M)$. Assume $M, Θ, Φ ⊢ G : Θ', Φ'$ holds, where $G ∈ \{\text{removes class N}, \text{removes interface N}\}$. Let N be the class/interface that $G$ removes from M and let $π$ be a product of M. Then, the following holds:

1. eval($π, Φ', Prg$) = true if and only if eval($π, Φ, Prg$) = true implies eval($π, Θ(M.N), Prg$) = true.

2. eval($π, Θ'(M.N), Prg$) = true if and only if both eval($π, Θ(M.N), Prg$) = true and eval($π, Φ, Prg$) = false.

3. For all $M.N.q \in dom(Θ)$: eval($π, Φ'(M.N.q), Prg$) = true if and only if both eval($π, Θ(M.N.q), Prg$) = true and eval($π, Φ, Prg$) = false. Moreover, for all $x \in ddom(M)$ with $x \notin M.N \cup \{M.N.q | M.N.q \in dom(Θ)\}$ we have $Θ'(x) = Θ_m(x)$.

**Proof.** As before, $Φ$ is an activation condition (no removal in the core). The proof is by verifying the statements for rules [A:REMC] and [A:REMI]. □

**Lemma 8 (Modifying Classes/interfaces in Modules).** Let Prg be a normal form ABS-VM program, M a module of Prg, and let $Θ$ have domain $ddom(M)$. Assume

$$ M, Θ, Φ \vdash \underset{\text{interface N}}{\text{modifies}} \underset{\text{class N}}{\text{class N}} \quad [\text{adds...}][\text{removes...}] \\ \times \{Op_1 \cdots Op_n\} : Θ', Φ' $$

holds, where $Op_i \in \{\text{AO}, \text{SO}\}$. In the premise of this derivation are sub-derivations of $M.I, Θ_{i-1}, Φ \vdash Op_i : Θ_i, Φ_i$ for $1 \le i \le m$. If $π$ is a product of M then the following holds:

1. eval($π, Φ', Prg$) = true if and only if eval($π, \bigwedge_{1 \le i \le n} Φ_i, Prg$) = true and eval($π, Φ, Prg$) = true both imply that eval($π, Θ(M.N), Prg$) = true.

2. $Θ' = Θ_n$.

**Proof.** Here $Φ$ is the activation condition of a delta. The proof uses Lemmas 3–5 on the derivation ending in applications of rules [A:MODC] and [A:MODI]. □

## E.3. Deltas and modules

**Lemma 9 (Applying Deltas, Building Modules).** Let Prg be a normal form ABS-VM program, let M be a module of Prg, and let $Θ_0$ have domain $ddom(M)$. Assume one of the following cases applies:

* $M, Θ_0 \vdash \text{delta } M.D; C0_1 \cdots C0_n \vdash IO_{n+1} \cdots IO_m : Θ', Φ'$ holds. Therefore, in the premises of this derivation we have $M, Θ_{i-1}, M.D \vdash C0_i : Θ_i, Φ_i$ for $1 \le i \le n$ and $M, Θ_{i-1}, M.D \vdash IO_i : Θ_i, Φ_i$ for $n+1 \le i \le m$.
* $\vdash$ module *M*; ... Defn₁... Defnₙ [ init{S} ] Dltₙ₁+₁... Dltₘ CK : Θ', Φ' holds. Therefore, in the premises of this derivation we find:

1. $\Theta_0 = [q \mapsto \text{false}]_{q \in \text{dom}(M)}$

2. $M, \Theta_{i-1}, \text{true} \vdash \text{Defn}_i : \Theta_i, \Phi_i \text{ for } 1 \le i \le n$

3. $M, \Theta_{i-1} \vdash Dlt_i : \Theta_i, \Phi_i \text{ for } n+1 \le i \le m$

If $\pi$ is a product of $M$ then the following holds:

1. $\text{eval}(\pi, \Phi', \text{Prg}) = \text{true}$ if and only if $\text{eval}(\pi, \Phi_i, \text{Prg}) = \text{true}$ for all $i$ such that $1 \le i \le m$.

2. $\Theta' = \Theta_m$.

**Proof.** The proof of the first case uses Lemmas 6-8 on the derivation ending with application of rule [A:DELTA]. The proof of the second case uses the first case and Lemma 6 on the derivation ending with application of rule [A:MODULE]. □

## References

Alouneh, S., Abed, S., Shayej, M.H.A., Mesleh, R., 2019. A comprehensive study and analysis on SAT-solvers: advances, usages and achievements. Artif. Intell. Rev. 52, 2575-2601.

Apel, S., Batory, D.S., Kästner, C., Saake, G., 2013. Feature-Oriented Software Product Lines: Concepts and Implementation. Springer.

Batory, D., 2005. Feature models, grammars, and propositional formulas. In: Proceedings of International Software Product Line Conference. SPLC. In: LNCS, vol. 3714, Springer, pp. 7-20. http://dx.doi.org/10.1007/11554844_3.

Batory, D., Sarvela, J.N., Rauschmayer, A., 2004. Scaling step-wise refinement. IEEE Trans. Softw. Eng. 30, 355-371. http://dx.doi.org/10.1109/TSE.2004.23.

Bettini, L., Damiani, F., 2017. Xtraitj: Traits for the Java platform. J. Syst. Softw. 131, 419-441. http://dx.doi.org/10.1016/j.jss.2016.07.035.

Bettini, L., Damiani, F., Schaefer, I., 2013a. Compositional type checking of delta-oriented software product lines. Acta Inform. 50 (2), 77-122. http://dx.doi.org/10.1007/s00236-012-0173-z.

Bettini, L., Damiani, F., Schaefer, I., Strocco, F., 2013b. TraitRecord: A programming language with traits and records. Sci. Comput. Program. 78 (5), 521-541. http://dx.doi.org/10.1016/j.scico.2011.06.007.

Bono, V., Damiani, F., Giachino, E., 2008. On traits and types in a java-like setting. In: Fifth IFIP International Conference on Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, TC 1, Foundations of Computer Science, September 7-10, 2008, Milano, Italy. pp. 367-382. http://dx.doi.org/10.1007/978-0-387-09680-3_25.

Bracha, G., 1992. The Programming Language JIGSAW: Mixins, Modularity and Multiple Inheritance (Ph.D. thesis). Department of Comp. Sci., Univ. of Utah.

Cardelli, L., 1997. Program fragments, linking, and modularization. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL '97, ACM, New York, NY, USA, pp. 266-277. http://dx.doi.org/10.1145/263699.263735, URL: http://doi.acm.org/10.1145/263699.263735.

Clarke, D., Muschevici, R., Proença, J., Schaefer, I., Schlatte, R., 2010. Variability modelling in the ABS language. In: FMCO. In: LNCS, vol. 6957, Springer, pp. 204-224. http://dx.doi.org/10.1007/978-3-642-25271-6_11.

Clements, P., Northrop, L., 2001. Software Product Lines: Practices & Patterns. Addison Wesley Longman.

Czarnecki, K., Eisenecker, U.W., 2000. Generative Programming: Methods, Tools, and Applications. Addison-Wesley.

Damiani, F., Hähnle, R., Kamburjan, E., Lienhardt, M., 2017a. A unified and formal programming model for deltas and traits. In: FASE. In: LNCS, vol. 10202, Springer, pp. 424-441. http://dx.doi.org/10.1007/978-3-662-54494-5_25.

Damiani, F., Hähnle, R., Kamburjan, E., Lienhardt, M., 2018a. Interoperability of software product line variants. In: SPLC. ACM, pp. 264-268. http://dx.doi.org/10.1145/3233027.3236401.

Damiani, F., Hähnle, R., Kamburjan, E., Lienhardt, M., 2018b. Same same but different: Interoperability of software product line variants. In: Principled Software Development. Springer, pp. 99-117. http://dx.doi.org/10.1007/978-3-319-98047-8_7.

Damiani, F., Hähnle, R., Kamburjan, E., Lienhardt, M., Paolini, L., 2021. Variability modules for Java-like languages. In: Mousavi, M., Schobbens, P. (Eds.), Proc. 25th ACM Intl. Systems and Software Product Line Conf., Volume A. ACM, New York, NY, USA, pp. 1-12. http://dx.doi.org/10.1145/3461001.3471143.

Damiani, F., Lienhardt, M., 2016. On type checking delta-oriented product lines. In: Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings. In: LNCS, vol. 9681, Springer, pp. 47-62. http://dx.doi.org/10.1007/978-3-319-33693-0_4.

Damiani, F., Lienhardt, M., Muschevici, R., Schaefer, I., 2017b. An extension of the ABS toolchain with a mechanism for type checking SPLs. In: Integrated Formal Methods, 13th Intl. Conf., IFM, Turin, Italy. In: LNCS, vol. 10510, Springer, pp. 111-126. http://dx.doi.org/10.1007/978-3-319-66845-1_8.

Damiani, F., Lienhardt, M., Paolini, L., 2019. A formal model for multi software product lines. Sci. Comput. Program. 172, 203-231. http://dx.doi.org/10.1016/j.scico.2018.11.005.

Damiani, F., Schaefer, I., 2012. Family-based analysis of type safety for delta-oriented software product lines. In: Margaria, T., Steffen, B. (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. In: LNCS, vol. 7609, Springer Berlin Heidelberg, pp. 193-207. http://dx.doi.org/10.1007/978-3-642-34026-0_15.

Damiani, F., Schaefer, I., Schuster, S., Winkelmann, T., 2014a. Delta-trait programming of software product lines. In: Margaria, T., Steffen, B. (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 289-303. http://dx.doi.org/10.1007/978-3-662-45234-9_21.

Damiani, F., Schaefer, I., Winkelmann, T., 2014b. Delta-oriented multi software product lines. In: Proceedings of the 18th International Software Product Line Conference - Volume 1. SPLC '14, ACM, pp. 232-236. http://dx.doi.org/10.1145/2648511.2648536.

Delaware, B., Cook, W.R., Batory, D., 2009. Fitting the pieces together: A machine-checked model of safe composition. In: ESEC/FSE. ACM, pp. 243-252. http://dx.doi.org/10.1145/1595696.1595733.

Ducasse, S., Nierstrasz, O., Schärli, N., Wuyts, R., Black, A.P., 2006. Traits: A mechanism for fine-grained reuse. ACM Trans. Program. Lang. Syst. 28 (2), 331-388. http://dx.doi.org/10.1145/1119479.1119483.

Hähnle, R., 2013. The abstract behavioral specification language: A tutorial introduction. In: Bonsangue, M., de Boer, F., Giachino, E., Hähnle, R. (Eds.), Intl. School on Formal Models for Components and Objects: Post Proceedings. In: LNCS, vol. 7866, Springer, pp. 1-37. http://dx.doi.org/10.1007/978-3-642-40615-7_1.

Holl, G., Grünbacher, P., Rabiser, R., 2012. A systematic review and an expert survey on capabilities supporting multi product lines. In: Softw. Technol. 54 (8), 828-852. http://dx.doi.org/10.1016/j.insoft.2012.02.002. URL: http://www.sciencedirect.com/science/article/pii/S095058491200033X.

Igarashi, A., Pierce, B.C., Wadler, P., 1999. Featherweight Java: A minimal core calculus for Java and GJ. In: Hailpern, B., Northrop, L.M., Berman, A.M. (Eds.), Proc. ACM SIGPLAN Conf. on Object-Oriented Programming Systems, Languages & Applications (OOPSLA), Denver, Colorado, USA. ACM, pp. 132-146. http://dx.doi.org/10.1145/320384.320395.

Igarashi, A., Pierce, B., Wadler, P., 2001. Featherweight Java: A minimal core calculus for Java and GJ. ACM TOPLAS 23 (3), 396-450. http://dx.doi.org/10.1145/503502.503505.

Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M., 2010. ABS: A core language for abstract behavioral specification. In: Formal Methods for Components and Objects - 9th International Symposium, FMCO 2010, Graz, Austria, November 29 - December 1, 2010. Revised Papers. pp. 142-164. http://dx.doi.org/10.1007/978-3-642-25271-6_8.

Kamburjan, E., Hähnle, R., 2016. Uniform modeling of railway operations. In: FTSCS. In: Communications in Computer and Information Science, vol. 694, pp. 55-71. http://dx.doi.org/10.1007/978-3-319-53946-1_4.

Kamburjan, E., Hähnle, R., 2018. Prototyping formal system models with active objects. In: Bartoletti, M., Knight, S. (Eds.), Proceedings 11th Interaction and Concurrency Experience, ICE 2018, Madrid, Spain, June 20-21, 2018. In: EPTCS, vol. 279, pp. 52-67. http://dx.doi.org/10.4204/EPTCS.279.7.

Kamburjan, E., Hähnle, R., Schön, S., 2018. Formal modeling and analysis of railway operations with active objects. Sci. Comput. Program. 166, 167-193. http://dx.doi.org/10.1016/j.scico.2018.07.001.

Kästner, C., Apel, S., Thüm, T., Saake, G., 2012a. Type checking annotation-based product lines. ACM Trans. Softw. Eng. Methodol. 21 (3), http://dx.doi.org/10.1145/2211616.2211617.

Kästner, C., Ostermann, K., Erdweg, S., 2012b. A variability-aware module system. In: Leavens, G.T., Dwyer, M.B. (Eds.), Proc. ACM International Conference on Object Oriented Programming Systems Languages and Applications. OOPSLA '12, ACM, New York, NY, USA, pp. 773-792. http://dx.doi.org/10.1145/2384616.2384673.

Koscielny, J., Holthusen, S., Schaefer, I., Schulze, S., Bettini, L., Damiani, F., 2014. Deltaj 1.5: delta-oriented programming for Java 1.5. In: Kolodziej, J., Childers, B.R. (Eds.), Intl. Conf. on Principles and Practices of Programming on the Java Platform Virtual Machines, Languages and Tools, PPPJ, Cracow, Poland. ACM, pp. 63-74. http://dx.doi.org/10.1145/2647508.

Lagorio, G., Servetto, M., Zucca, E., 2009. Featherweight Jigsaw: A minimal core calculus for modular composition of classes. In: Proceedings of the 23rd European Conference on ECOOP 2009 - Object-Oriented Programming. Springer-Verlag, Berlin, Heidelberg, pp. 244-268. http://dx.doi.org/10.1007/978-3-642-03013-0_12.

Lagorio, G., Servetto, M., Zucca, E., 2012. Featherweight Jigsaw - Replacing inheritance by composition in Java-like languages. Inform. and Comput. 214, 86-111. http://dx.doi.org/10.1016/j.ic.2012.02.004.
* $\vdash$ module *M*; ... Defn₁... Defnₙ [ init{S} ] Dltₙ₁+₁... Dltₘ CK : Θ', Φ' holds. Therefore, in the premises of this derivation we find:

1. $\Theta_0 = [q \mapsto \text{false}]_{q \in \text{dom}(M)}$

2. $M, \Theta_{i-1}, \text{true} \vdash \text{Defn}_i : \Theta_i, \Phi_i \text{ for } 1 \le i \le n$

3. $M, \Theta_{i-1} \vdash Dlt_i : \Theta_i, \Phi_i \text{ for } n+1 \le i \le m$

If $\pi$ is a product of $M$ then the following holds:

1. $\text{eval}(\pi, \Phi', \text{Prg}) = \text{true}$ if and only if $\text{eval}(\pi, \Phi_i, \text{Prg}) = \text{true}$ for all $i$ such that $1 \le i \le m$.

2. $\Theta' = \Theta_m$.

**Proof.** The proof of the first case uses Lemmas 6-8 on the derivation ending with application of rule [A:DELTA]. The proof of the second case uses the first case and Lemma 6 on the derivation ending with application of rule [A:MODULE]. □

## References

Alouneh, S., Abed, S., Shayej, M.H.A., Mesleh, R., 2019. A comprehensive study and analysis on SAT-solvers: advances, usages and achievements. Artif. Intell. Rev. 52, 2575-2601.

Apel, S., Batory, D.S., Kästner, C., Saake, G., 2013. Feature-Oriented Software Product Lines: Concepts and Implementation. Springer.

Batory, D., 2005. Feature models, grammars, and propositional formulas. In: Proceedings of International Software Product Line Conference. SPLC. In: LNCS, vol. 3714, Springer, pp. 7-20. http://dx.doi.org/10.1007/11554844_3.

Batory, D., Sarvela, J.N., Rauschmayer, A., 2004. Scaling step-wise refinement. IEEE Trans. Softw. Eng. 30, 355-371. http://dx.doi.org/10.1109/TSE.2004.23.

Bettini, L., Damiani, F., 2017. Xtraitj: Traits for the Java platform. J. Syst. Softw. 131, 419-441. http://dx.doi.org/10.1016/j.jss.2016.07.035.

Bettini, L., Damiani, F., Schaefer, I., 2013a. Compositional type checking of delta-oriented software product lines. Acta Inform. 50 (2), 77-122. http://dx.doi.org/10.1007/s00236-012-0173-z.

Bettini, L., Damiani, F., Schaefer, I., Strocco, F., 2013b. TraitRecord: A programming language with traits and records. Sci. Comput. Program. 78 (5), 521-541. http://dx.doi.org/10.1016/j.scico.2011.06.007.

Bono, V., Damiani, F., Giachino, E., 2008. On traits and types in a java-like setting. In: Fifth IFIP International Conference on Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, TC 1, Foundations of Computer Science, September 7-10, 2008, Milano, Italy. pp. 367-382. http://dx.doi.org/10.1007/978-0-387-09680-3_25.

Bracha, G., 1992. The Programming Language JIGSAW: Mixins, Modularity and Multiple Inheritance (Ph.D. thesis). Department of Comp. Sci., Univ. of Utah.

Cardelli, L., 1997. Program fragments, linking, and modularization. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL '97, ACM, New York, NY, USA, pp. 266-277. http://dx.doi.org/10.1145/263699.263735, URL: http://doi.acm.org/10.1145/263699.263735.

Clarke, D., Muschevici, R., Proença, J., Schaefer, I., Schlatte, R., 2010. Variability modelling in the ABS language. In: FMCO. In: LNCS, vol. 6957, Springer, pp. 204-224. http://dx.doi.org/10.1007/978-3-642-25271-6_11.

Clements, P., Northrop, L., 2001. Software Product Lines: Practices & Patterns. Addison Wesley Longman.

Czarnecki, K., Eisenecker, U.W., 2000. Generative Programming: Methods, Tools, and Applications. Addison-Wesley.

Damiani, F., Hähnle, R., Kamburjan, E., Lienhardt, M., 2017a. A unified and formal programming model for deltas and traits. In: FASE. In: LNCS, vol. 10202, Springer, pp. 424-441. http://dx.doi.org/10.1007/978-3-662-54494-5_25.

Damiani, F., Hähnle, R., Kamburjan, E., Lienhardt, M., 2018a. Interoperability of software product line variants. In: SPLC. ACM, pp. 264-268. http://dx.doi.org/10.1145/3233027.3236401.

Damiani, F., Hähnle, R., Kamburjan, E., Lienhardt, M., 2018b. Same same but different: Interoperability of software product line variants. In: Principled Software Development. Springer, pp. 99-117. http://dx.doi.org/10.1007/978-3-319-98047-8_7.

Damiani, F., Hähnle, R., Kamburjan, E., Lienhardt, M., Paolini, L., 2021. Variability modules for Java-like languages. In: Mousavi, M., Schobbens, P. (Eds.), Proc. 25th ACM Intl. Systems and Software Product Line Conf., Volume A. ACM, New York, NY, USA, pp. 1-12. http://dx.doi.org/10.1145/3461001.3471143.

Damiani, F., Lienhardt, M., 2016. On type checking delta-oriented product lines. In: Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings. In: LNCS, vol. 9681, Springer, pp. 47-62. http://dx.doi.org/10.1007/978-3-319-33693-0_4.

Damiani, F., Lienhardt, M., Muschevici, R., Schaefer, I., 2017b. An extension of the ABS toolchain with a mechanism for type checking SPLs. In: Integrated Formal Methods, 13th Intl. Conf., IFM, Turin, Italy. In: LNCS, vol. 10510, Springer, pp. 111-126. http://dx.doi.org/10.1007/978-3-319-66845-1_8.

Damiani, F., Lienhardt, M., Paolini, L., 2019. A formal model for multi software product lines. Sci. Comput. Program. 172, 203-231. http://dx.doi.org/10.1016/j.scico.2018.11.005.

Damiani, F., Schaefer, I., 2012. Family-based analysis of type safety for delta-oriented software product lines. In: Margaria, T., Steffen, B. (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. In: LNCS, vol. 7609, Springer Berlin Heidelberg, pp. 193-207. http://dx.doi.org/10.1007/978-3-642-34026-0_15.

Damiani, F., Schaefer, I., Schuster, S., Winkelmann, T., 2014a. Delta-trait programming of software product lines. In: Margaria, T., Steffen, B. (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 289-303. http://dx.doi.org/10.1007/978-3-662-45234-9_21.

Damiani, F., Schaefer, I., Winkelmann, T., 2014b. Delta-oriented multi software product lines. In: Proceedings of the 18th International Software Product Line Conference - Volume 1. SPLC '14, ACM, pp. 232-236. http://dx.doi.org/10.1145/2648511.2648536.

Delaware, B., Cook, W.R., Batory, D., 2009. Fitting the pieces together: A machine-checked model of safe composition. In: ESEC/FSE. ACM, pp. 243-252. http://dx.doi.org/10.1145/1595696.1595733.

Ducasse, S., Nierstrasz, O., Schärli, N., Wuyts, R., Black, A.P., 2006. Traits: A mechanism for fine-grained reuse. ACM Trans. Program. Lang. Syst. 28 (2), 331-388. http://dx.doi.org/10.1145/1119479.1119483.

Hähnle, R., 2013. The abstract behavioral specification language: A tutorial introduction. In: Bonsangue, M., de Boer, F., Giachino, E., Hähnle, R. (Eds.), Intl. School on Formal Models for Components and Objects: Post Proceedings. In: LNCS, vol. 7866, Springer, pp. 1-37. http://dx.doi.org/10.1007/978-3-642-40615-7_1.

Holl, G., Grünbacher, P., Rabiser, R., 2012. A systematic review and an expert survey on capabilities supporting multi product lines. In: Softw. Technol. 54 (8), 828-852. http://dx.doi.org/10.1016/j.insoft.2012.02.002. URL: http://www.sciencedirect.com/science/article/pii/S095058491200033X.

Igarashi, A., Pierce, B.C., Wadler, P., 1999. Featherweight Java: A minimal core calculus for Java and GJ. In: Hailpern, B., Northrop, L.M., Berman, A.M. (Eds.), Proc. ACM SIGPLAN Conf. on Object-Oriented Programming Systems, Languages & Applications (OOPSLA), Denver, Colorado, USA. ACM, pp. 132-146. http://dx.doi.org/10.1145/320384.320395.

Igarashi, A., Pierce, B., Wadler, P., 2001. Featherweight Java: A minimal core calculus for Java and GJ. ACM TOPLAS 23 (3), 396-450. http://dx.doi.org/10.1145/503502.503505.

Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M., 2010. ABS: A core language for abstract behavioral specification. In: Formal Methods for Components and Objects - 9th International Symposium, FMCO 2010, Graz, Austria, November 29 - December 1, 2010. Revised Papers. pp. 142-164. http://dx.doi.org/10.1007/978-3-642-25271-6_8.

Kamburjan, E., Hähnle, R., 2016. Uniform modeling of railway operations. In: FTSCS. In: Communications in Computer and Information Science, vol. 694, pp. 55-71. http://dx.doi.org/10.1007/978-3-319-53946-1_4.

Kamburjan, E., Hähnle, R., 2018. Prototyping formal system models with active objects. In: Bartoletti, M., Knight, S. (Eds.), Proceedings 11th Interaction and Concurrency Experience, ICE 2018, Madrid, Spain, June 20-21, 2018. In: EPTCS, vol. 279, pp. 52-67. http://dx.doi.org/10.4204/EPTCS.279.7.

Kamburjan, E., Hähnle, R., Schön, S., 2018. Formal modeling and analysis of railway operations with active objects. Sci. Comput. Program. 166, 167-193. http://dx.doi.org/10.1016/j.scico.2018.07.001.

Kästner, C., Apel, S., Thüm, T., Saake, G., 2012a. Type checking annotation-based product lines. ACM Trans. Softw. Eng. Methodol. 21 (3), http://dx.doi.org/10.1145/2211616.2211617.

Kästner, C., Ostermann, K., Erdweg, S., 2012b. A variability-aware module system. In: Leavens, G.T., Dwyer, M.B. (Eds.), Proc. ACM International Conference on Object Oriented Programming Systems Languages and Applications. OOPSLA '12, ACM, New York, NY, USA, pp. 773-792. http://dx.doi.org/10.1145/2384616.2384673.

Koscielny, J., Holthusen, S., Schaefer, I., Schulze, S., Bettini, L., Damiani, F., 2014. Deltaj 1.5: delta-oriented programming for Java 1.5. In: Kolodziej, J., Childers, B.R. (Eds.), Intl. Conf. on Principles and Practices of Programming on the Java Platform Virtual Machines, Languages and Tools, PPPJ, Cracow, Poland. ACM, pp. 63-74. http://dx.doi.org/10.1145/2647508.

Lagorio, G., Servetto, M., Zucca, E., 2009. Featherweight Jigsaw: A minimal core calculus for modular composition of classes. In: Proceedings of the 23rd European Conference on ECOOP 2009 - Object-Oriented Programming. Springer-Verlag, Berlin, Heidelberg, pp. 244-268. http://dx.doi.org/10.1007/978-3-642-03013-0_12.

Lagorio, G., Servetto, M., Zucca, E., 2012. Featherweight Jigsaw - Replacing inheritance by composition in Java-like languages. Inform. and Comput. 214, 86-111. http://dx.doi.org/10.1016/j.ic.2012.02.004.
Lienhardt, M., Clarke, D., 2012. Conflict detection in delta-oriented programming. In: IsoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, Part I. In: LNCS, vol. 7609, Springer, pp. 178-192. http://dx.doi.org/10.1007/978-3-642-34026-0_14.

Liquori, L., Spiwack, A., 2008. Feathertrait: A modest extension of featherweight
java. ACM Trans. Program. Lang. Syst. 30 (2), 11:1-11:32. http://dx.doi.org/
10.1145/1330017.1330022.

Mauliadi, R., Setyautami, M.R.A., Afriyanti, I., Azurat, A., 2017. A platform for charities system generation with SPL approach. In: Proc. Intl. Conf. on Information Technology Systems and Innovation. ICITSI, IEEE, New York, NY, USA, pp. 108-113. http://dx.doi.org/10.1109/ICITSI.2017.8267927.

Mikhajlov, L., Sekerinski, E., 1998. A study of the fragile base class problem. In: ECOOP'98. In: LNCS, vol. 1445, pp. 355-383, cited By 1.

Nierstrasz, O., Ducasse, S., Schärli, N., 2006. Flattening traits. J. Object Technol. 5 (4), 129-148. http://dx.doi.org/10.5381/jot.2006.5.4.a4.

Pohl, K., Böckle, G., van der Linden, F., 2005. Software Product Line Engineering - Foundations, Principles, and Techniques. Springer, Berlin, Germany.

Reppy, J.H., Turon, A., 2007. Metaprogramming with traits. In: Ernst, E. (Ed.), ECOOP 2007 - Object-Oriented Programming, 21st European Conference, Berlin, Germany, July 30 - August 3, 2007, Proceedings. In: Lecture Notes in Computer Science, vol. 4609, Springer, pp. 373-398. http://dx.doi.org/10.1007/978-3-540-73589-2_18.

Roffe, A.J., Calderon, J.S.T., 2021. Random formula generators. CoRR abs/2110.09228. URL: https://arxiv.org/abs/2110.09228. arXiv:2110.09228.

Roman, S., 2008. Lattices and Ordered Sets. Springer New York, URL: https://books.google.it/books?id=NZN8aum26LgC.

Schaefer, I., Bettini, L., Bono, V., Damiani, F., Tanzarella, N., 2010. Delta-oriented programming of software product lines. In: Software Product Lines: Going beyond (SPLC 2010). In: LNCS, vol. 6287, pp. 77-91. http://dx.doi.org/10.1007/978-3-642-15579-6_6.

Schaefer, I., Damiani, F., 2010. Pure delta-oriented programming. In: Proceedings of the 2nd International Workshop on Feature-Oriented Software Development. FOSD '10, ACM, pp. 49-56. http://dx.doi.org/10.1145/1868688.1868696.

Schaefer, I., Rabiser, R., Clarke, D., Bettini, L., Benavides, D., Botterweck, G., Pathak, A., Trujillo, S., Villela, K., 2012. Software diversity. Int. J. Softw. Tools Technol. Transf. 14 (5), 477-495. http://dx.doi.org/10.1007/s10009-012-0253-y.

Schärli, N., Ducasse, S., Nierstrasz, O., Black, A.P., 2003. Traits: Composable units of behaviour. In: Cardelli, L. (Ed.), ECOOP 2003 - Object-Oriented Programming, 17th European Conference, Darmstadt, Germany, July 21-25, 2003, Proceedings. In: LNCS, vol. 2743, Springer, pp. 248-274. http://dx.doi.org/10.1007/978-3-540-45070-2_12.

Schröter, R., Krieter, S., Thüm, T., Benduhn, F., Saake, G., 2016. Feature-model interfaces: The highway to compositional analyses of highly-configurable systems. In: Proceedings of the 38th International Conference on Software Engineering. ICSE '16, ACM, pp. 667-678. http://dx.doi.org/10.1145/2884781.2884823.

Schröter, R., Siegmund, N., Thüm, T., 2013a. Towards modular analysis of multi product lines. In: Proceedings of the 17th International Software Product Line Conference Co-Located Workshops. SPLC '13, ACM, pp. 96-99. http://dx.doi.org/10.1145/2499777.2500719.

Schröter, R., Thüm, T., Siegmund, N., Saake, G., 2013b. Automated analysis of dependent feature models. In: The Seventh International Workshop on Variability Modelling of Software-Intensive Systems, VaMoS '13, Pisa, Italy, January 23 - 25, 2013. pp. 9:1-9:5. http://dx.doi.org/10.1145/2430502.2430515.

Setyautami, M.R.A., Adianto, D., Azurat, A., 2018. Modeling multi software product lines using UML. In: Proc. 22nd Intl. Systems and Software Product Line Conference, Vol. 1. ACM, New York, NY, USA, pp. 274-278. http://dx.doi.org/10.1145/3233027.3236400.

Setyautami, M.R.A., Hähnle, R., 2021. An architectural pattern to realize multi software product lines in Java. In: Grünbacher, P., Seidl, C., Dhungana, D., Lovasz-Bukvova, H. (Eds.), Proc. 15th Intl. Working Conf. on Variability Modelling of Software-Intensive Systems, Krems, Austria. ACM Press, pp. 9:1-9:9. http://dx.doi.org/10.1145/3442391.3442401.

Setyautami, M.R.A., Rubiantoro, R.R., Azurat, A., 2019. Model-driven engineering for delta-oriented software product lines. In: 26th Asia-Pacific Software Engineering Conf., APSEC, Putrajaya, Malaysia. IEEE, pp. 371-377. http://dx.doi.org/10.1109/APSEC48747.2019.00057.

Smith, C., Drossopoulou, S., 2005. Chai: Traits for java-like languages. In: Black, A.P. (Ed.), ECOOP 2005 - Object-Oriented Programming. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 453-478. http://dx.doi.org/10.1007/115311420_20.

Strniša, R., Sewell, P., Parkinson, M., 2007. The Java module system: Core design and semantic definition. In: Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications. OOPSLA '07, Association for Computing Machinery, New York, NY, USA, pp. 499-514. http://dx.doi.org/10.1145/1297027.1297064.

Thaker, S., Batory, D., Kitchin, D., Cook, W., 2007. Safe composition of product lines. In: Proceedings of the 6th International Conference on Generative Programming and Component Engineering. GPCE '07, ACM, New York, NY, USA, pp. 95-104. http://dx.doi.org/10.1145/1289971.1289989.

Thüm, T., Apel, S., Kästner, C., Schaefer, I., Saake, G., 2014. A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47 (1), 6:1-6:45. http://dx.doi.org/10.1145/2580950.

Trujillo-Tzanahua, G.I., Juárez-Martínez, U., Aguilar-Lasserre, A.A., Cortés-Verdín, M.K., 2018. Multiple software product lines: applications and challenges. In: Mejia, J., Muñoz, M., Rocha, A., Quiñonez, Y., Calvo-Manzano, J. (Eds.), Trends and Applications in Software Engineering. Springer International Publishing, Cham, pp. 117-126. http://dx.doi.org/10.1007/978-3-319-69341-5_11.

Wirth, N., 1980. The module: A system structuring facility in high-level programming languages. In: Tobias, J.M. (Ed.), Language Design and Programming Methodology. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 1-24. http://dx.doi.org/10.1007/3-540-09745-7_1.

Wong, P.Y.H., Diakov, N., Schaefer, I., 2012. Modelling distributed adaptable object oriented systems using HATS approach: A fredhopper case study (invited paper). In: Beckert, B., Damiani, F., Gurov, D. (Eds.), 2nd Intl. Conf. on Formal Verification of Object-Oriented Software, Torino, Italy. In: LNCS, vol. 7421, Springer, pp. 49-66. http://dx.doi.org/10.1007/978-3-642-31762-0_5.
Lienhardt, M., Clarke, D., 2012. Conflict detection in delta-oriented programming. In: IsoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, Part I. In: LNCS, vol. 7609, Springer, pp. 178-192. http://dx.doi.org/10.1007/978-3-642-34026-0_14.

Liquori, L., Spiwack, A., 2008. Feathertrait: A modest extension of featherweight
java. ACM Trans. Program. Lang. Syst. 30 (2), 11:1-11:32. http://dx.doi.org/
10.1145/1330017.1330022.

Mauliadi, R., Setyautami, M.R.A., Afriyanti, I., Azurat, A., 2017. A platform for charities system generation with SPL approach. In: Proc. Intl. Conf. on Information Technology Systems and Innovation. ICITSI, IEEE, New York, NY, USA, pp. 108-113. http://dx.doi.org/10.1109/ICITSI.2017.8267927.

Mikhajlov, L., Sekerinski, E., 1998. A study of the fragile base class problem. In: ECOOP'98. In: LNCS, vol. 1445, pp. 355-383, cited By 1.

Nierstrasz, O., Ducasse, S., Schärli, N., 2006. Flattening traits. J. Object Technol. 5 (4), 129-148. http://dx.doi.org/10.5381/jot.2006.5.4.a4.

Pohl, K., Böckle, G., van der Linden, F., 2005. Software Product Line Engineering - Foundations, Principles, and Techniques. Springer, Berlin, Germany.

Reppy, J.H., Turon, A., 2007. Metaprogramming with traits. In: Ernst, E. (Ed.), ECOOP 2007 - Object-Oriented Programming, 21st European Conference, Berlin, Germany, July 30 - August 3, 2007, Proceedings. In: Lecture Notes in Computer Science, vol. 4609, Springer, pp. 373-398. http://dx.doi.org/10.1007/978-3-540-73589-2_18.

Roffe, A.J., Calderon, J.S.T., 2021. Random formula generators. CoRR abs/2110.09228. URL: https://arxiv.org/abs/2110.09228. arXiv:2110.09228.

Roman, S., 2008. Lattices and Ordered Sets. Springer New York, URL: https://books.google.it/books?id=NZN8aum26LgC.

Schaefer, I., Bettini, L., Bono, V., Damiani, F., Tanzarella, N., 2010. Delta-oriented programming of software product lines. In: Software Product Lines: Going beyond (SPLC 2010). In: LNCS, vol. 6287, pp. 77-91. http://dx.doi.org/10.1007/978-3-642-15579-6_6.

Schaefer, I., Damiani, F., 2010. Pure delta-oriented programming. In: Proceedings of the 2nd International Workshop on Feature-Oriented Software Development. FOSD '10, ACM, pp. 49-56. http://dx.doi.org/10.1145/1868688.1868696.

Schaefer, I., Rabiser, R., Clarke, D., Bettini, L., Benavides, D., Botterweck, G., Pathak, A., Trujillo, S., Villela, K., 2012. Software diversity. Int. J. Softw. Tools Technol. Transf. 14 (5), 477-495. http://dx.doi.org/10.1007/s10009-012-0253-y.

Schärli, N., Ducasse, S., Nierstrasz, O., Black, A.P., 2003. Traits: Composable units of behaviour. In: Cardelli, L. (Ed.), ECOOP 2003 - Object-Oriented Programming, 17th European Conference, Darmstadt, Germany, July 21-25, 2003, Proceedings. In: LNCS, vol. 2743, Springer, pp. 248-274. http://dx.doi.org/10.1007/978-3-540-45070-2_12.

Schröter, R., Krieter, S., Thüm, T., Benduhn, F., Saake, G., 2016. Feature-model interfaces: The highway to compositional analyses of highly-configurable systems. In: Proceedings of the 38th International Conference on Software Engineering. ICSE '16, ACM, pp. 667-678. http://dx.doi.org/10.1145/2884781.2884823.

Schröter, R., Siegmund, N., Thüm, T., 2013a. Towards modular analysis of multi product lines. In: Proceedings of the 17th International Software Product Line Conference Co-Located Workshops. SPLC '13, ACM, pp. 96-99. http://dx.doi.org/10.1145/2499777.2500719.

Schröter, R., Thüm, T., Siegmund, N., Saake, G., 2013b. Automated analysis of dependent feature models. In: The Seventh International Workshop on Variability Modelling of Software-Intensive Systems, VaMoS '13, Pisa, Italy, January 23 - 25, 2013. pp. 9:1-9:5. http://dx.doi.org/10.1145/2430502.2430515.

Setyautami, M.R.A., Adianto, D., Azurat, A., 2018. Modeling multi software product lines using UML. In: Proc. 22nd Intl. Systems and Software Product Line Conference, Vol. 1. ACM, New York, NY, USA, pp. 274-278. http://dx.doi.org/10.1145/3233027.3236400.

Setyautami, M.R.A., Hähnle, R., 2021. An architectural pattern to realize multi software product lines in Java. In: Grünbacher, P., Seidl, C., Dhungana, D., Lovasz-Bukvova, H. (Eds.), Proc. 15th Intl. Working Conf. on Variability Modelling of Software-Intensive Systems, Krems, Austria. ACM Press, pp. 9:1-9:9. http://dx.doi.org/10.1145/3442391.3442401.

Setyautami, M.R.A., Rubiantoro, R.R., Azurat, A., 2019. Model-driven engineering for delta-oriented software product lines. In: 26th Asia-Pacific Software Engineering Conf., APSEC, Putrajaya, Malaysia. IEEE, pp. 371-377. http://dx.doi.org/10.1109/APSEC48747.2019.00057.

Smith, C., Drossopoulou, S., 2005. Chai: Traits for java-like languages. In: Black, A.P. (Ed.), ECOOP 2005 - Object-Oriented Programming. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 453-478. http://dx.doi.org/10.1007/115311420_20.

Strniša, R., Sewell, P., Parkinson, M., 2007. The Java module system: Core design and semantic definition. In: Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications. OOPSLA '07, Association for Computing Machinery, New York, NY, USA, pp. 499-514. http://dx.doi.org/10.1145/1297027.1297064.

Thaker, S., Batory, D., Kitchin, D., Cook, W., 2007. Safe composition of product lines. In: Proceedings of the 6th International Conference on Generative Programming and Component Engineering. GPCE '07, ACM, New York, NY, USA, pp. 95-104. http://dx.doi.org/10.1145/1289971.1289989.

Thüm, T., Apel, S., Kästner, C., Schaefer, I., Saake, G., 2014. A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47 (1), 6:1-6:45. http://dx.doi.org/10.1145/2580950.

Trujillo-Tzanahua, G.I., Juárez-Martínez, U., Aguilar-Lasserre, A.A., Cortés-Verdín, M.K., 2018. Multiple software product lines: applications and challenges. In: Mejia, J., Muñoz, M., Rocha, A., Quiñonez, Y., Calvo-Manzano, J. (Eds.), Trends and Applications in Software Engineering. Springer International Publishing, Cham, pp. 117-126. http://dx.doi.org/10.1007/978-3-319-69341-5_11.

Wirth, N., 1980. The module: A system structuring facility in high-level programming languages. In: Tobias, J.M. (Ed.), Language Design and Programming Methodology. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 1-24. http://dx.doi.org/10.1007/3-540-09745-7_1.

Wong, P.Y.H., Diakov, N., Schaefer, I., 2012. Modelling distributed adaptable object oriented systems using HATS approach: A fredhopper case study (invited paper). In: Beckert, B., Damiani, F., Gurov, D. (Eds.), 2nd Intl. Conf. on Formal Verification of Object-Oriented Software, Torino, Italy. In: LNCS, vol. 7421, Springer, pp. 49-66. http://dx.doi.org/10.1007/978-3-642-31762-0_5.