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

HAL
open science

Variability modules

Ferruccio Damiani, Reiner Hähnle, Eduard Kamburjan, Michael Lienhardt, Luca Paolini

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

To cite this version:

Ferruccio Damiani, Reiner Hähnle, Eduard Kamburjan, Michael Lienhardt, Luca Paolini. Variability modules. Journal of Systems and Software, 2022, 195, pp.111510. 10.1016/j.jss.2022.111510. hal-04620104

HAL Id: hal-04620104

https://hal.science/hal-04620104

Submitted on 21 Jun 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
Variability modules

Ferruccio Damiani, Reiner Hähnle, Eduard Kamburjan, Michael Lienhardt, Luca Paolini

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

To cite this version:

Ferruccio Damiani, Reiner Hähnle, Eduard Kamburjan, Michael Lienhardt, Luca Paolini. Variability modules. Journal of Systems and Software, 2022, 195, pp.111510. 10.1016/j.jss.2022.111510. hal-04620104

HAL Id: hal-04620104

https://hal.science/hal-04620104v1

Submitted on 21 Jun 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>
Variability modules ⭐

Ferruccio Damiani<sup>a,*</sup>, Reiner Hähnle<sup>b</sup>, Eduard Kamburjan<sup>c,*</sup>, Michael Lienhardt<sup>d</sup>,
Luca Paolini<sup>a</sup>

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

Check for
updates

ARTICLE INFO

Article history:

Received 21 February 2022

Received in revised form 18 July 2022

Accepted 8 September 2022

Available online 24 September 2022

Keywords:

Delta-oriented programming

Family-based analysis

Language design

Modules

Multi product line

Variant generation

A B S T R A C T

A Software Product Line (SPL) is a family of similar programs, called variants, generated from a common artifact base. A Multi SPL (MPL) is a set of interdependent SPLs: each variant can depend on variants from other SPLs. MPLs are challenging to model and to implement efficiently, especially when different variants of the same SPL must coexist and interoperate. We address this challenge by introducing the concept of a variability module (VM), a new language construct. A VM constitutes at the same time a module and an SPL of standard (variability-free), possibly interdependent, modules. Generating a variant of a VM triggers the generation of all variants required to satisfy its dependencies. Consequentially, a set of interdependent VMs represents an MPL that can be compiled into a set of standard modules. We illustrate the VM concept with an example from an industrial modeling scenario and formalize it in a core calculus. We define family-based analyses to check that a VM satisfies certain well-formedness conditions and whether all variants can be generated. Finally, we provide an implementation of VM for the Java-like modeling language ABS, and evaluate it with case studies.

© 2022 The Author(s). Published by Elsevier Inc. This is an open access article under the CC BY license

(http://creativecommons.org/licenses/by/4.0/).

# 1. Introduction

Modeling variability aspects of complex software systems poses challenges currently not adequately met by standard approaches to software product line engineering (SPLE) (Clements and Northrop, 2001; Pohl et al., 2005). A first modeling challenge is the situation when more than one product line is involved and these product lines depend on each other. Such sets of related and interdependent product lines are known as a multi product line (MPL) (Holl et al., 2012; Trujillo-Tzanahua et al., 2018). A second modeling challenge, orthogonal to MPLs, is the situation when different product variants from the same product line need to co-exist in the same context and must be interoperable (Damiani et al., 2018a).

In Section 2 we exemplify these two challenges in the context of an industrial case study from the literature (Kamburjan and Hähnle, 2016; Kamburjan et al., 2018), performed for Deutsche Bahn Netz AG, where: (i) several interdependent product lines for networks, signals, switches, etc., occur; and (ii) mechanic and

electric rail switches are different variants of the same product line, and some train stations include both. Overall, MPLs give rise to the quest for mechanisms for hiding implementation details, reducing dependencies, controlling access to elements, etc. (Holl et al., 2012).

We take the standard concept of a module (Wirth, 1980), used to structure large software systems since the 1970s, as a baseline. Software modules are supported in many programming and modeling languages, including ABS, Ada, Haskell, Java, Scala, to name just a few. Because modules are intended to facilitate interoperability and encapsulation, no further *ad hoc* concepts are needed for this purpose. We merely *add variability* to modules, rendering each module a product line of standard, variability-free modules. We call the resulting language concept *variability module* (VM).

The main advantage of VMs is their conceptual simplicity: as a straightforward extension of standard software modules, they are intuitive to use for anyone familiar with modules and with software product lines. Each VM is both a module and a product line of modules. This reduction of concepts not only drastically simplifies syntax, but reduces the cognitive burden on the modeler. To substantiate this claim, in Section 2 we illustrate the railways MPL case study in terms of VMs without the need to introduce any formal concepts. Nevertheless, there are a number of fundamental design decisions to take in the VM design concept. In Section 3 we

<footnote><sup>a</sup> Dipartimento di Informatica, University of Turin, Turin, Italy</footnote>

<footnote><sup>b</sup> Department of Computer Science, Technical University of Darmstadt, Darmstadt, Germany</footnote>

<footnote><sup>c</sup> Department of Informatics, University of Oslo, Oslo, Norway</footnote>

<footnote><sup>d</sup> ONERA, Palaiseau, France</footnote>

<footnote>☆ Editor: Raffaela Mirandola.</footnote>

<footnote>* Corresponding author.</footnote>

<footnote>E-mail addresses: ferruccio.damiani@unito.it (F. Damiani),</footnote>

<footnote>reiner.haehnle@tu-darmstadt.de (R. Hähnle), eduard@ifi.uio.no (E. Kamburjan),</footnote>

<footnote>michael.lienhardt@onera.fr (M. Lienhardt), luca.paolini@unito.it (L. Paolini).</footnote>
# Variability modules☆

Ferruccio Damiani<sup>a,*</sup>, Reiner Hähnle<sup>b</sup>, Eduard Kamburjan<sup>c,*</sup>, Michael Lienhardt<sup>d</sup>,
Luca Paolini<sup>a</sup>

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

Check for
updates

## ARTICLE INFO

**Article history:**

Received 21 February 2022

Received in revised form 18 July 2022

Accepted 8 September 2022

Available online 24 September 2022

**Keywords:**

Delta-oriented programming

Family-based analysis

Language design

Modules

Multi product line

Variant generation

## ABSTRACT

A Software Product Line (SPL) is a family of similar programs, called variants, generated from a common artifact base. A Multi SPL (MPL) is a set of interdependent SPLs: each variant can depend on variants from other SPLs. MPLs are challenging to model and to implement efficiently, especially when different variants of the same SPL must coexist and interoperate. We address this challenge by introducing the concept of a variability module (VM), a new language construct. A VM constitutes at the same time a module and an SPL of standard (variability-free), possibly interdependent, modules. Generating a variant of a VM triggers the generation of all variants required to satisfy its dependencies. Consequentially, a set of interdependent VMs represents an MPL that can be compiled into a set of standard modules. We illustrate the VM concept with an example from an industrial modeling scenario and formalize it in a core calculus. We define family-based analyses to check that a VM satisfies certain well-formedness conditions and whether all variants can be generated. Finally, we provide an implementation of VM for the Java-like modeling language ABS, and evaluate it with case studies.

© 2022 The Author(s). Published by Elsevier Inc. This is an open access article under the CC BY license

(http://creativecommons.org/licenses/by/4.0/).

## 1. Introduction

Modeling variability aspects of complex software systems poses challenges currently not adequately met by standard approaches to software product line engineering (SPLE) (Clements and Northrop, 2001; Pohl et al., 2005). A first modeling challenge is the situation when more than one product line is involved and these product lines depend on each other. Such sets of related and interdependent product lines are known as a multi product line (MPL) (Holl et al., 2012; Trujillo-Tzanahua et al., 2018). A second modeling challenge, orthogonal to MPLs, is the situation when different product variants from the same product line need to co-exist in the same context and must be interoperable (Damiani et al., 2018a).

In Section 2 we exemplify these two challenges in the context of an industrial case study from the literature (Kamburjan and Hähnle, 2016; Kamburjan et al., 2018), performed for Deutsche Bahn Netz AG, where: (i) several interdependent product lines for networks, signals, switches, etc., occur; and (ii) mechanic and

electric rail switches are different variants of the same product line, and some train stations include both. Overall, MPLs give rise to the quest for mechanisms for hiding implementation details, reducing dependencies, controlling access to elements, etc. (Holl et al., 2012).

We take the standard concept of a module (Wirth, 1980), used to structure large software systems since the 1970s, as a baseline. Software modules are supported in many programming and modeling languages, including ABS, Ada, Haskell, Java, Scala, to name just a few. Because modules are intended to facilitate interoperability and encapsulation, no further *ad hoc* concepts are needed for this purpose. We merely *add variability* to modules, rendering each module a product line of standard, variability-free modules. We call the resulting language concept *variability module* (VM).

The main advantage of VMs is their conceptual simplicity: as a straightforward extension of standard software modules, they are intuitive to use for anyone familiar with modules and with software product lines. Each VM is both a module and a product line of modules. This reduction of concepts not only drastically simplifies syntax, but reduces the cognitive burden on the modeler. To substantiate this claim, in Section 2 we illustrate the railways MPL case study in terms of VMs without the need to introduce any formal concepts. Nevertheless, there are a number of fundamental design decisions to take in the VM design concept. In Section 3 we

<footnote><sup>a</sup> Dipartimento di Informatica, University of Turin, Turin, Italy</footnote>

<footnote><sup>b</sup> Department of Computer Science, Technical University of Darmstadt, Darmstadt, Germany</footnote>

<footnote><sup>c</sup> Department of Informatics, University of Oslo, Oslo, Norway</footnote>

<footnote><sup>d</sup> ONERA, Palaiseau, France</footnote>

<footnote>☆ Editor: Raffaela Mirandola.</footnote>

<footnote>* Corresponding author.</footnote>

<footnote>E-mail addresses: ferruccio.damiani@unito.it (F. Damiani), reiner.haehnle@tu-darmstadt.de (R. Hähnle), eduard@ifi.uio.no (E. Kamburjan), michael.lienhardt@onera.fr (M. Lienhardt), luca.paolini@unito.it (L. Paolini).</footnote>
provide background on code reuse in SPL implementation, then, in Section 4, we motivate and discuss the VM design decisions.

We formulate the VM concept as an extension of the standard concept of module for Java-like (i.e., object-oriented, class-based and strongly typed) languages. To support variability, VMs employ *delta-oriented programming* (DOP) – see Schaefer et al. (2010) and (Apel et al., 2013, Sect. 6.6.1). Specifically, we contribute (i) a theoretical foundation of VMs, including formal syntax and semantics, in terms of a core calculus; and (ii) an implementation of VMs as an extension of the ABS language (Hähnle, 2013; Johnsen et al., 2010).

We choose ABS because it features native implementations of DOP and it was successfully used in industrial case studies for variability modeling (Kamburjan et al., 2018; Mauliadi et al., 2017; Wong et al., 2012). We stress that VMs can be added on top of *any* Java-like language. For instance, a proof-of-concept realization of VM for the Java programming language, based on architectural patterns, is (informally) described by Setyautami and Hähnle (2021). That paper demonstrates the usefulness of the VM concept, but lacks several VM features introduced here, as well as a formal foundation.

The formal underpinnings of VMs are covered in Sections 5–9. In Section 5 we declare their syntax and spell out consistency requirements of ABS-VM, a core calculus for ABS with VMs. Section 6 formalizes a statically checkable property of VMs: the *principle of encapsulated variability (PEV)*, which ensures that any dependency among VMs can be reduced to dependencies among standard, variability-free modules. In Section 7 we define variant generation in terms of a “flattening” semantics: the variants requested from an SPL represented by a VM, together with necessary variants of other VMs it depends upon, are generated by translating each VM into a set of variability-free, standard modules (one per variant). This results in a variability-free program with suitably disambiguated identifiers and is sufficient to define the semantics of VMs precisely, to compile and to run them. In Section 8 we define type-safety for ABS-VM programs: the guarantee that all variants of all VMs of a program can be generated and together form a well-typed variability-free ABS program. In Section 9 we define family-based analyses that partially check whether an ABS-VM program is type-safe, including the property that all variants of all VMs can be generated.

Section 10 describes how the VM concept is integrated into the existing ABS tool chain. As long as one has control over the parser and abstract syntax tree, it is relatively straightforward to realize the family-based checks (of Section 9) and the flattening algorithm (of Section 7) within any compiler tool chain. Section 11 evaluates VMs by means of case studies. Related work is discussed in Section 12. We conclude in Section 13 by outlining ongoing work.

The present article is based on an SPLC 2021 paper (Damiani et al., 2021), with the following extensions:

1. We *define* type-uniformity, pre-typing, and applicability consistency analyses for ABS-VM programs.

2. We *implement* sanity condition checks, a PEV compliance check, maximal unique annotation inference, as well as the analyses listed in item 1

3. The VM language features so-called *open* product definitions (Section 5.1), however, these were neither *implemented* nor *used* in a case study, which is now done.

4. We *extend* the evaluation.

## 2. Introducing variability modules

We illustrate variability modules and how they support variant interoperability by way of an example based on the industrial

<figure><img src="image_5.png" /><figcaption>**Fig. 1.** Features of signals and switches.</figcaption></figure>

FormbaR case study from railway engineering (Kamburjan et al., 2018).<fnref n="1" /> We look at the full FormbaR case study during VM evaluation in Section 11.

Our scenario contains signals, switches, interlocking systems, that use multiple variants of signals and switches, and a railway station that uses multiple variants of interlocking systems. Fig. 1 shows the feature models for switches and signals. Feature models (Czarnecki and Eisenecker, 2000) specify software variants in terms of features. A feature is a name representing some functionality, a set of features is called a configuration, and each variant is identified by a valid configuration (called a product, for short). Equivalent representations of feature models have been proposed in the literature, e.g., by Batory (2005) and Apel et al. (2013), like feature diagrams (Fig. 1) and propositional formulas (lines beginning with the keywords *features* in Figs. 2–3).

A signal is either a light signal, using bulbs and colors to indicate the signal aspect or a form signal that uses mechanically moved shapes. All variants of a signal share the same interface to the interlocking system and basic functionality, such as aspect change (for example, signals have always the aspects “Halt” and “Go”). In case of multiple outgoing tracks, a signal may also indicate the direction a train is taking — so there are four signal variants. Variability occurs, for example, in a class *Bulb*, only present in the light signals variant and in the fact that method `setToHalt` (which changes the shown aspect to “Halt”) is implemented differently for form and light signals (the latter communicate with their *Bulb* instances).

Signals are modeled by the VM *signals* in Fig. 2. It starts with the *module header*, comprising: the keyword *module*, the module *name*, the list of *exported module elements*, the *feature list* constrained with a propositional formula describing the products. This is followed by a list of *configuration* definitions (here just one), where each definition gives a name to a set of features. Finally, a list of *product* definitions (here just one), where each definition gives a *name* to a product of the SPL.

Next is the module *core part*, comprising declarations of interface *ISig* and of class *CSig* that implements *ISig*. By default, classes and interfaces can be modified/removed by deltas to obtain different product variants, however, class/interface declarations annotated by the keyword *unique* must be *the same* in all product variants. Unique declarations enable interoperability between different product variants of the same VM.

Finally there is the *delta part*, comprising the deltas that describe the implementation of different variants and their application conditions. Classes and interfaces added by deltas can be modified or removed again by other deltas. The delta *LDelta*, triggered by feature Light, adds a class *Bulb* and modifies the class *CSig* to reference the class *Bulb*. Deltas *FDelta* and *DDelta* implement features Form and Dir, respectively.

<footnote n="1">¹ For presentation purposes some aspects are modeled in a slightly different manner as in Kamburjan et al. (2018).</footnote>
provide background on code reuse in SPL implementation, then, in Section 4, we motivate and discuss the VM design decisions.

We formulate the VM concept as an extension of the standard concept of module for Java-like (i.e., object-oriented, class-based and strongly typed) languages. To support variability, VMs employ delta-oriented programming (DOP) – see Schaefer et al. (2010) and (Apel et al., 2013, Sect. 6.6.1). Specifically, we contribute (i) a theoretical foundation of VMs, including formal syntax and semantics, in terms of a core calculus; and (ii) an implementation of VMs as an extension of the ABS language (Hähnle, 2013; Johnsen et al., 2010).

We choose ABS because it features native implementations of DOP and it was successfully used in industrial case studies for variability modeling (Kamburjan et al., 2018; Mauliadi et al., 2017; Wong et al., 2012). We stress that VMs can be added on top of any Java-like language. For instance, a proof-of-concept realization of VM for the Java programming language, based on architectural patterns, is (informally) described by Setyautami and Hähnle (2021). That paper demonstrates the usefulness of the VM concept, but lacks several VM features introduced here, as well as a formal foundation.

The formal underpinnings of VMs are covered in Sections 5–9. In Section 5 we declare their syntax and spell out consistency requirements of ABS-VM, a core calculus for ABS with VMs. Section 6 formalizes a statically checkable property of VMs: the *principle of encapsulated variability (PEV)*, which ensures that any dependency among VMs can be reduced to dependencies among standard, variability-free modules. In Section 7 we define variant generation in terms of a “flattening” semantics: the variants requested from an SPL represented by a VM, together with necessary variants of other VMs it depends upon, are generated by translating each VM into a set of variability-free, standard modules (one per variant). This results in a variability-free program with suitably disambiguated identifiers and is sufficient to define the semantics of VMs precisely, to compile and to run them. In Section 8 we define type-safety for ABS-VM programs: the guarantee that all variants of all VMs of a program can be generated and together form a well-typed variability-free ABS program. In Section 9 we define family-based analyses that partially check whether an ABS-VM program is type-safe, including the property that all variants of all VMs can be generated.

Section 10 describes how the VM concept is integrated into the existing ABS tool chain. As long as one has control over the parser and abstract syntax tree, it is relatively straightforward to realize the family-based checks (of Section 9) and the flattening algorithm (of Section 7) within any compiler tool chain. Section 11 evaluates VMs by means of case studies. Related work is discussed in Section 12. We conclude in Section 13 by outlining ongoing work.

The present article is based on an SPLC 2021 paper (Damiani et al., 2021), with the following extensions:

1. We *define* type-uniformity, pre-typing, and applicability consistency analyses for ABS-VM programs.

2. We *implement* sanity condition checks, a PEV compliance check, maximal unique annotation inference, as well as the analyses listed in item 1

3. The VM language features so-called *open* product definitions (Section 5.1), however, these were neither *implemented* nor *used* in a case study, which is now done.

4. We *extend* the evaluation.

## 2. Introducing variability modules

We illustrate variability modules and how they support variant interoperability by way of an example based on the industrial

<figure><img src="image_4.png" /><figcaption>**Fig. 1.** Features of signals and switches.</figcaption></figure>

FormbaR case study from railway engineering (Kamburjan et al., 2018).<fnref n="1" /> We look at the full FormbaR case study during VM evaluation in Section 11.

Our scenario contains signals, switches, interlocking systems, that use multiple variants of signals and switches, and a railway station that uses multiple variants of interlocking systems. Fig. 1 shows the feature models for switches and signals. Feature models (Czarnecki and Eisenecker, 2000) specify software variants in terms of features. A feature is a name representing some functionality, a set of features is called a configuration, and each variant is identified by a valid configuration (called a product, for short). Equivalent representations of feature models have been proposed in the literature, e.g., by Batory (2005) and Apel et al. (2013), like feature diagrams (Fig. 1) and propositional formulas (lines beginning with the keywords *features* in Figs. 2–3).

A signal is either a light signal, using bulbs and colors to indicate the signal aspect or a form signal that uses mechanically moved shapes. All variants of a signal share the same interface to the interlocking system and basic functionality, such as aspect change (for example, signals have always the aspects “Halt” and “Go”). In case of multiple outgoing tracks, a signal may also indicate the direction a train is taking — so there are four signal variants. Variability occurs, for example, in a class *Bulb*, only present in the light signals variant and in the fact that method `setToHalt` (which changes the shown aspect to “Halt”) is implemented differently for form and light signals (the latter communicate with their *Bulb* instances).

Signals are modeled by the VM *signals* in Fig. 2. It starts with the *module header*, comprising: the keyword *module*, the module *name*, the list of *exported module elements*, the *feature list* constrained with a propositional formula describing the products. This is followed by a list of *configuration definitions* (here just one), where each definition gives a name to a set of features. Finally, a list of *product definitions* (here just one), where each definition gives a *name* to a product of the SPL.

Next is the module *core part*, comprising declarations of interface *ISig* and of class *CSig* that implements *ISig*. By default, classes and interfaces can be modified/removed by deltas to obtain different product variants, however, class/interface declarations annotated by the keyword *unique* must be *the same* in all product variants. Unique declarations enable interoperability between different product variants of the same VM.

Finally there is the *delta part*, comprising the deltas that describe the implementation of different variants and their application conditions. Classes and interfaces added by deltas can be modified or removed again by other deltas. The delta *LDelta*, triggered by feature Light, adds a class *Bulb* and modifies the class *CSig* to reference the class *Bulb*. Deltas *FDelta* and *DDelta* implement features Form and Dir, respectively.

<footnote n="1">¹ For presentation purposes some aspects are modeled in a slightly different manner as in Kamburjan et al. (2018).</footnote>
<figure><img src="image_6.png" /><figcaption>Fig. 2. An SPL of signals as a VM.</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>Fig. 3. An SPL of tracks and switches as a VM.</figcaption></figure>

Switches and tracks are modeled by the VM in Fig. 3. It is structurally similar to Signals. A switch is either electric (controlled from the interlocking system) or mechanic (controlled locally by a lever). Class CTrack contains a reference to class CSwitch, which is not declared unique. So, even though class CTrack is not modified/removed by any delta, its declaration cannot be annotated with unique.

Interlocking systems are modeled by the VM in Fig. 4. An interlocking system manages switches and signals that lie on tracks, it imports all the exported elements (feature names are implicitly exported/imported) of the VMs Signals and Switches. The VM InterlockingSys has four variants, modeled by two optional features. Line 7 contains a product definition that gives name PSwitch to a product of the VM Switch. It is called an open product definition, because it depends on the selected product of the VM InterlockingSys itself: if feature Modern is selected PSwitch specifies an electric switch, otherwise it specifies a mechanic switch (product clauses are evaluated in order until a valid one

is found). Line 9 contains an open product definition for the VM Signal. It is worth observing that open product definitions enable implementing different variants of the VM InterlockingSys even without using deltas. Method testSig of class CILS instantiates classes from two different product variants of Switches and from two different product variants of Signals. All references to non-unique imported classes/interfaces specify a product, by using a with clause. In a with clause, the product can be specified by explicitly listing its features, by using one of the defined product names, or (more generally) by a set-theoretic expression. For example, track is taken from product (Mechanic) of module Switches, while sigNormal uses the product name LSig imported from Signals. In line 19 a switch is added to a track element: since track contains a reference to an instance of the mechanic variant of class CTrack, appendSwitch() will add a mechanic switch. All signal variants of the VM Signals share the same definition of the unique ISig interface, thus making it accessible to anyone that imports it from Signals. On the other hand, the CBulb class
<figure><img src="image_5.png" /><figcaption>Fig. 2. An SPL of signals as a VM.</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Fig. 3. An SPL of tracks and switches as a VM.</figcaption></figure>

Switches and tracks are modeled by the VM in Fig. 3. It is structurally similar to Signals. A switch is either electric (controlled from the interlocking system) or mechanic (controlled locally by a lever). Class CTrack contains a reference to class CSwitch, which is not declared unique. So, even though class CTrack is not modified/removed by any delta, its declaration cannot be annotated with unique.

Interlocking systems are modeled by the VM in Fig. 4. An interlocking system manages switches and signals that lie on tracks, it imports all the exported elements (feature names are implicitly exported/imported) of the VMs Signals and Switches. The VM InterlockingSys has four variants, modeled by two optional features. Line 7 contains a product definition that gives name PSwitch to a product of the VM Switch. It is called an open product definition, because it depends on the selected product of the VM InterlockingSys itself: if feature Modern is selected PSwitch specifies an electric switch, otherwise it specifies a mechanic switch (product clauses are evaluated in order until a valid one

is found). Line 9 contains an open product definition for the VM Signal. It is worth observing that open product definitions enable implementing different variants of the VM InterlockingSys even without using deltas. Method testSig of class CILS instantiates classes from two different product variants of Switches and from two different product variants of Signals. All references to non-unique imported classes/interfaces specify a product, by using a with clause. In a with clause, the product can be specified by explicitly listing its features, by using one of the defined product names, or (more generally) by a set-theoretic expression. For example, track is taken from product (Mechanic) of module Switches, while sigNormal uses the product name LSig imported from Signals. In line 19 a switch is added to a track element: since track contains a reference to an instance of the mechanic variant of class CTrack, appendSwitch() will add a mechanic switch. All signal variants of the VM Signals share the same definition of the unique ISig interface, thus making it accessible to anyone that imports it from Signals. On the other hand, the CBulb class
<figure><img src="image_8.png" /><figcaption>Fig. 4. An SPL of interlocking systems as a VM.</figcaption></figure>

<figure><img src="image_9.png" /><figcaption>Fig. 5. A railway station as a main module.</figcaption></figure>

is only used inside the VM *Signals*. Different product variants are fully interoperable, as witnessed by the expression in line 22.

We conclude this brief overview of VMs by defining the terminology of unique and main module.

* A *unique module* (UM) is a VM that does not contain a feature model. Therefore, it contains no configuration definitions, no open product definitions, and no deltas, however, it may contain *with* clauses and closed product definitions. All classes and interfaces of a UM are implicitly considered unique, so the *unique* keyword can be omitted.

* A *main module* is a UM containing an implicit class providing an initialization method declared by the keyword *init*. Each program has at most one main module. Programs without a main module cannot be executed (like Java programs without a class containing a main method).

The whole railway station is modeled by the main module `RailwayStation` (Fig. 5) as well as VMs `Signals` (Fig. 2), `Switches` (Fig. 3), and `InterlockingSys` (Fig. 4). They represent an MPL called the *railway station* henceforth.

### 3. Code reuse in SPL implementation

The example in Section 2 illustrates how DOP supports SPL implementation, and how VMs support both interoperable variants and MPLs. Before we continue with the formalization of VMs, let us briefly recall the bigger picture in software product line engineering as far as code reuse in feature-oriented SPL implementation is concerned.

In software product line engineering one aims to develop a family of similar programs, called variants, by managed reuse

(Clements and Northrop, 2001; Pohl et al., 2005). In feature-oriented SPLs (Apel et al., 2013) this amounts to: (i) From the *problem space* perspective, each variant of an SPL is identified by a set of features, called a *product*; (ii) from the *solution space* perspective, code reuse mechanisms for variant implementations have to be flexible enough to capture commonalities in the variants and to realize the desired variants (Schaefer et al., 2012).

Consider, for instance, the SPL for signals in Section 2: (i) Concerning the problem space, it has *n* features and *m* products; (ii) concerning the solution space, it has programs written in a Java-like language as variants, where each variant represents a signal by means of an interface `ISig`, which is the same for all variants, and a class, which is different in each variant. A straightforward, but naive, approach to SPL implementation provides the code of all *m* variants within the same program. Then the SPL for signals is implemented as a program comprising the interface `ISig` and *m* classes `CSig1`, ..., `CSigm` (one for each product). This approach, however, has several issues:

1. The code reuse mechanism of a Java-like implementation language might not be flexible enough to capture commonalities in the variants, so some code might be duplicated. In particular, the rigidity of class-based inheritance (code reuse can be realized only within a class hierarchy Mikhajlov and Sekerinski, 1998; Ducasse et al., 2006) puts limitations on the reuse of code across variants.

2. Java-like languages possess no construct to explicitly capture the relation between the problem and the solution spaces. To document the relation between features and variants, and to support automatic variant generation, *ad hoc* external tool support must be added.

3. The approach does not scale: recall that an SPL with *n* features can have up to *m* = $2^n$ products, thus up to $2^n$ classes `CSig` must be defined.

Using a Java-like language featuring flexible code reuse mechanisms (for example, traits (Schärli et al., 2003; Ducasse et al., 2006)<fnref n="2" /> or the constructs of the JIGSAW framework (Bracha,

<footnote n="2">² Traits were first proposed in the dynamically typed, object-oriented, class-based Smalltalk/Squeak language (Schärli et al., 2003; Ducasse et al., 2006) and</footnote>
<figure><img src="image_7.png" /><figcaption>Fig. 4. An SPL of interlocking systems as a VM.</figcaption></figure>

<figure><img src="image_8.png" /><figcaption>Fig. 5. A railway station as a main module.</figcaption></figure>

is only used inside the VM Signals. Different product variants are fully interoperable, as witnessed by the expression in line 22.

We conclude this brief overview of VMs by defining the terminology of unique and main module.

* A *unique module* (UM) is a VM that does not contain a feature model. Therefore, it contains no configuration definitions, no open product definitions, and no deltas, however, it may contain *with* clauses and closed product definitions. All classes and interfaces of a UM are implicitly considered unique, so the *unique* keyword can be omitted.

* A *main module* is a UM containing an implicit class providing an initialization method declared by the keyword *init*. Each program has at most one main module. Programs without a main module cannot be executed (like Java programs without a class containing a main method).

The whole railway station is modeled by the main module `RailwayStation` (Fig. 5) as well as VMs `Signals` (Fig. 2), `Switches` (Fig. 3), and `InterlockingSys` (Fig. 4). They represent an MPL called the *railway station* henceforth.

## 3. Code reuse in SPL implementation

The example in Section 2 illustrates how DOP supports SPL implementation, and how VMs support both interoperable variants and MPLs. Before we continue with the formalization of VMs, let us briefly recall the bigger picture in software product line engineering as far as code reuse in feature-oriented SPL implementation is concerned.

In software product line engineering one aims to develop a family of similar programs, called variants, by managed reuse

(Clements and Northrop, 2001; Pohl et al., 2005). In feature-oriented SPLs (Apel et al., 2013) this amounts to: (i) From the *problem space* perspective, each variant of an SPL is identified by a set of features, called a *product*; (ii) from the *solution space* perspective, code reuse mechanisms for variant implementations have to be flexible enough to capture commonalities in the variants and to realize the desired variants (Schaefer et al., 2012).

Consider, for instance, the SPL for signals in Section 2: (i) Concerning the problem space, it has *n* features and *m* products; (ii) concerning the solution space, it has programs written in a Java-like language as variants, where each variant represents a signal by means of an interface `ISig`, which is the same for all variants, and a class, which is different in each variant. A straightforward, but naive, approach to SPL implementation provides the code of all *m* variants within the same program. Then the SPL for signals is implemented as a program comprising the interface `ISig` and *m* classes `CSig1`, ..., `CSigm` (one for each product). This approach, however, has several issues:

1. The code reuse mechanism of a Java-like implementation language might not be flexible enough to capture commonalities in the variants, so some code might be duplicated. In particular, the rigidity of class-based inheritance (code reuse can be realized only within a class hierarchy Mikhajlov and Sekerinski, 1998; Ducasse et al., 2006) puts limitations on the reuse of code across variants.

2. Java-like languages possess no construct to explicitly capture the relation between the problem and the solution spaces. To document the relation between features and variants, and to support automatic variant generation, *ad hoc* external tool support must be added.

3. The approach does not scale: recall that an SPL with *n* features can have up to *m* = $2^n$ products, thus up to $2^n$ classes `CSig` must be defined.

Using a Java-like language featuring flexible code reuse mechanisms (for example, traits (Schärli et al., 2003; Ducasse et al., 2006)<fnref n="2" /> or the constructs of the JIGSAW framework (Bracha,

<footnote n="2">² Traits were first proposed in the dynamically typed, object-oriented, class-based Smalltalk/Squeak language (Schärli et al., 2003; Ducasse et al., 2006) and</footnote>
1992)$^3$) addresses the first issue, but not the remaining ones. To address the second and third issue, programming constructs specifically designed for *inter-product* (i.e., across different variants) code reuse have been developed.

Following Schaefer et al. (2012), we classify programming constructs dedicated to inter-product code reuse into three approaches. First, the *annotative approach* expresses negative variability: code is marked with those features of an SPL it implements and a variant is obtained by excluding code associated with *non-selected* features. An example of the annotative approach is CIDE (Kästner et al., 2012a). Second, the *compositional approach* expresses positive variability: variants are built by composing code fragments that implement specific features. A prominent instance is *feature-oriented programming* (FOP), for example Batory et al. (2004) or (Apel et al., 2013, Sect. 6.1). FOP can be viewed as a restriction of DOP with the following constraints: there is a one-to-one mapping between deltas and features (each delta is activated if and only if the corresponding feature is selected), the delta application order is total, and there are no class/interface/-field/method removal operations (Schaefer and Damiani, 2010). Third, the *transformational approach* expresses both positive and negative variability. DOP is an instance of the transformational approach.

In the context of annotative/compositional/transformational approaches to inter-product code reuse, the code reuse mechanism provided by the language in which each variant is written has the role of an *intra-product* code reuse mechanism (that is, it expresses code reuse *within* the same variant) (Damiani et al., 2014a).

**Remark 1 (Inter- and Intra-Product Code Reuse in ABS).** The original version of the ABS language (Hähnle, 2013; Johnsen et al., 2010) has deltas as a construct for inter-product code reuse and *no construct* for intra-product code reuse: we refer to this version of ABS as *Delta-ABS*. Hence, in some Delta-ABS case studies code duplication within the same variant was present. A notable case of a Delta-ABS model with duplicated code is the first version of the FormbaR case study (Kamburjan and Hähnle, 2016), where each infrastructure element (for example, a signal) is modeled by a class and (since different variants of the same infrastructure element need to coexist) a separate class is declared for each variant of an infrastructure element. Certain code is duplicated across all variants, for example, the code for a method that models the end of a train passing through an infrastructure element is duplicated in three out of five classes present.

A more recent ABS version (Damiani et al., 2017a) added traits for intra-product code reuse to Delta-ABS: we refer to that ABS version with *Delta-Trait-ABS*. The second version of the FormbaR case study (Kamburjan et al., 2018), implemented in Delta-Trait-ABS, saves duplicated code by using traits, resulting in 40% fewer lines of code on the named infrastructure alone. The second and third issue noted above, however, are not addressed with traits.

To the best of our knowledge, no programming construct for implementing interoperable variants overcomes the second and third issue discussed above. VMs address all three issues and provide proper support for MPLs as well as variant interoperability. In Section 11 we present a refactored version of the FormbaR case study based on VMs.

## 4. Design decisions

We briefly illustrate the rationale behind the major VM design decisions.

**Unique Annotation.** As illustrated in Section 2, *unique* class/interface declarations in a VM $M$ are shared by all variants of $M$. Without the *unique* keyword, unique class/interface declarations need to be inferred (via *Definition 4*), creating the danger of unintended changes of the set of classes/interface faces in a program considered to be unique. Obviously, a tool that points out all class/interface declarations that *could* be annotated *unique* is useful.

**Principle of Encapsulated Variability (PEV).** The PEV prescribes that each VM can depend on other VMs only by using classes or interfaces that are either *unique* or that belong to a *specific* variant. If a VM program adheres to the PEV, then flattening (defined in Section 7) – which removes variability and generates those variants required by the dependencies – can resolve all dependencies among VMs to dependencies among UMs. The main reasons for adopting the PEV are *simplicity* and *usability*: it suffices to work with a standard module concept (no need for composition or disambiguation operators as, for example, Kästner et al. (2012b)) and it is easy for the modeler to find out to which implementation any object reference in a VM refers to.

**Disjoint Feature Models.** Each VM has its own feature model, disjoint from those of other VMs: each feature name belongs to the VM where it is declared (like class interface names). There are no export/import clauses for features: each VM can refer to a feature $f$ of another VM $M$ only within a scope where the name $M$ is specified: each occurrence of a feature name $f$ is understood as $M.f$ for a VM name $M$ that is clear from the context. Feature names can be defined, with a different meaning, in different VMs. Feature names are implicitly exported/imported. It might be useful to add support for expressing constraints connecting the different feature models (e.g., to specify that certain variants must not co-exist in the same application).

**Implicit Export/Import Flattening.** Each VM $M$ must declare any export/ import that may occur in one of its variants. The flattening generates more specific export/import clauses for each variant by dropping the export clauses for classes/interfaces not present in that variant, and by creating import clauses for the required variants of the VMs mentioned in the import clauses of $M$. This design choice avoids the need to define delta operations on export/import clauses in the language that then would be supplied by the modeler.<fnref n="4" /> Altogether, it reduces the cognitive burden to understand VM code and the effort to write it.

**Family-based Checking.** VMs are designed to facilitate family-based analyses (Thüm et al., 2014). The implementation of VMs as part of the ABS compiler tool chain (Section 10) supports family-based analysis to check – before flattening

<footnote>subsequently formulated in a Java-like setting by various authors (Smith and Drossopoulou, 2005; Nierstrasz et al., 2006; Reppy and Turon, 2007; Bono et al., 2008; Liquori and Spiwack, 2008; Bettini et al., 2013b; Bettini and Damiani, 2017).</footnote>

<footnote n="3">³ The constructs of the JIGSAW framework (Bracha, 1992) were formalized in a Java-like setting by means of the FGig calculus (Lagorio et al., 2009, 2012).</footnote>

<footnote n="4">⁴ To extend VMs with delta operations on export clauses is straightforward. It would sometimes allow to shorten export clauses. On the other hand, since implicit flattening drops all unused imports, deltas on import clauses provide no advantage.</footnote>
1992)$^3$) addresses the first issue, but not the remaining ones. To address the second and third issue, programming constructs specifically designed for *inter-product* (i.e., across different variants) code reuse have been developed.

Following Schaefer et al. (2012), we classify programming constructs dedicated to inter-product code reuse into three approaches. First, the *annotative approach* expresses negative variability: code is marked with those features of an SPL it implements and a variant is obtained by excluding code associated with *non-selected* features. An example of the annotative approach is CIDE (Kästner et al., 2012a). Second, the *compositional approach* expresses positive variability: variants are built by composing code fragments that implement specific features. A prominent instance is *feature-oriented programming* (FOP), for example Batory et al. (2004) or (Apel et al., 2013, Sect. 6.1). FOP can be viewed as a restriction of DOP with the following constraints: there is a one-to-one mapping between deltas and features (each delta is activated if and only if the corresponding feature is selected), the delta application order is total, and there are no class/interface/-field/method removal operations (Schaefer and Damiani, 2010). Third, the *transformational approach* expresses both positive and negative variability. DOP is an instance of the transformational approach.

In the context of annotative/compositional/transformational approaches to inter-product code reuse, the code reuse mechanism provided by the language in which each variant is written has the role of an *intra-product* code reuse mechanism (that is, it expresses code reuse *within* the same variant) (Damiani et al., 2014a).

**Remark 1 (Inter- and Intra-Product Code Reuse in ABS).** The original version of the ABS language (Hähnle, 2013; Johnsen et al., 2010) has deltas as a construct for inter-product code reuse and *no construct* for intra-product code reuse: we refer to this version of ABS as *Delta-ABS*. Hence, in some Delta-ABS case studies code duplication within the same variant was present. A notable case of a Delta-ABS model with duplicated code is the first version of the FormbaR case study (Kamburjan and Hähnle, 2016), where each infrastructure element (for example, a signal) is modeled by a class and (since different variants of the same infrastructure element need to coexist) a separate class is declared for each variant of an infrastructure element. Certain code is duplicated across all variants, for example, the code for a method that models the end of a train passing through an infrastructure element is duplicated in three out of five classes present.

A more recent ABS version (Damiani et al., 2017a) added traits for intra-product code reuse to Delta-ABS: we refer to that ABS version with *Delta-Trait-ABS*. The second version of the FormbaR case study (Kamburjan et al., 2018), implemented in Delta-Trait-ABS, saves duplicated code by using traits, resulting in 40% fewer lines of code on the named infrastructure alone. The second and third issue noted above, however, are not addressed with traits.

To the best of our knowledge, no programming construct for implementing interoperable variants overcomes the second and third issue discussed above. VMs address all three issues and provide proper support for MPLs as well as variant interoperability. In Section 11 we present a refactored version of the FormbaR case study based on VMs.

# 4. Design decisions

We briefly illustrate the rationale behind the major VM design decisions.

**Unique Annotation.** As illustrated in Section 2, *unique* class/interface declarations in a VM $M$ are shared by all variants of $M$. Without the *unique* keyword, unique class/interface declarations need to be inferred (via *Definition 4*), creating the danger of unintended changes of the set of classes/interface faces in a program considered to be unique. Obviously, a tool that points out all class/interface declarations that *could* be annotated *unique* is useful.

**Principle of Encapsulated Variability (PEV).** The PEV prescribes that each VM can depend on other VMs only by using classes or interfaces that are either *unique* or that belong to a *specific* variant. If a VM program adheres to the PEV, then flattening (defined in Section 7) – which removes variability and generates those variants required by the dependencies – can resolve all dependencies among VMs to dependencies among UMs. The main reasons for adopting the PEV are *simplicity* and *usability*: it suffices to work with a standard module concept (no need for composition or disambiguation operators as, for example, Kästner et al. (2012b)) and it is easy for the modeler to find out to which implementation any object reference in a VM refers to.

**Disjoint Feature Models.** Each VM has its own feature model, disjoint from those of other VMs: each feature name belongs to the VM where it is declared (like class interface names). There are no export/import clauses for features: each VM can refer to a feature $f$ of another VM $M$ only within a scope where the name $M$ is specified: each occurrence of a feature name $f$ is understood as $M.f$ for a VM name $M$ that is clear from the context. Feature names can be defined, with a different meaning, in different VMs. Feature names are implicitly exported/imported. It might be useful to add support for expressing constraints connecting the different feature models (e.g., to specify that certain variants must not co-exist in the same application).

**Implicit Export/Import Flattening.** Each VM $M$ must declare any export/ import that may occur in one of its variants. The flattening generates more specific export/import clauses for each variant by dropping the export clauses for classes/interfaces not present in that variant, and by creating import clauses for the required variants of the VMs mentioned in the import clauses of $M$. This design choice avoids the need to define delta operations on export/import clauses in the language that then would be supplied by the modeler.<fnref n="4" /> Altogether, it reduces the cognitive burden to understand VM code and the effort to write it.

**Family-based Checking.** VMs are designed to facilitate family-based analyses (Thüm et al., 2014). The implementation of VMs as part of the ABS compiler tool chain (Section 10) supports family-based analysis to check – before flattening

<footnote>subsequently formulated in a Java-like setting by various authors (Smith and Drossopoulou, 2005; Nierstrasz et al., 2006; Reppy and Turon, 2007; Bono et al., 2008; Liquori and Spiwack, 2008; Bettini et al., 2013b; Bettini and Damiani, 2017).</footnote>

<footnote n="3">³ The constructs of the JIGSAW framework (Bracha, 1992) were formalized in a Java-like setting by means of the FGig calculus (Lagorio et al., 2009, 2012).</footnote>

<footnote n="4">⁴ To extend VMs with delta operations on export clauses is straightforward. It would sometimes allow to shorten export clauses. On the other hand, since implicit flattening drops all unused imports, deltas on import clauses provide no advantage.</footnote>
<figure><img src="image_10.png" /><figcaption>Fig. 6. ABS-VM abridged syntax — the fragment of the grammar describing the syntax of Vf-ABS is highlighted in gray.</figcaption></figure>

— whether a program *Prog* satisfies the PEV and whether all variants of all VMs in *Prog* can be generated and would form (as a whole) a variability free ABS program that satisfies certain well-formedness conditions (Section 9).

## 5. Syntax of variability modules

Fig. 6 defines the syntax of ABS with VMs (ABS-VM, for short) as an extension of variability-free ABS (Vf-ABS, for short). Vf-ABS is the sequential, OO fragment of ABS (Johnsen et al., 2010; Hähnle, 2013) and ABS-VM extends it with VM concepts.<fnref n="5" />

We write *M* to denote module names, *C* for class names, *I* for interface names, *K* for feature configuration names, *P* for product names, *D* for delta names, *m* for method names, and *f* for field names. A *named element* is either a (variability) module, an *interface/class* definition, a *method header*, a *field/method* definition, a *method formal parameter* declaration, a *delta*, a *class/attribute/interfaceheader* operation, or a *delta activation condition*. Given a *named element* *X*, we write *name(X)* to denote its name. Following Igarashi et al. (2001), $\bar{X}$ denotes a possibly empty finite sequence of elements *X*. If the elements in $\bar{X}$ are named, we assume their names are pairwise distinct.

<footnote n="5">⁵ Even though ABS supports variability management based on deltas, for presentational purposes, we singled out Vf-ABS. We stress that the syntax of delta definitions in ABS-VM is essentially identical to ABS syntax.</footnote>
<figure><img src="image_9.png" /><figcaption>Fig. 6. ABS-VM abridged syntax — the fragment of the grammar describing the syntax of Vf-ABS is highlighted in gray.</figcaption></figure>

— whether a program *Prg* satisfies the PEV and whether all variants of all VMs in *Prg* can be generated and would form (as a whole) a variability free ABS program that satisfies certain well-formedness conditions (Section 9).

## 5. Syntax of variability modules

Fig. 6 defines the syntax of ABS with VMs (ABS-VM, for short) as an extension of variability-free ABS (Vf-ABS, for short). Vf-ABS is the sequential, OO fragment of ABS (Johnsen et al., 2010; Hähnle, 2013) and ABS-VM extends it with VM concepts.<fnref n="5" />

We write *M* to denote module names, *C* for class names, *I* for interface names, *K* for feature configuration names, *P* for product names, *D* for delta names, *m* for method names, and *f* for field names. A *named element* is either a (variability) module, an *interface/class* definition, a *method header*, a *field/method* definition, a *method formal parameter* declaration, a *delta*, a *class/attribute/interfaceheader* operation, or a *delta activation condition*. Given a *named element* *X*, we write *name(X)* to denote its name. Following Igarashi et al. (2001), $\bar{X}$ denotes a possibly empty finite sequence of elements *X*. If the elements in $\bar{X}$ are named, we assume their names are pairwise distinct.

<footnote n="5">⁵ Even though ABS supports variability management based on deltas, for presentational purposes, we singled out Vf-ABS. We stress that the syntax of delta definitions in ABS-VM is essentially identical to ABS syntax.</footnote>
## 5.1. ABS-VM syntax

A program is a sequence of VMs. A VM consists of a header (MdlH), a core part (MdlC), and a delta part (Md1D). A VM header comprises the keyword module followed by the name of the VM, by some (possibly none) import and export clauses (listing the class/interface/configuration/product names, respectively, that are exported or imported by the VM), by the optional definition of a feature model (where F are the features and Φ is a propositional formula over features), by a list of configuration definitions, and by a list of product definitions. A configuration expression KE is a set-theoretic expression over feature sets (+, * and — denote union, intersection and difference, respectively). A product definition PD is closed if it is of the form product P [ for M ] = KE, otherwise it is open. The clauses in an open product definition are examined in sequence until the first applicable clause is found.<fnref n="6" /> The right-hand sides of configuration definitions do not contain product names, and the right-hand sides of closed product definitions do not contain open product names. Recursive configuration/product definitions are forbidden.

Both the module core part and the module delta part may be empty. A module core part comprises a sequence of class and interface definitions Defn. As an extension to ABS syntax, each of these definitions may be prefixed by the keyword unique. Each use of a class, interface or product name imported from another module may be prefixed by the name of the module—the name of the module must be used if there are ambiguities (for example, when an interface with name I is imported from two different modules). Moreover, each use of a non-unique class or interface imported from another module must be followed by a with-clause, specifying (by means of a configuration expression) the variant of the VM it is taken from.

**Remark 2 (On UMs and Vf-ABS Modules).** A UM, as defined in Section 2, is a Vf-ABS module if and only if it does not contain product definitions or occurrences of the with keyword.

The module delta part comprises a sequence of delta definitions $\bar{Dlt}$ followed by configuration knowledge CK. Each delta specifies a number of changes to the module core part. A delta comprises the keyword delta followed by the name of the delta, by a sequence of class operations $\bar{Co}$ and by a sequence of interface operations $\bar{Io}$. An interface operation can add or remove an interface definition, or modify it by adding/removing names to the list of the extended interfaces or by adding/removing method headers. A class operation can add or remove a class definition, or modify it by adding/removing names to the list of the implemented interfaces, by adding/removing fields or by adding/removing/modifying methods. Modifying a method means to replace its body with a new body. The new body may call its previous incarnation via the reserved method name original.

Configuration knowledge CK provides a mapping from products to variants by describing the connection between deltas and features: it specifies an activation condition Φ (a propositional formula over features) for each delta D by means of a DAC clause; and it specifies an application ordering between deltas by means of a sequence of DAO clauses. Each DAO clause specifies a partial order over the set of deltas in terms of a total order on disjoint subsets of delta names—a DAO clause allows developers to express (as a partial order) dependencies between the deltas (which are usually semantic “requires” relations Bettini et al., 2013a). The overall delta application order is the union of these partial orders—the compiler checks that the resulting relation R

represents a specification that is consistent (i.e., R is a partial order) and unambiguous (i.e., all the total delta application orders that respect R generate the same variant for each product). Techniques for checking that R is unambiguous are described in the literature (Bettini et al., 2013a; Lienhardt and Clarke, 2012). Without loss of generality, for each VM, we assume that the total order in which delta definitions are listed is compatible with R.

## 5.2. ABS-VM sanity conditions

In the rest of the paper, without loss of generality, we assume each ABS-VM program Prg to satisfy a number of sanity conditions that enforce minimal consistency requirements for ABS-VM programs. These sanity conditions, listed below, apply to each VM name M occurring anywhere in Prg.

1. Prg contains a definition of the VM M.

2. If M is a main module (see end of Section 2) then any other VM of Prg does not contain the keyword init (i.e., Prg contains at most one main module).

3. If M contains a clause import tC from M' then M' ≠ M and all traded names in tC occur in the export clause of M'.

4. All class references CR and interface references IR occurring in M are qualified, that is of the form M' . N [ with ... ] for some module name M' and class/interface name N such that if M' ≠ M then M contains the import clause import tC from M' where either tC = * or N occurs in tC.

5. All traded names occurring in the export clause of M are defined in M: each configuration/product name is defined in the module header and each class/interface name is defined in the module core part or added by some delta in the module delta part.

6. If M is a UM (see end of Section 2) then all its class/interface definitions have the qualifier unique.

7. No open product names are exported and no product names with a declaration of the form product P for M' = ... are exported.

8. The following properties hold for different definitions in M:

(a) configuration K = KE: (i) all feature names occurring in KE are features of M and all configuration names occurring in KE have been already defined in M; (ii) no product name occurs in KE.

(b) product P = KE: (i) condition (8a). (ii) above holds; (ii) all product names occurring in KE have been already defined in M and are closed; (iii) KE denotes a product of M.

(c) product P for M' = KE: (i) M ≠ M'; (ii) all feature names occurring in KE are features of M' and all configuration/product names occurring in KE are imported from M'; (iii) KE denotes a product of M'.

(d) product P for M' = {$\Phi_1$= KE₁, ..., $\Phi_n$= KEₙ} (n ≥ 1): (i) M ≠ M'; (ii) for all 1 ≤ j ≤ n, all configuration/product names occurring in KEⱼ are imported from M'; (iii) for all 1 ≤ j ≤ n, all feature names occurring in $\Phi_j$ are features of M and all feature names occurring in KEⱼ are features of M'; (iv) for all 1 ≤ j ≤ n, at least one product of M satisfies (∧$_{1≤i≤n}$¬$\Phi_i$) ∧ $\Phi_j$, and KEⱼ denotes a product of M'; (v) all products of M satisfy $\bigvee_{1≤i≤n}$ $\Phi_i$.

(e) product P = {$\Phi_1$= KE₁, ..., $\Phi_n$= KEₙ} (n ≥ 1): (i) for all 1 ≤ j ≤ n, all configuration/product names occurring in KEⱼ have been already defined in M; (ii) the condition obtained from condition (8d). (iii) above by replacing M' with M holds; (iii) the condition obtained from condition (8d). (iv) above by replacing M' with M holds; (iv) condition (8d). (v) above holds.

<footnote n="6">⁶ The sanity conditions (see Section 5.2) guarantee that such a clause exists.</footnote>
## 5.1. ABS-VM syntax

A program is a sequence of VMs. A VM consists of a header (MdlH), a core part (MdlC), and a delta part (Md1D). A VM header comprises the keyword module followed by the name of the VM, by some (possibly none) import and export clauses (listing the class/interface/configuration/product names, respectively, that are exported or imported by the VM), by the optional definition of a feature model (where F are the features and Φ is a propositional formula over features), by a list of configuration definitions, and by a list of product definitions. A configuration expression KE is a set-theoretic expression over feature sets (+, * and — denote union, intersection and difference, respectively). A product definition PD is closed if it is of the form product P [ for M ] = KE, otherwise it is open. The clauses in an open product definition are examined in sequence until the first applicable clause is found.<fnref n="6" /> The right-hand sides of configuration definitions do not contain product names, and the right-hand sides of closed product definitions do not contain open product names. Recursive configuration/product definitions are forbidden.

Both the module core part and the module delta part may be empty. A module core part comprises a sequence of class and interface definitions Defn. As an extension to ABS syntax, each of these definitions may be prefixed by the keyword unique. Each use of a class, interface or product name imported from another module may be prefixed by the name of the module—the name of the module must be used if there are ambiguities (for example, when an interface with name I is imported from two different modules). Moreover, each use of a non-unique class or interface imported from another module must be followed by a with-clause, specifying (by means of a configuration expression) the variant of the VM it is taken from.

**Remark 2 (On UMs and Vf-ABS Modules).** A UM, as defined in Section 2, is a Vf-ABS module if and only if it does not contain product definitions or occurrences of the with keyword.

The module delta part comprises a sequence of delta definitions $\bar{Dlt}$ followed by configuration knowledge CK. Each delta specifies a number of changes to the module core part. A delta comprises the keyword delta followed by the name of the delta, by a sequence of class operations $\bar{Co}$ and by a sequence of interface operations $\bar{Io}$. An interface operation can add or remove an interface definition, or modify it by adding/removing names to the list of the extended interfaces or by adding/removing method headers. A class operation can add or remove a class definition, or modify it by adding/removing names to the list of the implemented interfaces, by adding/removing fields or by adding/removing/modifying methods. Modifying a method means to replace its body with a new body. The new body may call its previous incarnation via the reserved method name original.

Configuration knowledge CK provides a mapping from products to variants by describing the connection between deltas and features: it specifies an activation condition Φ (a propositional formula over features) for each delta D by means of a DAC clause; and it specifies an application ordering between deltas by means of a sequence of DAO clauses. Each DAO clause specifies a partial order over the set of deltas in terms of a total order on disjoint subsets of delta names—a DAO clause allows developers to express (as a partial order) dependencies between the deltas (which are usually semantic “requires” relations Bettini et al., 2013a). The overall delta application order is the union of these partial orders—the compiler checks that the resulting relation R

represents a specification that is consistent (i.e., R is a partial order) and unambiguous (i.e., all the total delta application orders that respect R generate the same variant for each product). Techniques for checking that R is unambiguous are described in the literature (Bettini et al., 2013a; Lienhardt and Clarke, 2012). Without loss of generality, for each VM, we assume that the total order in which delta definitions are listed is compatible with R.

## 5.2. ABS-VM sanity conditions

In the rest of the paper, without loss of generality, we assume each ABS-VM program Prg to satisfy a number of sanity conditions that enforce minimal consistency requirements for ABS-VM programs. These sanity conditions, listed below, apply to each VM name M occurring anywhere in Prg.

1. Prg contains a definition of the VM M.

2. If M is a main module (see end of Section 2) then any other VM of Prg does not contain the keyword init (i.e., Prg contains at most one main module).

3. If M contains a clause import tC from M' then M' ≠ M and all traded names in tC occur in the export clause of M'.

4. All class references CR and interface references IR occurring in M are qualified, that is of the form M' . N [ with ... ] for some module name M' and class/interface name N such that if M' ≠ M then M contains the import clause import tC from M' where either tC = * or N occurs in tC.

5. All traded names occurring in the export clause of M are defined in M: each configuration/product name is defined in the module header and each class/interface name is defined in the module core part or added by some delta in the module delta part.

6. If M is a UM (see end of Section 2) then all its class/interface definitions have the qualifier unique.

7. No open product names are exported and no product names with a declaration of the form product P for M' = ... are exported.

8. The following properties hold for different definitions in M:

(a) configuration K = KE: (i) all feature names occurring in KE are features of M and all configuration names occurring in KE have been already defined in M; (ii) no product name occurs in KE.

(b) product P = KE: (i) condition (8a). (ii) above holds; (ii) all product names occurring in KE have been already defined in M and are closed; (iii) KE denotes a product of M.

(c) product P for M' = KE: (i) M ≠ M'; (ii) all feature names occurring in KE are features of M' and all configuration/product names occurring in KE are imported from M'; (iii) KE denotes a product of M'.

(d) product P for M' = {$\Phi_1$= KE₁, ..., $\Phi_n$= KEₙ} (n ≥ 1): (i) M ≠ M'; (ii) for all 1 ≤ j ≤ n, all configuration/product names occurring in KEⱼ are imported from M'; (iii) for all 1 ≤ j ≤ n, all feature names occurring in $\Phi_j$ are features of M and all feature names occurring in KEⱼ are features of M'; (iv) for all 1 ≤ j ≤ n, at least one product of M satisfies ($\bigwedge_{1 \le i \le n} \neg \Phi_i$) ∧ $\Phi_j$, and KEⱼ denotes a product of M'; (v) all products of M satisfy $\bigvee_{1 \le i \le n} \Phi_i$.

(e) product P = {$\Phi_1$= KE₁, ..., $\Phi_n$= KEₙ} (n ≥ 1): (i) for all 1 ≤ j ≤ n, all configuration/product names occurring in KEⱼ have been already defined in M; (ii) the condition obtained from condition (8d). (iii) above by replacing M' with M holds; (iii) the condition obtained from condition (8d). (iv) above by replacing M' with M holds; (iv) condition (8d). (v) above holds.

<footnote n="6">6 The sanity conditions (see Section 5.2) guarantee that such a clause exists.</footnote>
9. If M contains an occurrence of `new M'.C()` with KE or `M'.I` with KE: (i) all feature names occurring in KE are features of `M'`; (ii) if `M'=M` then all configuration/product names occurring in KE are defined in M; (iii) if `M'≠M` then all configuration/product names occurring in KE are either imported from `M'` or defined in M by a declaration of the form `product P for M' = ...`; (iv) either KE does not contain occurrences of open product names or it is an open product name; (v) KE denotes a product of `M'`.

To check whether a program satisfies the sanity conditions is straightforward: for each VM M:

* Conditions (1), (2) can be checked by inspection of Prg.

* Condition (3) can be checked by inspection of M and of the header of the modules `M'` listed in the import clauses of M.

* Conditions (4)–(7), (8a), (8b), (8c)(i), (8d)(i), (8e)(i)–(ii), (9)(i)–(ii) can be checked by inspection of M, where condition (8b)(iii) also requires to evaluate a propositional formula.

* Conditions (8c)(ii)–(iii), (8d)(ii)–(iii), and (9)(iii)–(iv) can be checked by inspection of M and of the header of `M'`, where conditions (8c)(iii) and (9)(v) also requires to evaluate a propositional formula.

* Conditions (8d)(iv)–(v), (8e)(iii)–(iv) can be checked with a SAT solver (Alouneh et al., 2019). We call them SAT sanity conditions.

It is worth observing that sanity conditions (1)–(5) apply as well to Vf-ABS programs. When they are satisfied for a given Vf-ABS program we say it is *sane*.

# 6. Encapsulated variability

In Section 6.1 we formalize the principle of encapsulated variability (PEV) that was informally introduced in Section 4. In Section 6.2, we address the issue of inferring the maximal set of class/interface declarations that can soundly be annotated with unique.

## 6.1. PEV-compliance

To formalize PEV-compliance, we first introduce some auxiliary definitions. Namely, the notion of dependency, and the functions CORE, UNIQUE and BASE.

**Definition 1 (Dependency).** A VM `M'` depends on a VM `M` if `M'` contains an occurrence of `M.N`, where `N` is a class/interface name. An occurrence of `M.I` with KE or `new M.C()` with KE is called with-dependency (on `M.I` or `M.C`, respectively), while an occurrence of `M.I` or `new M.C(...)` (i.e. not followed by a `with`) is called with-free-dependency (on `M.I` or `M.C`, respectively).

* A dependency of the form `... with KE` is called with-open-dependency if KE contains an occurrence of an open product name `P`, it is called with-closed-dependency otherwise.

* A dependency is called ground if it is: either with-free or of the form `... with π`, where `π` is a set of features {$F_1, ..., F_n$} ($n \ge 0$).

Given the notion of dependency, we now define the CORE function, which returns the set of class and interfaces defined in the core part of a VM, the UNIQUE function returning the subset of the core that is annotated as unique, and the BASE function returning the subset of the core that is modified by some delta.

**Definition 2 (Functions CORE, UNIQUE, BASE).** Given a program Prg, then for all VMs M of Prg: CORE(Prg, M) is the set of qualified names `M.N` of all interfaces/classes `N` whose definition occurs in the core part of M; UNIQUE(Prg, M) ⊆ CORE(Prg, M) contains those class/interface names whose declaration is annotated with unique; BASE(Prg, M) ⊆ CORE(Prg, M) contains those class/interface names that are modified, removed or added by some delta of M.

We can now formalize PEV-compliance in terms of the above functions as follows.

**Definition 3 (PEV-Compliance).** A program Prg is PEV-compliant iff for all VMs M of Prg:

1. `UNIQUE(Prg, M) ∩ BASE(Prg, M) = ∅`.

2. For all `M.N ∈ UNIQUE(Prg, M)` the definition Defn of `N` (in the core part `MdlC` of M) does not contain with-open-dependencies and, for all with-free-dependencies on `M.N'` occurring in Defn, it holds that `M.N' ∈ UNIQUE(Prg, M)`.

3. For all with-free-dependencies on `M'.N` occurring in `M`: if `M' ≠ M` then `M'.N ∈ UNIQUE(Prg, M')`.

To check whether a program is PEV-compliant is straightforward and programs that are not PEV-compliant are rejected by the compiler. The code in Section 2 is PEV-compliant.

**Example 1 (Lack of PEV-Compliance).** Consider the three programs in Fig. 7. None of them is PEV-compliant. The first program Prg1 violates the first condition: `I` is part of `UNIQUE(Prg1, M)` (because of its annotation) and of `BASE(Prg1, M)` (because it is modified by `D`).

The second program Prg2 violates the second condition: `M.I` has a dependency on `M.J` that is not unique: `M.J ∉ UNIQUE(Prg2, M)`. Because of this, it is not determined which interface is extended, as there may be multiple variants even for dependencies within the same module. The third program Prg3 is analogous for dependencies to other modules and violates the third condition, as `M'.I ∉ UNIQUE(Prg3, M')`.

According to the PEV, VMs support two types of interaction among variants:

**Variant interoperability.** Different variants of the same VM can co-exist and cooperate via unique classes/interfaces. For instance, in the railway station MPL of Section 2, all interfaces are unique and all classes are not unique (which is a common pattern). Then, in line 22 of Fig. 4, an instance of class CSig in the variant of VM Signal for product `{Light}` receives an invocation of method `eqAspect` that declares an argument of type Signal takes as parameter an instance of CSig in the variant of Signal for product `{Form}`.

**Variant interdependence.** The code of a variant of a VM `M1` can depend on the code of a variant of a VM `M2` (and possibly vice versa). I.e., the code of `M1` refers to unique classes/interfaces of `M2` (via with-free-dependencies) or to classes/interfaces of a specific variant of `M2` (via with-dependencies). A special case of variant interdependence is when `M1 = M2`, i.e., `M1` has a with-dependency on a class/interface of `M1` itself. Then in the flattened program a variant of `M1` will contain an occurrence of a class/interface name that is declared in a different variant of `M1`.

## 6.2. Maximal set of unique annotations

The following definition and theorem show that, given an ABS-VM program that satisfies the sanity conditions (see Section 5.2) one can automatically infer the maximal set of class/interface declarations that can soundly be annotated with unique.
9. If M contains an occurrence of `new M'.C()` with KE or `M'.I` with KE: (i) all feature names occurring in KE are features of `M'`; (ii) if `M'=M` then all configuration/product names occurring in KE are defined in M; (iii) if `M'≠M` then all configuration/product names occurring in KE are either imported from `M'` or defined in M by a declaration of the form `product P for M' = ...`; (iv) either KE does not contain occurrences of open product names or it is an open product name; (v) KE denotes a product of `M'`.

To check whether a program satisfies the sanity conditions is straightforward: for each VM M:

* Conditions (1), (2) can be checked by inspection of Prg.

* Condition (3) can be checked by inspection of M and of the header of the modules `M'` listed in the import clauses of M.

* Conditions (4)–(7), (8a), (8b), (8c)(i), (8d)(i), (8e)(i)–(ii), (9)(i)–(ii) can be checked by inspection of M, where condition (8b)(iii) also requires to evaluate a propositional formula.

* Conditions (8c)(ii)–(iii), (8d)(ii)–(iii), and (9)(iii)–(iv) can be checked by inspection of M and of the header of `M'`, where conditions (8c)(iii) and (9)(v) also requires to evaluate a propositional formula.

* Conditions (8d)(iv)–(v), (8e)(iii)–(iv) can be checked with a SAT solver (Alouneh et al., 2019). We call them SAT sanity conditions.

It is worth observing that sanity conditions (1)–(5) apply as well to Vf-ABS programs. When they are satisfied for a given Vf-ABS program we say it is *sane*.

# 6. Encapsulated variability

In Section 6.1 we formalize the principle of encapsulated variability (PEV) that was informally introduced in Section 4. In Section 6.2, we address the issue of inferring the maximal set of class/interface declarations that can soundly be annotated with unique.

## 6.1. PEV-compliance

To formalize PEV-compliance, we first introduce some auxiliary definitions. Namely, the notion of dependency, and the functions CORE, UNIQUE and BASE.

**Definition 1 (Dependency).** A VM `M'` depends on a VM `M` if `M'` contains an occurrence of `M.N`, where `N` is a class/interface name. An occurrence of `M.I` with KE or `new M.C()` with KE is called with-dependency (on `M.I` or `M.C`, respectively), while an occurrence of `M.I` or `new M.C(...)` (i.e. not followed by a `with`) is called with-free-dependency (on `M.I` or `M.C`, respectively).

* A dependency of the form `... with KE` is called with-open-dependency if KE contains an occurrence of an open product name `P`, it is called with-closed-dependency otherwise.

* A dependency is called ground if it is: either with-free or of the form `... with π`, where `π` is a set of features {$F_1, ..., F_n$} ($n \ge 0$).

Given the notion of dependency, we now define the CORE function, which returns the set of class and interfaces defined in the core part of a VM, the UNIQUE function returning the subset of the core that is annotated as unique, and the BASE function returning the subset of the core that is modified by some delta.

**Definition 2 (Functions CORE, UNIQUE, BASE).** Given a program Prg, then for all VMs M of Prg: CORE(Prg, M) is the set of qualified names `M.N` of all interfaces/classes `N` whose definition occurs in the core part of M; UNIQUE(Prg, M) ⊆ CORE(Prg, M) contains those class/interface names whose declaration is annotated with unique; BASE(Prg, M) ⊆ CORE(Prg, M) contains those class/interface names that are modified, removed or added by some delta of M.

We can now formalize PEV-compliance in terms of the above functions as follows.

**Definition 3 (PEV-Compliance).** A program Prg is PEV-compliant iff for all VMs M of Prg:

1. `UNIQUE(Prg, M) ∩ BASE(Prg, M) = ∅`.

2. For all `M.N ∈ UNIQUE(Prg, M)` the definition Defn of `N` (in the core part `MdlC` of M) does not contain with-open-dependencies and, for all with-free-dependencies on `M.N'` occurring in Defn, it holds that `M.N' ∈ UNIQUE(Prg, M)`.

3. For all with-free-dependencies on `M'.N` occurring in `M`: if `M' ≠ M` then `M'.N ∈ UNIQUE(Prg, M')`.

To check whether a program is PEV-compliant is straightforward and programs that are not PEV-compliant are rejected by the compiler. The code in Section 2 is PEV-compliant.

**Example 1 (Lack of PEV-Compliance).** Consider the three programs in Fig. 7. None of them is PEV-compliant. The first program Prg1 violates the first condition: `I` is part of `UNIQUE(Prg1, M)` (because of its annotation) and of `BASE(Prg1, M)` (because it is modified by `D`).

The second program Prg2 violates the second condition: `M.I` has a dependency on `M.J` that is not unique: `M.J ∉ UNIQUE(Prg2, M)`. Because of this, it is not determined which interface is extended, as there may be multiple variants even for dependencies within the same module. The third program Prg3 is analogous for dependencies to other modules and violates the third condition, as `M'.I ∉ UNIQUE(Prg3, M')`.

According to the PEV, VMs support two types of interaction among variants:

**Variant interoperability.** Different variants of the same VM can co-exist and cooperate via unique classes/interfaces. For instance, in the railway station MPL of Section 2, all interfaces are unique and all classes are not unique (which is a common pattern). Then, in line 22 of Fig. 4, an instance of class CSig in the variant of VM Signal for product `{Light}` receives an invocation of method `eqAspect` that declares an argument of type Signal takes as parameter an instance of CSig in the variant of Signal for product `{Form}`.

**Variant interdependence.** The code of a variant of a VM `M1` can depend on the code of a variant of a VM `M2` (and possibly vice versa). I.e., the code of `M1` refers to unique classes/interfaces of `M2` (via with-free-dependencies) or to classes/interfaces of a specific variant of `M2` (via with-dependencies). A special case of variant interdependence is when `M1 = M2`, i.e., `M1` has a with-dependency on a class/interface of `M1` itself. Then in the flattened program a variant of `M1` will contain an occurrence of a class/interface name that is declared in a different variant of `M1`.

## 6.2. Maximal set of unique annotations

The following definition and theorem show that, given an ABS-VM program that satisfies the sanity conditions (see Section 5.2) one can automatically infer the maximal set of class/interface declarations that can soundly be annotated with unique.
```pascal
module M;
unique interface I {}
delta D; modifies interface I { adds Unit m(); }
```

```pascal
module M;
unique interface I extends J {}
interface J {}
delta D; modifies interface J { adds Unit m(); }
```

```pascal
module M;
import * from M';
interface J extends I {}
module M'; export *;
interface I {}
delta D; modifies interface I { adds Unit m(); }
```

<caption>**Fig. 7.** Not PEV-compliant programs.</caption>

**Definition 4 (Function MaxUNIQUE).** For every ABS-VM program $\mathit{Prg}$, for all VM $\mathcal{M}$ of $\mathit{Prg}$, let $S_{\mathcal{M}} = \mathit{CORE}(\mathit{Prg}, \mathcal{M}) \setminus \mathit{BASE}(\mathit{Prg}, \mathcal{M})$ and $F_{\mathcal{M}}: (2^{S_{\mathcal{M}}}, \subseteq) \rightarrow (2^{S_{\mathcal{M}}}, \subseteq)$ is defined as the non-increasing monotone function such that: $F_{\mathcal{M}}(X)$ is the subset of $X$ obtained by removing simultaneously all classes/interfaces $\mathcal{M} \cdot \mathcal{N}$ such that the definition of $\mathcal{N}$ (in the core part of $\mathcal{M}$) contains a with-free-dependency on a class/interface $\mathcal{M} \cdot \mathcal{N}' \notin X$ or contains a with-open-dependency. Then $\mathit{MaxUNIQUE}(\mathit{Prg}, \mathcal{M})$ is the set computed by iterating $F_{\mathcal{M}}(X)$ on $S_{\mathcal{M}}$ until a fixpoint is reached, i.e. $U = F_{\mathcal{M}}(S_{\mathcal{M}})$ such that $U = F_{\mathcal{M}}(U)$ for some $n \ge 0$.

Function $\mathit{MaxUNIQUE}(\mathit{Prg}, \mathcal{M})$ is computed locally on the VM $\mathcal{M}$ and always terminates (since $F_{\mathcal{M}}$ is non-increasing monotone and $S_{\mathcal{M}}$ is finite). Unfortunately, a program $\mathit{Prg}$ such that, for all VM $\mathcal{M}$ of $\mathit{Prg}$, $\mathit{UNIQUE}(\mathit{Prg}, \mathcal{M}) = \mathit{MaxUNIQUE}(\mathit{Prg}, \mathcal{M})$ may not adhere to the PEV, because of item (3) in **Definition 3**. However, by the following theorem, if such a $\mathit{Prg}$ does not adhere to the PEV then any program obtained from $\mathit{Prg}$ by adding or removing unique annotations does not adhere to the PEV.

**Theorem 1 (Maximal Set of Unique Annotations Admitting PEV).**
For all programs $\mathit{Prg}$ adhering to the PEV: (i) for all VM of $\mathit{Prg}$, $\mathit{UNIQUE}(\mathit{Prg}, \mathcal{M}) \subseteq \mathit{MaxUNIQUE}(\mathit{Prg}, \mathcal{M})$; (ii) the program $\mathit{Prg}'$ obtained by adding unique annotations to $\mathit{Prg}$ until, for all VM $\mathcal{M}$, $\mathit{UNIQUE}(\mathit{Prg}', \mathcal{M}) = \mathit{MaxUNIQUE}(\mathit{Prg}', \mathcal{M})$, adheres to PEV.

**Proof.** By **Definition 4** $F_{\mathcal{M}}$ is a set-theoretic inclusion-preserving map and the powerset $2^{S_{\mathcal{M}}}$ is a complete lattice. By the Knaster-Tarski theorem (Roman, 2008) there exist smallest and greatest fixpoints of $F_{\mathcal{M}}$. Moreover, the PEV (**Definition 3**(2)) requires $\mathit{UNIQUE}(\mathit{Prg}, \mathcal{M})$ to be a fixpoint of $F_{\mathcal{M}}$. Now item (i) holds, because the set $\mathit{MaxUNIQUE}(\mathit{Prg}, \mathcal{M})$ is the greatest fixpoint of $F_{\mathcal{M}}$—the proof is as follows: let $G$ be the greatest fixpoint of $F_{\mathcal{M}}$; clearly $G \subseteq S_{\mathcal{M}}$ and (since $F_{\mathcal{M}}$ is non-increasing monotone) $G = F_{\mathcal{M}}^n(G) \subseteq F_{\mathcal{M}}^n(S_{\mathcal{M}})$ for all $n \in \mathbb{N}$; but $\mathit{MaxUNIQUE}(\mathit{Prg}, \mathcal{M})$ is the fixpoint obtained by iterating $F_{\mathcal{M}}$ on $S_{\mathcal{M}}$. Item (ii) holds, because $\mathit{Prg}'$ satisfies **Definition 3**—in particular: item (1) holds by definition of $S_{\mathcal{M}}$ and non-increasing monotonicity of $F_{\mathcal{M}}$; item (2) is satisfied by any fixpoint of $F_{\mathcal{M}}$; since $\mathit{Prg}$ satisfies item (3), so does $\mathit{Prg}'$. $\square$

# 7. Flattening semantics of variability modules

In this section, we consider (without loss of generality) sane ABS-VM programs that are in normal form, according to the following definition.

**Definition 5 (ABS-VM Normal Form).** An ABS-VM program $\mathit{Prg}$ is in normal form if: (i) $\mathit{Prg}$ is PEV-compliant; (ii) all configuration definitions and closed product definitions are resolved in $\mathit{Prg}$, i.e.:

* All corresponding declarations are removed from $\mathit{Prg}$.

* All occurrences of names of such definitions are removed from export/import clauses of $\mathit{Prg}$.

* All occurrences of such definitions in $\mathit{Prg}$ are replaced with their value (a set of features)<fnref n="8" /> and all the occurrences of with KE such that KE is not an open product name are replaced with with $\pi$, where $\pi$ is the value of KE (a product).<fnref n="9" />

In Section 7.1 we introduce auxiliary functions for the extraction of relevant information from ABS-VM programs. In Section 7.2 we give the semantics of ABS-VM in terms of rewrite rules for transforming an ABS-VM program into a Vf-ABS program.

## 7.1. Auxiliary functions

**Definition 6 (Lookup Functions).** Given a VM $\mathcal{M}$ of $\mathit{Prg}$ we define the sets:

* `mdlUnique(\mathit{Prg}, \mathcal{M})` for all interface/class definitions in the Module Core Part of $\mathcal{M}$ annotated with unique.

* `mdlNotUnique(\mathit{Prg}, \mathcal{M})` for all interface/class definitions not contained in `mdlUnique(\mathit{Prg}, \mathcal{M})`.

* `mdlInit(\mathit{Prg}, \mathcal{M})` for the init block of $\mathcal{M}$, if it exists, or the empty sequence otherwise; also `mdlInit(\mathit{Prg})` for the name $\mathcal{M}$ of the single VM such that `mdlInit(\mathit{Prg}, \mathcal{M})` is not the empty sequence.

* `mdlDelta(\mathit{Prg}, \mathcal{M}, \pi)`, where $\pi$ is a product of $\mathcal{M}$, for any ordered sequence $\underline{\mathrm{init}}$ containing exactly those deltas of $\mathcal{M}$ activated by $\pi$, respecting the order among deltas specified in the configuration knowledge of $\mathcal{M}$.

For technical reasons we extend the set of products of each VM $\mathcal{M}$ with a dedicated auxiliary product, denoted $\bot$, identifying the unique part of $\mathcal{M}$.

**Definition 7 (Extended Product).** An extended product $\mathrm{xc}$ of a VM $\mathcal{M}$ is either a product $\pi$ of $\mathcal{M}$ or the symbol $\bot$ not used for any other product.

We define notation for extracting the meaning of ground (**Definition 1**) dependencies in the Module Core Part of a given VM of a given program. In the following, we use $\delta$ to range over dependencies.

<footnote n="7">⁷ Therefore, because of sanity condition (7), export/import clauses no longer contain product names.</footnote>

<footnote n="8">⁸ This is always possible, because configuration definitions and closed product definitions cannot depend on open product definitions by sanity conditions (8a)(ii), (8b)(ii), and (8c)(ii).</footnote>

<footnote n="9">⁹ Because of sanity condition (9)(v).</footnote>
```pascal
module M;
unique interface I {}
delta D; modifies interface I { adds Unit m(); }
```

```pascal
module M;
unique interface I extends J {}
interface J {}
delta D; modifies interface J { adds Unit m(); }
```

```pascal
module M;
import * from M';
interface J extends I {}
module M'; export *;
interface I {}
delta D; modifies interface I { adds Unit m(); }
```

<caption>**Fig. 7.** Not PEV-compliant programs.</caption>

**Definition 4 (Function MaxUNIQUE).** For every ABS-VM program $\mathit{Prg}$, for all VM $\mathcal{M}$ of $\mathit{Prg}$, let $S_{\mathcal{M}} = \mathit{CORE}(\mathit{Prg}, \mathcal{M}) \setminus \mathit{BASE}(\mathit{Prg}, \mathcal{M})$ and $F_{\mathcal{M}}: (2^{S_{\mathcal{M}}}, \subseteq) \rightarrow (2^{S_{\mathcal{M}}}, \subseteq)$ is defined as the non-increasing monotone function such that: $F_{\mathcal{M}}(X)$ is the subset of $X$ obtained by removing simultaneously all classes/interfaces $\mathcal{M}.N$ such that the definition of $\mathcal{N}$ (in the core part of $\mathcal{M}$) contains a *with-free-dependency* on a class/interface $\mathcal{M}.N' \notin X$ or contains a *with-open-dependency*. Then $\mathit{MaxUNIQUE}(\mathit{Prg}, \mathcal{M})$ is the set computed by iterating $F_{\mathcal{M}}(X)$ on $S_{\mathcal{M}}$ until a fixpoint is reached, i.e. $U = F_{\mathcal{M}}^{n}(S_{\mathcal{M}})$ such that $U = F_{\mathcal{M}}(U)$ for some $n \ge 0$.

Function $\mathit{MaxUNIQUE}(\mathit{Prg}, \mathcal{M})$ is computed locally on the VM $\mathcal{M}$ and always terminates (since $F_{\mathcal{M}}$ is non-increasing monotone and $S_{\mathcal{M}}$ is finite). Unfortunately, a program $\mathit{Prg}$ such that, for all VM $\mathcal{M}$ of $\mathit{Prg}$, $\mathit{UNIQUE}(\mathit{Prg}, \mathcal{M}) = \mathit{MaxUNIQUE}(\mathit{Prg}, \mathcal{M})$ may not adhere to the PEV, because of item (3) in **Definition 3**. However, by the following theorem, if such a $\mathit{Prg}$ does not adhere to the PEV then any program obtained from $\mathit{Prg}$ by adding or removing unique annotations does not adhere to the PEV.

**Theorem 1 (Maximal Set of Unique Annotations Admitting PEV).**
For all programs $\mathit{Prg}$ adhering to the PEV: (i) for all VM of $\mathit{Prg}$, $\mathit{UNIQUE}(\mathit{Prg}, \mathcal{M}) \subseteq \mathit{MaxUNIQUE}(\mathit{Prg}, \mathcal{M})$; (ii) the program $\mathit{Prg}'$ obtained by adding unique annotations to $\mathit{Prg}$ until, for all VM $\mathcal{M}$, $\mathit{UNIQUE}(\mathit{Prg}', \mathcal{M}) = \mathit{MaxUNIQUE}(\mathit{Prg}', \mathcal{M})$, adheres to PEV.

**Proof.** By **Definition 4** $F_{\mathcal{M}}$ is a set-theoretic inclusion-preserving map and the powerset $2^{S_{\mathcal{M}}}$ is a complete lattice. By the Knaster-Tarski theorem (Roman, 2008) there exist smallest and greatest fixpoints of $F_{\mathcal{M}}$. Moreover, the PEV (**Definition 3**(2)) requires $\mathit{UNIQUE}(\mathit{Prg}, \mathcal{M})$ to be a fixpoint of $F_{\mathcal{M}}$. Now item (i) holds, because the set $\mathit{MaxUNIQUE}(\mathit{Prg}, \mathcal{M})$ is the greatest fixpoint of $F_{\mathcal{M}}$—the proof is as follows: let $G$ be the greatest fixpoint of $F_{\mathcal{M}}$; clearly $G \subseteq S_{\mathcal{M}}$ and (since $F_{\mathcal{M}}$ is non-increasing monotone) $G = F_{\mathcal{M}}^{n}(G) \subseteq F_{\mathcal{M}}^{n}(S_{\mathcal{M}})$ for all $n \in \mathbb{N}$; but $\mathit{MaxUNIQUE}(\mathit{Prg}, \mathcal{M})$ is the fixpoint obtained by iterating $F_{\mathcal{M}}$ on $S_{\mathcal{M}}$. Item (ii) holds, because $\mathit{Prg}'$ satisfies **Definition 3**—in particular: item (1) holds by definition of $S_{\mathcal{M}}$ and non-increasing monotonicity of $F_{\mathcal{M}}$; item (2) is satisfied by any fixpoint of $F_{\mathcal{M}}$; since $\mathit{Prg}$ satisfies item (3), so does $\mathit{Prg}'$. $\square$

# 7. Flattening semantics of variability modules

In this section, we consider (without loss of generality) sane ABS-VM programs that are in normal form, according to the following definition.

**Definition 5 (ABS-VM Normal Form).** An ABS-VM program $\mathit{Prg}$ is in normal form if: (i) $\mathit{Prg}$ is PEV-compliant; (ii) all configuration definitions and closed product definitions are resolved in $\mathit{Prg}$, i.e.:

* All corresponding declarations are removed from $\mathit{Prg}$.

* All occurrences of names of such definitions are removed from export/import clauses of $\mathit{Prg}$.

* All occurrences of such definitions in $\mathit{Prg}$ are replaced with their value (a set of features)<fnref n="8" /> and all the occurrences of *with KE* such that *KE* is not an open product name are replaced with *with π*, where *π* is the value of *KE* (a product).<fnref n="9" />

In Section 7.1 we introduce auxiliary functions for the extraction of relevant information from ABS-VM programs. In Section 7.2 we give the semantics of ABS-VM in terms of rewrite rules for transforming an ABS-VM program into a Vf-ABS program.

## 7.1. Auxiliary functions

**Definition 6 (Lookup Functions).** Given a VM $\mathcal{M}$ of $\mathit{Prg}$ we define the sets:

* `mdlUnique(\mathit{Prg}, \mathcal{M})` for all interface/class definitions in the Module Core Part of $\mathcal{M}$ annotated with unique.

* `mdlNotUnique(\mathit{Prg}, \mathcal{M})` for all interface/class definitions not contained in `mdlUnique(\mathit{Prg}, \mathcal{M})`.

* `mdlInit(\mathit{Prg}, \mathcal{M})` for the init block of $\mathcal{M}$, if it exists, or the empty sequence otherwise; also `mdlInit(\mathit{Prg})` for the name $\mathcal{M}$ of the single VM such that `mdlInit(\mathit{Prg}, \mathcal{M})` is not the empty sequence.

* `mdlDelta(\mathit{Prg}, \mathcal{M}, \pi)`, where $\pi$ is a product of $\mathcal{M}$, for any ordered sequence $\underline{\mathrm{init}}$ containing exactly those deltas of $\mathcal{M}$ activated by $\pi$, respecting the order among deltas specified in the configuration knowledge of $\mathcal{M}$.

For technical reasons we extend the set of products of each VM $\mathcal{M}$ with a dedicated auxiliary product, denoted $\bot$, identifying the unique part of $\mathcal{M}$.

**Definition 7 (Extended Product).** An extended product $\mathrm{xc}$ of a VM $\mathcal{M}$ is either a product $\pi$ of $\mathcal{M}$ or the symbol $\bot$ not used for any other product.

We define notation for extracting the meaning of ground (**Definition 1**) dependencies in the Module Core Part of a given VM of a given program. In the following, we use $\delta$ to range over dependencies.

<footnote n="7">⁷ Therefore, because of sanity condition (7), export/import clauses no longer contain product names.</footnote>

<footnote n="8">⁸ This is always possible, because configuration definitions and closed product definitions cannot depend on open product definitions by sanity conditions (8a)(ii), (8b)(ii), and (8c)(ii).</footnote>

<footnote n="9">⁹ Because of sanity condition (9)(v).</footnote>
**Definition 8 (Ground Dependency Meaning).** Given a program *Prg*, a VM *M* of *Prg*, a ground dependency *δ* on *M'*.N occurring in *M*, and an extended product *xc* of *M*.

$$ \Downarrow (\mathbf{Prg}, \mathbf{M}, \delta, \mathbf{xc}) = \left\{ \begin{array}{ll} (\mathbf{M}', \perp) & \text{when } \mathbf{M}' \in \text{UNIQUE}(\mathbf{Prg}, \mathbf{M}') \\ (\mathbf{M}', \mathbf{xc}) & \text{when } \mathbf{M}' = \mathbf{M}, \delta \text{ is with-free} \\ & \text{and } \mathbf{M}' \cdot \mathbf{N} \notin \text{UNIQUE}(\mathbf{Prg}, \mathbf{M}) \\ (\mathbf{M}', \pi) & \text{when } \delta \text{ is } \mathbf{M}' \cdot \mathbf{N} \text{ with } \pi \\ & \text{and } \mathbf{M}' \cdot \mathbf{N} \notin \text{UNIQUE}(\mathbf{Prg}, \mathbf{M}') \end{array} \right. $$

If all dependencies in the core part *MdLC* of *M* are ground define $\Downarrow(\mathbf{Prg}, \mathbf{M}, \mathbf{MdLC}, \mathbf{xc}) = \{\Downarrow(\mathbf{Prg}, \mathbf{M}, \delta, \mathbf{xc}) | \delta \text{ is a dependency in } \mathbf{MdLC}\}$.

Flattening a program *Prg* may require to generate more than one variant for each of its VMs. The flattening process generates new names for the generated Vf-ABS modules implementing the required variants and translates the dependencies occurring in *Prg* into uses of (i.e., with-free dependencies on) the generated names. Next we define notation for the names of the generated modules and the translation of with- and with-free-dependencies into the corresponding dependencies among non-variable ABS modules.

**Definition 9 (New Module Name, Dependency Translation).** Given a program *Prg*, a VM *M* of *Prg*, let *xc* be either *⊥* or a product *π* of *M*. We denote with $\Uparrow(\mathbf{M}, \mathbf{xc})$ the name of the module that implements the unique part of the variants of *M* when *xc* = *⊥*, otherwise, the name of the module that implements the non-unique part of the variant of *M* for product *xc*. Moreover, for any ground dependency *δ* on *M'*.N:

$$ \Uparrow(\mathbf{Prg}, \mathbf{M}, \delta, \mathbf{xc}) = \left\{ \begin{array}{ll} \Uparrow(\mathbf{M}', \perp) \cdot \mathbf{N} & \text{when } \mathbf{M}' \cdot \mathbf{N} \in \text{UNIQUE}(\mathbf{Prg}, \mathbf{M}') \\ \Uparrow(\mathbf{M}', \mathbf{xc}) \cdot \mathbf{N} & \text{when } \mathbf{M}' = \mathbf{M}, \delta \text{ is with-free} \\ & \text{and } \mathbf{M}' \cdot \mathbf{N} \notin \text{UNIQUE}(\mathbf{Prg}, \mathbf{M}) \\ \Uparrow(\mathbf{M}', \pi) \cdot \mathbf{N} & \text{when } \delta \text{ is } \mathbf{M}' \cdot \mathbf{N} \text{ with } \pi \\ & \text{and } \mathbf{M}' \cdot \mathbf{N} \notin \text{UNIQUE}(\mathbf{Prg}, \mathbf{M}') \end{array} \right. $$

If all dependencies in the core part *MdLC* of *M* are ground define $\Uparrow(\mathbf{Prg}, \mathbf{M}, \mathbf{MdLC}, \mathbf{xc})$ as the VM core *MdLC* obtained from *MdLC* by replacing each dependency *δ* occurring in it with $\Uparrow(\mathbf{Prg}, \mathbf{M}, \delta, \mathbf{xc})$.

## 7.2. Flattening

The following definition formalizes the application of an ordered delta sequence $\overline{\mathbf{Dlt}}$ (the deltas activated by a product $\pi$ of a VM $\mathbf{M}$) to a sequence $\overline{\mathbf{Defn}}$ of interface/class definitions (the non-unique class/interface definitions in the module core part *MdLC* of $\mathbf{M}$). This is the standard semantics of delta application (Schaefer et al., 2010).

**Definition 10 (Delta Application).** Given a sequence of declarations $\overline{\mathbf{Defn}}$ and an ordered sequence of deltas $\overline{\mathbf{Dlt}}$, we denote with the relation $(\overline{\mathbf{Dlt}}, \overline{\mathbf{Defn}}) \to^* \overline{\mathbf{Defn}'}$ that $\overline{\mathbf{Defn}'}$ is the outcome of the procedure described in Appendix A.

According to the definition above, application of a delta succeeds under the following conditions: (i) each class/interface to be removed or modified is present in the module in focus; (ii) each attribute to be removed or modified is present (with identical header) in the class/interface in focus; (iii) each class, method or field to be added is not present already; (iv) when adding/removing interface references from $\overline{\mathbf{IR}}$ in class C implements $\overline{\mathbf{IR}}$ ... and interface I extends $\overline{\mathbf{IR}}$..., the sequence $\overline{\mathbf{IR}}$ is treated as a set: first interface references are added to $\overline{\mathbf{IR}}$ (this operation succeeds even if some of the added interface references are already present in $\overline{\mathbf{IR}}$) yielding $\overline{\mathbf{IR}'}$—only then interface references are removed (this operation succeeds even when some of the removed interface references are not present in $\overline{\mathbf{IR}'}$).

Let $\pi$ be a product of $\mathbf{M}$. We define a mapping $\sigma = \text{genP}(\mathbf{Prg}, \mathbf{M}, \pi)$ from open product names defined by $\mathbf{M}$

to their corresponding set of features. Given a sequence of interface/class definitions $\overline{\mathbf{Defn}}$ and such a mapping $\sigma$, we denote with $\sigma(\overline{\mathbf{Defn}})$ the definitions obtained from $\overline{\mathbf{Defn}}$ by replacing each occurrence of a open product name with its associated set of features.<fnref n="10" />

We are ready to define the rules that flatten a VM to produce either a Vf-ABS module containing its unique class/interfaces, or a Vf-ABS module containing the non-unique class/interfaces generated for a given product:

**Definition 11 (Local Flattening of VM Relative to an Extended Product).** Let $\mathbf{M}$ be the name of a VM of *Prg*, *xc* an extended product of $\mathbf{M}$. The local flattening of $\mathbf{M}$ relative to *xc* is the Vf-ABS module $\mathbf{MdL}$ such that the judgment $\mathbf{M} \xrightarrow{\mathbf{Prg.xc}} \mathbf{D}, \mathbf{MdL}$ (defined by rules LF:VM⊥ and LF:VM⊥ below) holds, where: (i) $\mathbf{MdL}$ is the code of a Vf-ABS module named $\Uparrow(\mathbf{M}, \mathbf{xc})$, which, for the case $\mathbf{xc} = \perp$ implements the unique part of the variants of $\mathbf{M}$, for the case $\mathbf{xc} = \pi$ implements the non-unique part of the variant of $\mathbf{M}$ for product $\pi$; (ii) $\mathbf{D}$ is the set of pairs (module, extended product) identifying the set of variants from which $\Uparrow(\mathbf{M}, \mathbf{xc})$ depends on the rules given in Box I.

Rule LF:VM⊥ generates a module implementing the unique part of the variants of a given VM $\mathbf{M}$. To do so, it extracts the unique part $\overline{\mathbf{Defn}}$ of the VM, its optional init block, and the dependencies $\mathbf{D}$ occurring in these parts. The rule returns the set of dependencies $\mathbf{D}$ (which identifies Vf-ABS modules that need to be generated) and a new Vf-ABS module named $\Uparrow(\mathbf{M}, \perp)$ that: (i) exports everything; (ii) imports from all Vf-ABS modules identified in $\mathbf{D}$; (iii) contains the unique classes/interfaces of the original VM, where all syntactic dependencies are translated according to $\Uparrow$.

Rule LF:VM⊥ generates a Vf-ABS module implementing the non-unique part of the variant of the VM $\mathbf{M}$ for a product $\pi$. It is similar to the first rule, except for two elements: (i) the optional init block is not considered (it cannot be present); (ii) the extracted (non-unique classes/interfaces) part of the VM is modified by applying the activated deltas as described in Definition 10 before being integrated in the resulting module.

**Example 2 (Local Flattening).** Consider the following VM $\mathbf{M}$, which declares two interfaces, only one of which is unique.

```pascal
module M;
export J;
features F with true;
unique interface I {}
interface J extends I {}
delta D; modifies interface J { adds Unit m(); }
delta D when F;
```

Rule LF:VM⊥ generates the module implementing the unique part of the VM with added import and export clauses.

```pascal
module M;
export *;
import * from Mf;
interface I {}
```

Rule LF:VM⊥ for $\pi = \{\mathbf{F}\}$ generates the following module:

```pascal
module Mf;
export J;
import * from M;
interface J { Unit m(); }
```

<footnote n="10">¹⁰ Since we are considering programs that satisfy the sanity conditions and are in normal form, this set of features is a product.</footnote>
**Definition 8 (Ground Dependency Meaning).** Given a program *Prg*, a VM *M* of *Prg*, a ground dependency *δ* on *M'*. *N* occurring in *M*, and an extended product *xc* of *M*.

$$ \Downarrow (\mathbf{Prg}, \mathbf{M}, \delta, \mathbf{xc}) = \left\{ \begin{array}{ll} (\mathbf{M}', \perp) & \text{when } \mathbf{M}' \in \text{UNIQUE}(\mathbf{Prg}, \mathbf{M}') \\ (\mathbf{M}', \mathbf{xc}) & \text{when } \mathbf{M}' = \mathbf{M}, \delta \text{ is with-free} \\ & \text{and } \mathbf{M}' \cdot \mathbf{N} \notin \text{UNIQUE}(\mathbf{Prg}, \mathbf{M}) \\ (\mathbf{M}', \pi) & \text{when } \delta \text{ is } \mathbf{M}' \cdot \mathbf{N} \text{ with } \pi \\ & \text{and } \mathbf{M}' \cdot \mathbf{N} \notin \text{UNIQUE}(\mathbf{Prg}, \mathbf{M}') \end{array} \right. $$

If all dependencies in the core part *MdLC* of *M* are ground define $\Downarrow(\mathbf{Prg}, \mathbf{M}, \mathbf{MdLC}, \mathbf{xc}) = \{\Downarrow(\mathbf{Prg}, \mathbf{M}, \delta, \mathbf{xc}) | \delta \text{ is a dependency in } \mathbf{MdLC}\}$.

Flattening a program *Prg* may require to generate more than one variant for each of its VMs. The flattening process generates new names for the generated Vf-ABS modules implementing the required variants and translates the dependencies occurring in *Prg* into uses of (i.e., with-free dependencies on) the generated names. Next we define notation for the names of the generated modules and the translation of with- and with-free-dependencies into the corresponding dependencies among non-variable ABS modules.

**Definition 9 (New Module Name, Dependency Translation).** Given a program *Prg*, a VM *M* of *Prg*, let *xc* be either $\perp$ or a product $\pi$ of *M*. We denote with $\Uparrow(\mathbf{M}, \mathbf{xc})$ the name of the module that implements the unique part of the variants of *M* when $\mathbf{xc} = \perp$, otherwise, the name of the module that implements the non-unique part of the variant of *M* for product *xc*. Moreover, for any ground dependency $\delta$ on $\mathbf{M'}.\mathbf{N}$:

$$ \Uparrow(\mathbf{Prg}, \mathbf{M}, \delta, \mathbf{xc}) = \left\{ \begin{array}{ll} \Uparrow(\mathbf{M}', \perp).\mathbf{N} & \text{when } \mathbf{M}' \cdot \mathbf{N} \in \text{UNIQUE}(\mathbf{Prg}, \mathbf{M}') \\ \Uparrow(\mathbf{M}', \mathbf{xc}).\mathbf{N} & \text{when } \mathbf{M}' = \mathbf{M}, \delta \text{ is with-free} \\ & \text{and } \mathbf{M}' \cdot \mathbf{N} \notin \text{UNIQUE}(\mathbf{Prg}, \mathbf{M}) \\ \Uparrow(\mathbf{M}', \pi).\mathbf{N} & \text{when } \delta \text{ is } \mathbf{M}' \cdot \mathbf{N} \text{ with } \pi \\ & \text{and } \mathbf{M}' \cdot \mathbf{N} \notin \text{UNIQUE}(\mathbf{Prg}, \mathbf{M}') \end{array} \right. $$

If all dependencies in the core part *MdLC* of *M* are ground define $\Uparrow(\mathbf{Prg}, \mathbf{M}, \mathbf{MdLC}, \mathbf{xc})$ as the VM core *MdLC* obtained from *MdLC* by replacing each dependency $\delta$ occurring in it with $\Uparrow(\mathbf{Prg}, \mathbf{M}, \delta, \mathbf{xc})$.

## 7.2. Flattening

The following definition formalizes the application of an ordered delta sequence $\mathbf{Dlt}$ (the deltas activated by a product $\pi$ of a VM *M*) to a sequence $\mathbf{Defn}$ of interface/class definitions (the non-unique class/interface definitions in the module core part *MdLC* of *M*). This is the standard semantics of delta application (Schaefer et al., 2010).

**Definition 10 (Delta Application).** Given a sequence of declarations $\mathbf{Defn}$ and an ordered sequence of deltas $\mathbf{Dlt}$, we denote with the relation $(\mathbf{Dlt}, \mathbf{Defn}) \to^* \mathbf{Defn}'$ that $\mathbf{Defn}'$ is the outcome of the procedure described in Appendix A.

According to the definition above, application of a delta succeeds under the following conditions: (i) each class/interface to be removed or modified is present in the module in focus; (ii) each attribute to be removed or modified is present (with identical header) in the class/interface in focus; (iii) each class, method or field to be added is not present already; (iv) when adding/removing interface references from $\overline{\mathbf{IR}}$ in class C implements $\overline{\mathbf{IR}}$ ... and interface I extends $\overline{\mathbf{IR}}$, ..., the sequence $\overline{\mathbf{IR}}$ is treated as a set: first interface references are added to $\overline{\mathbf{IR}}$ (this operation succeeds even if some of the added interface references are already present in $\overline{\mathbf{IR}}$) yielding $\overline{\mathbf{IR}}'$—only then interface references are removed (this operation succeeds even when some of the removed interface references are not present in $\overline{\mathbf{IR}}'$).

Let $\pi$ be a product of *M*. We define a mapping $\sigma = \text{genP}(\mathbf{Prg}, \mathbf{M}, \pi)$ from open product names defined by *M*

to their corresponding set of features. Given a sequence of interface/class definitions $\mathbf{Defn}$ and such a mapping $\sigma$, we denote with $\sigma(\mathbf{Defn})$ the definitions obtained from $\mathbf{Defn}$ by replacing each occurrence of a open product name with its associated set of features.<fnref n="10" />

We are ready to define the rules that flatten a VM to produce either a Vf-ABS module containing its unique class/interfaces, or a Vf-ABS module containing the non-unique class/interfaces generated for a given product:

**Definition 11 (Local Flattening of VM Relative to an Extended Product).** Let *M* be the name of a VM of *Prg*, *xc* an extended product of *M*. The local flattening of *M* relative to *xc* is the Vf-ABS module *Md1* such that the judgment $M \mathbf{\xrightarrow{\mathbf{Prg.xc}}} D, \mathbf{Md1}$ (defined by rules LF:VM⊥ and LF:VM⊥ below) holds, where: (i) *Md1* is the code of a Vf-ABS module named $\Uparrow(\mathbf{M}, \mathbf{xc})$, which, for the case $\mathbf{xc} = \perp$ implements the unique part of the variants of *M*, for the case $\mathbf{xc} = \pi$ implements the non-unique part of the variant of *M* for product $\pi$; (ii) *D* is the set of pairs (module, extended product) identifying the set of variants from which $\Uparrow(\mathbf{M}, \mathbf{xc})$ depends on the rules given in Box I.

Rule LF:VM⊥ generates a module implementing the unique part of the variants of a given VM *M*. To do so, it extracts the unique part $\mathbf{Defn}$ of the VM, its optional init block, and the dependencies *D* occurring in these parts. The rule returns the set of dependencies *D* (which identifies Vf-ABS modules that need to be generated) and a new Vf-ABS module named $\Uparrow(\mathbf{M}, \perp)$ that: (i) exports everything; (ii) imports from all Vf-ABS modules identified in *D*; (iii) contains the unique classes/interfaces of the original VM, where all syntactic dependencies are translated according to $\Uparrow$.

Rule LF:VM⊥ generates a Vf-ABS module implementing the non-unique part of the variant of the VM *M* for a product $\pi$. It is similar to the first rule, except for two elements: (i) the optional init block is not considered (it cannot be present); (ii) the extracted (non-unique classes/interfaces) part of the VM is modified by applying the activated deltas as described in Definition 10 before being integrated in the resulting module.

**Example 2 (Local Flattening).** Consider the following VM *M*, which declares two interfaces, only one of which is unique.

```pascal
module M;
export J;
features F with true;
unique interface I {}
interface J extends I {}
delta D; modifies interface J { adds Unit m(); }
delta D when F;
```

Rule LF:VM⊥ generates the module implementing the unique part of the VM with added import and export clauses.

```pascal
module M;
export *;
import * from Mf;
interface I {}
```

Rule LF:VM⊥ for $\pi = \{F\}$ generates the following module:

```pascal
module Mf;
export J;
import * from M;
interface J { Unit m(); }
```

<footnote n="10">¹⁰ Since we are considering programs that satisfy the sanity conditions and are in normal form, this set of features is a product.</footnote>
LF:VM⊥

$mdlUnique(Prg, M) = \underline{Defn} \quad \underline{Defn} \; \mathrm{mdlInit}(Prg, M) = \mathrm{MdLC}$
$\Downarrow(Prg, M, \mathrm{MdLC}, \perp) = D = \{(M_i, x_{c_i}) | i \in I\}$

$M \xrightarrow{\text{Prg.}\perp} D, \text{module } \Uparrow(M, \perp); \text{ export *; import * from } \Uparrow(M_i, x_{c_i}); \Uparrow(Prg, M, \text{MdLC}, \perp)$

LF:VM⊥

$mdlNotUnique(Prg, M) = \underline{Defn} \quad \underline{Defn} \; \mathrm{mdlDelta}(Prg, M, \pi) = \underline{Dlt}$
$(\underline{Dlt}, \underline{Defn}) \to^* \underline{Defn}' \quad \sigma = \mathrm{genP}(Prg, M, \pi)$
$\sigma(\underline{Defn}') = \underline{Defn''} \quad \Downarrow(Prg, M, \underline{Defn''}, \perp) = D = \{(M_i, x_{c_i}) | i \in I\}$

$M \xrightarrow{\text{Prg.}\pi} D, \text{module } \Uparrow(M, \pi); \text{ export *; import * from } \Uparrow(M_i, x_{c_i}); \Uparrow(Prg, M, \underline{Defn''}, \pi)$

Box I.

CF:VM1

$\underline{xc}$ is an extended product of $M$ \quad $M \xrightarrow{\text{Prg.xc}} D, \text{MdL}$ \quad $A = ((M, xc))$
$\varepsilon, \emptyset, ((M, xc)) \xrightarrow{\text{Prg}} \text{MdL}, A, (D \setminus A)$

CF:VM2

$\underline{\text{Prg}'} \neq \varepsilon \quad (M, xc) \in D_1 \quad M \xrightarrow{\text{Prg.xc}} D, \text{MdL}$
$A_2 = A_1 \cup \{(M, xc)\}$
$D_2 = (D_1 \cup D) \setminus A_2$
$\underline{\text{Prg}'} \in \underline{\text{Prg}} \quad \underline{\text{Prg}} \xrightarrow{\text{Prg}} \text{MdL}, A_2, D_2$

Box II.

Next we define rewrite rules that, given a VM $M$ of $\text{Prg}$ and an extended product $xc$ of $M$, generate the variant of $M$ identified by $xc$ as well as all variants of the VMs in $\text{Prg}$ needed to resolve the dependencies of all the variants that arise during the rewriting.

**Definition 12 (Complete Flattening of VM Relative to an Extended Product).** Let $\varepsilon$ denote the empty program, representing the initial partial result of a complete flattening of a VM $M$ of an ABS-VM program $\text{Prg}$ relative to an extended product $xc$.

The two rules below define a judgment of the form
$\text{Prg}' \cdot A_1 \cdot D_1 \xrightarrow{\text{Prg}} \text{Prg}'' \cdot A_2 \cdot D_2$, where: $\text{Prg}'$ (either $\varepsilon$ or a Vf-ABS program) is a partial result of complete flattening, the set $A_1$ identifies the already generated Vf-ABS modules, the set $D_1$ identifies the Vf-ABS modules that must be generated to resolve the dependencies in $\text{Prg}'$, the Vf-ABS program $\text{Prg}''$ is obtained by adding to $\text{Prg}'$ the code of one of the Vf-ABS modules identified by $D_1$, and the sets $A_2, D_2$ are obtained by suitably updating $A_1, D_1$, respectively (see rules given in Box II).

Let $\text{Prg}^* \xrightarrow{*} \text{Prg}$ be the transitive closure of $\text{Prg}^* \xrightarrow{*} \text{Prg}$. The complete flattening of VM $M$ of $\text{Prg}$ relative to its extended product $xc$ is the Vf-ABS program $\text{Prg}'$ such that $\varepsilon, \emptyset, ((M, xc)) \xrightarrow{*} \text{Prg}'$, $A, \emptyset$ holds.

The sets $A, D, A_1, D_1, A_2$ and $D_2$ in the two rules above refer to dependencies in the original program $\text{Prg}$. Rule CF:VM1 starts with the empty ABS program, the empty set of resolved dependencies, and the singleton set $((M, xc))$ of dependencies to be resolved. It adds the ABS module implementing the extended product $xc$ of $M$ and updates the dependency sets. Rule CF:VM2 extends $\text{Prg}'$ by adding the ABS module required by one of the dangling dependencies in $D_1$, and replaces the dependency sets $A_1, D_1$ by their updated versions $A_2, D_2$, respectively.

Finally, we can formalize flattening of a whole ABS-VM program.

**Definition 13 (Flattening of ABS-VM Program).** The flattening of an ABS-VM program $\text{Prg}$ is the complete flattening of its main module relative to $\perp$: the Vf-ABS program $\text{Prg}'$ such that $\varepsilon, \emptyset, \{\text{mdlInit}(\text{Prg}), \perp\} \xrightarrow{*} \text{Prg}'$, $A, \emptyset$ holds.

module $M_0$;
import * from $M_F$;
init { $M_F$.J j = null; }

module M;
export *;
import * from $M_F$;
interface I {}

module $M_F$;
export J;
import * from M;
interface J { Unit m(); }

<caption>Fig. 8. Complete flattening of VM $M_0$ from Example 2.</caption>

**Example 3 (Complete Flattening).** Let us continue with Example 2. Consider the program $\text{Prg}$ that consists of $M$ and the module $M_0$ given below

module $M_0$;
import * from $M$;
init { J with {$F$} j = null; }

The complete flattening of $M_0$ is given in Fig. 8.

8. Type-safety for ABS-VM programs

In this section, as in Section 7, we consider ABS-VM programs in normal form (Definition 5). We first define well-typed Vf-ABS programs (Section 8.1), then type-safe ABS-VM programs (Section 8.2).

8.1. Well-typed Vf-ABS programs

We assume Vf-ABS programs to be sane (Section 5.2). First we set up terminology for what we call the basic types related to Vf-ABS programs.

**Definition 14 (Basic Type).** A basic type $\text{BT}$ of a Vf-ABS program is one of the following:
LF:VM⊥

mdlUnique(Prg, M) = Defn Defn mdllnit(Prg, M) = MdlC
  ⇐(Prg, M, MdlC, ⊥) = D = {(Mᵢ, xcᵢ) | i ∈ I}

$M \xrightarrow{\text{Prg.} \perp} D, \text{module } \Uparrow(M, \perp); \text{ export *; import * from } \Uparrow(M_i, xc_i); \Uparrow(\text{Prg}, M, \text{MdlC}, \perp)$

LF:VM⊥

mdlNotUnique(Prg, M) = Defn
  (Dlt, Defn) \to * Defn' 
  σ = genP(Prg, M, π)

$\sigma(\text{Defn}') = \text{Defn''} \Uparrow(\text{Prg}, M, \text{Defn'', \perp}) = D = \{(M_i, xc_i) | i \in I\}$

$M \xrightarrow{\text{Prg.} \pi} D, \text{module } \Uparrow(M, \pi); \text{ export *; import * from } \Uparrow(M_i, xc_i); \Uparrow(\text{Prg}, M, \text{Defn'', } \pi)$

Box I.

CF:VM₁

$xc$ is an extended product of $M$ $M \xrightarrow{\text{Prg.xc}} D, \text{Mdl}$ $A = ((M, xc))$
$\varepsilon, \emptyset, ((M, xc)) \xrightarrow{\text{Prg}} \text{Mdl}, A, (D \setminus A)$

CF:VM₂

$\frac{\text{Prg}' \neq \varepsilon (M, xc) \in D_1}{\text{Prg}' \neq \varepsilon (M, xc) \in D_1} M \xrightarrow{\text{Prg.xc}} D, \text{Mdl} \quad A_2 = A_1 \cup \{(M, xc)\} \quad D_2 = (D_1 \cup D) \setminus A_2$
$\frac{\text{Prg}' \neq A_1, D_1}{\text{Prg}' \neq A_1, D_1} \xrightarrow{\text{Prg}} \text{Prg}' \quad \text{Mdl}, A_2, D_2$

Box II.

Next we define rewrite rules that, given a VM $M$ of $\text{Prg}$ and an extended product $xc$ of $M$, generate the variant of $M$ identified by $xc$ as well as all variants of the VMs in $\text{Prg}$ needed to resolve the dependencies of all the variants that arise during the rewriting.

**Definition 12 (Complete Flattening of VM Relative to an Extended Product).** Let $\varepsilon$ denote the empty program, representing the initial partial result of a complete flattening of a VM $M$ of an ABS-VM program $\text{Prg}$ relative to an extended product $xc$.

The two rules below define a judgment of the form
$\text{Prg}'_{A_1, D_1} \xrightarrow{\text{Prg}} \text{Prg}''_{A_2, D_2}$, where: $\text{Prg}'$ (either $\varepsilon$ or a Vf-ABS program) is a partial result of complete flattening, the set $A_1$ identifies the already generated Vf-ABS modules, the set $D_1$ identifies the Vf-ABS modules that must be generated to resolve the dependencies in $\text{Prg}'$, the Vf-ABS program $\text{Prg}''$ is obtained by adding to $\text{Prg}'$ the code of one of the Vf-ABS modules identified by $D_1$, and the sets $A_2, D_2$ are obtained by suitably updating $A_1, D_1$, respectively (see rules given in Box II).

Let $\text{Prg}' \xrightarrow{*} \text{Prg}$ be the transitive closure of $\text{Prg}' \xrightarrow{\text{Prg}} \text{Prg}$. The complete flattening of VM $M$ of $\text{Prg}$ relative to its extended product $xc$ is the Vf-ABS program $\text{Prg}'$ such that $\varepsilon, \emptyset, ((M, xc)) \xrightarrow{\text{Prg}} \varepsilon, \emptyset$ holds.

The sets $A, D, A_1, D_1, A_2$ and $D_2$ in the two rules above refer to dependencies in the original program $\text{Prg}$. Rule CF:VM₁ starts with the empty ABS program, the empty set of resolved dependencies, and the singleton set $\{(M, xc)\}$ of dependencies to be resolved. It adds the ABS module implementing the extended product $xc$ of $M$ and updates the dependency sets. Rule CF:VM₂ extends $\text{Prg}'$ by adding the ABS module required by one of the dangling dependencies in $D_1$, and replaces the dependency sets $A_1, D_1$ by their updated versions $A_2, D_2$, respectively.

Finally, we can formalize flattening of a whole ABS-VM program.

**Definition 13 (Flattening of ABS-VM Program).** The flattening of an ABS-VM program $\text{Prg}$ is the complete flattening of its main module relative to $\perp$: the Vf-ABS program $\text{Prg}'$ such that $\varepsilon, \emptyset, \{\text{mdlInit}(\text{Prg}), \perp\} \xrightarrow{\text{Prg}} \varepsilon, \emptyset$ holds.

module $M_0$;
import * from $M_F$;
init { $M_F$.J j = null; }

module M;
export *;
import * from $M_F$;
interface I {}

module $M_F$;
export J;
import * from M;
interface J { Unit m(); }

<caption>Fig. 8. Complete flattening of VM $M_0$ from Example 2.</caption>

**Example 3 (Complete Flattening).** Let us continue with Example 2. Consider the program $\text{Prg}$ that consists of $M$ and the module $M_0$ given below

module $M_0$;
import * from M;
init { J with {F} j = null; }

The complete flattening of $M_0$ is given in Fig. 8.

## 8. Type-safety for ABS-VM programs

In this section, as in Section 7, we consider ABS-VM programs in normal form (Definition 5). We first define well-typed Vf-ABS programs (Section 8.1), then type-safe ABS-VM programs (Section 8.2).

### 8.1. Well-typed Vf-ABS programs

We assume Vf-ABS programs to be sane (Section 5.2). First we set up terminology for what we call the basic types related to Vf-ABS programs.

**Definition 14 (Basic Type).** A basic type $\text{BT}$ of a Vf-ABS program is one of the following:
```java
module M;
export I, J, C;
interface I { Int getK(); }
interface J { Unit inc(); }
class C implements I, J {
    Int k = 0;
    Int getK() { return k; }
    Unit inc() { k = k+1; }
}
```

$$
\begin{align*}
\text{PrgS}(M)(\text{export}) &= \text{M.I, M.J, M.C} & \text{PrgS}(M)(\text{import}) &= \emptyset \\
\text{PrgS}(I)(\text{super}) &= \emptyset & \text{PrgS}(J)(\text{super}) &= \emptyset & \text{PrgS}(C)(\text{super}) &= \{\text{M.I, M.J}\} \\
\text{PrgS}(I)(\text{getK}) &= () \rightarrow \text{Int} & \text{PrgS}(J)(\text{inc}) &= () \rightarrow \text{Unit} \\
\text{PrgS}(C)(k) &= \text{Int} & \text{PrgS}(C)(\text{getK}) &= () \rightarrow \text{Int} & \text{PrgS}(C)(\text{inc}) &= () \rightarrow \text{Unit}
\end{align*}
$$

<caption>Fig. 9. A program and its signature.</caption>

1. A variable basic type `VBT`: a primitive type `PT` or a qualified interface name of the shape `M.I` (so `VBT` is a strict subset of variable types `VT`, see Fig. 6).

2. An expression basic type `EBT`: a variable basic type or a qualified class name of the form `M.C`.

3. A method basic type `MBT` of the form `( VBT ) -> VBT`, where `VBT = VBT₁, ..., VBTn` (`n` ≥ 0) are the types of the formal parameters and `VBT` is the return type.

4. A reference basic type `RBT`: a qualified class/interface name of the form `M.N`.

The next definition provides signatures to represent the structure of classes, interfaces, modules, and programs without method implementations. The subsequent definitions introduce the subtyping relation induced by a program signature and the notion of a well-formed program signature, respectively.

**Definition 15 (Class/interface/module/program signature).**

1. A class signature consists of the class name, a mapping from the keyword `super` to the set of qualified names of the implemented interfaces, a mapping from each field name to its variable basic type, and a mapping from each method name to its method basic type. Class signatures are ranged over by `CS`. We write `sig(CD)` to denote the signature of class declaration `CD`.

2. An interface signature consists of the interface name, a mapping from the keyword `super` to the set of qualified names of the extended interfaces and a mapping from each method name to its method basic type. Interface signatures are ranged over by `IS`. We write `sig(ID)` to denote the signature of the interface declaration `ID`.

3. A module signature consists of the module name `M`, a mapping from the keyword `export` to its trade clause, a mapping from the keyword `import` to the set of all imported pairs `(tCᵢ, Mᵢ)` with `n` ≥ 0 and `Mᵢ` ≠ `M` (`1` ≤ `i` ≤ `n`), and a mapping from each class/interface name to its class/interface signature. Module signatures are ranged over by `Mdls`. We write `sig(Mdl)` to denote the signature of the module `Mdl`.

4. A program signature maps each module name to its module signature. Program signatures are ranged over by `PrgS`. We write `sig(Prg)` to denote the signature of the program `Prg`.

A program signature `sig(Prg)` can be computed by inspection of `Prg`, specifically, `ID` and `sig(ID)` are isomorphic.

**Example 4 (Program Signature).** Fig. 9 shows a program `Prg` and its signature `sig(Prg) = PrgS`.

**Definition 16 (Subtyping Relation Induced by Program Signature).** The subtyping relation induced by program signature `PrgS`, denoted by `<:PrgS`, is the transitive closure of the union of: (i) the identity relation on primitive types and qualified class/interface names defined in `Prg`, (ii) the implements-relation (defined by class `implements` clauses), (iii) the immediate extends-relation (defined by the interface `extends` clauses). When `PrgS` is clear from the context we write simply `<:`.

**Definition 17 (Well-Formed Program Signature).** A program signature `PrgS` is well-formed iff:

1. for every module name `M` appearing anywhere in `PrgS` we have `M` ∈ `dom(PrgS)`;

2. for every qualified class/interface name `M.N` appearing anywhere in `PrgS` we have `N` ∈ `dom(PrgS(M))`;

3. every traded name appearing in `PrgS(M)(export)` occurs in `dom(PrgS(M))`;

4. if `PrgS(M)(import)` contains a pair `(tC, M')` then `M'` ≠ `M` and all traded names in `tC` occur in `PrgS(M')(export)`;

5. the transitive closure of the immediate extends-relation is acyclic;

6. for all modules `M, M'` ∈ `dom(PrgS)`, classes/interfaces `N, N'` ∈ `dom(PrgS(M))`, if `M.N` <= `M'` and `M.N` <= `N'` and `N'` ∈ `dom(PrgS(M))` and `N'` ∩ `dom(PrgS(M))` = ∅, then for each field `a` ∈ `dom(PrgS(M)(N₁))` ∩ `dom(PrgS(M)(N₂))`, it holds that `PrgS(M₁)(N₁)(a) = PrgS(M₂)(N₂)(a)`.

The signature in Example 4 is well-formed. The typing rules for Vf-ABS are straightforward and follow a standard pattern for simple OO programs with modules.

**Definition 18 (Well-Typed Vf-ABS Module and Program).**

1. Let `PrgS` be the well-formed signature of a Vf-ABS program. A module `Mdl` such that `PrgS(name(Mdl)) = sig(Mdl)` is well-typed iff the judgment `PrgS ⊢ Mdl` can be derived by the rules given in Appendix B.

2. A Vf-ABS program `Prg` is well-typed iff it is sane and the judgment `Prg ⊢ Prg` can be derived by the following rule:

$$
\begin{array}{c}
T:Prg \\
\qquad \text{sig(Prg) is well-formed} \qquad \text{sig(Prg)} \vdash \text{Mdl}, \text{ for all } \text{Mdl} \in \text{Prg} \\
\qquad \qquad \vdash \text{Prg}
\end{array}
$$

## 8.2. Type-safety

We begin with an auxiliary definition based on local flattening (Definition 11).
```java
module M;
export I, J, C;
interface I { Int getK(); }
interface J { Unit inc(); }
class C implements I, J {
    Int k = 0;
    Int getK() { return k; }
    Unit inc() { k = k+1; }
}
```

$$
\begin{align*}
\text{PrgS}(M)(\text{export}) &= \text{M.I, M.J, M.C} & \text{PrgS}(M)(\text{import}) &= \emptyset \\
\text{PrgS}(I)(\text{super}) &= \emptyset & \text{PrgS}(J)(\text{super}) &= \emptyset & \text{PrgS}(C)(\text{super}) &= \{\text{M.I, M.J}\} \\
\text{PrgS}(I)(\text{getK}) &= () \rightarrow \text{Int} & \text{PrgS}(J)(\text{inc}) &= () \rightarrow \text{Unit} \\
\text{PrgS}(C)(k) &= \text{Int} & \text{PrgS}(C)(\text{getK}) &= () \rightarrow \text{Int} & \text{PrgS}(C)(\text{inc}) &= () \rightarrow \text{Unit}
\end{align*}
$$

<caption>Fig. 9. A program and its signature.</caption>

1. A variable basic type `VBT`: a primitive type `PT` or a qualified interface name of the shape `M.I` (so `VBT` is a strict subset of variable types `VT`, see Fig. 6).

2. An expression basic type `EBT`: a variable basic type or a qualified class name of the form `M.C`.

3. A method basic type `MBT` of the form `( VBT ) → VBT`, where `VBT = VBT₁,...,VBTn` (`n` ≥ 0) are the types of the formal parameters and `VBT` is the return type.

4. A reference basic type `RBT`: a qualified class/interface name of the form `M.N`.

The next definition provides signatures to represent the structure of classes, interfaces, modules, and programs without method implementations. The subsequent definitions introduce the subtyping relation induced by a program signature and the notion of a well-formed program signature, respectively.

**Definition 15 (Class/interface/module/program signature).**

1. A class signature consists of the class name, a mapping from the keyword `super` to the set of qualified names of the implemented interfaces, a mapping from each field name to its variable basic type, and a mapping from each method name to its method basic type. Class signatures are ranged over by `CS`. We write `sig(CD)` to denote the signature of class declaration `CD`.

2. An interface signature consists of the interface name, a mapping from the keyword `super` to the set of qualified names of the extended interfaces and a mapping from each method name to its method basic type. Interface signatures are ranged over by `IS`. We write `sig(ID)` to denote the signature of the interface declaration `ID`.

3. A module signature consists of the module name `M`, a mapping from the keyword `export` to its trade clause, a mapping from the keyword `import` to the set of all imported pairs `(tCᵢ, Mᵢ)` with `n` ≥ 0 and `Mᵢ` ≠ `M` (`1` ≤ `i` ≤ `n`), and a mapping from each class/interface name to its class/interface signature. Module signatures are ranged over by `Mdls`. We write `sig(Mdl)` to denote the signature of the module `Mdl`.

4. A program signature maps each module name to its module signature. Program signatures are ranged over by `PrgS`. We write `sig(Prg)` to denote the signature of the program `Prg`.

A program signature `sig(Prg)` can be computed by inspection of `Prg`, specifically, `ID` and `sig(ID)` are isomorphic.

**Example 4 (Program Signature).** Fig. 9 shows a program `Prg` and its signature `sig(Prg) = PrgS`.

**Definition 16 (Subtyping Relation Induced by Program Signature).** The subtyping relation induced by program signature `PrgS`, denoted by `<:PrgS`, is the transitive closure of the union of: (i) the identity relation on primitive types and qualified class/interface names defined in `Prg`, (ii) the implements-relation (defined by class `implements` clauses), (iii) the immediate extends-relation (defined by the interface `extends` clauses). When `PrgS` is clear from the context we write simply `<:`.

**Definition 17 (Well-Formed Program Signature).** A program signature `PrgS` is well-formed iff:

1. for every module name `M` appearing anywhere in `PrgS` we have `M` ∈ `dom(PrgS)`;

2. for every qualified class/interface name `M.N` appearing anywhere in `PrgS` we have `N` ∈ `dom(PrgS(M))`;

3. every traded name appearing in `PrgS(M)(export)` occurs in `dom(PrgS(M))`;

4. if `PrgS(M)(import)` contains a pair `(tC, M')` then `M'` ≠ `M` and all traded names in `tC` occur in `PrgS(M')(export)`;

5. the transitive closure of the immediate extends-relation is acyclic;

6. for all modules `M, M'` ∈ `dom(PrgS)`, classes/interfaces `N, N'` ∈ `dom(PrgS(M))`, if `M.N` <= `M'` and `M.N` <= `N'` and `N'` ∈ `dom(PrgS(M))` and `N'` ∩ `dom(PrgS(M))` = ∅, then for each field `a` ∈ `dom(PrgS(M)(N₁))` ∩ `dom(PrgS(M)(N₂))`, it holds that `PrgS(M₁)(N₁)(a)=PrgS(M₂)(N₂)(a)`.

The signature in Example 4 is well-formed. The typing rules for Vf-ABS are straightforward and follow a standard pattern for simple OO programs with modules.

**Definition 18 (Well-Typed Vf-ABS Module and Program).**

1. Let `PrgS` be the well-formed signature of a Vf-ABS program. A module `Mdl` such that `PrgS(name(Mdl)) = sig(Mdl)` is well-typed iff the judgment `PrgS ⊢ Mdl` can be derived by the rules given in Appendix B.

2. A Vf-ABS program `Prg` is well-typed iff it is sane and the judgment `Prg ⊢ Prg` can be derived by the following rule:

$$
\begin{array}{c}
\text{T:Prg} \\
\text{sig(Prg) is well-formed} \\
\vdash \text{Mdl, for all Mdl} \in \text{Prg} \\
\vdash \text{Prg}
\end{array}
$$

## 8.2. Type-safety

We begin with an auxiliary definition based on local flattening (Definition 11).
**Definition 19 (Overall Flattening of VM and Program).** Let $Prg$ be an ABS-VM program and $M$ be a VM of $Prg$.

1. The overall flattening of $M$ is the Vf-ABS program consisting of all Vf-ABS modules $Mdl$, where $Mdl$ is the local flattening of $M$ relative to one of its extended products.

2. The overall flattening of $Prg$ is the Vf-ABS program consisting of all Vf-ABS modules $Mdl$ occurring in the overall flattening of some VM of $Prg$.

Because of sanity conditions 1, 8, and 9 (Section 5.2) we can observe that if the overall flattening of $Prg$ succeeds then for all its VMs $Mdl$, the complete flattening of $Mdl$ relative to each of its extended products succeeds (and its modules are a subset of the modules of the overall flattening of $Prg$). In contrast, if the flattening of $Prg$ succeeds this does not imply that the overall flattening of $Prg$ succeeds (the local flattening of some VM relative to one of its products not required by the main module may fail).

We can now define type-safe ABS-VM programs in terms of well-typed Vf-ABS programs (Definition 18).

**Definition 20 (Type-Safe ABS-VM Program).** The ABS-VM program $Prg$ is type-safe iff its overall flattening (i) succeeds and (ii) produces a well-typed Vf-ABS program.

We observe that when $Prg$ is type-safe, for all its VMs $Mdl$, the complete flattening of $Mdl$ relative to each of its extended products generates a well-typed Vf-ABS program. Moreover, when a type-safe ABS-VM Program $Prg_1$ is modified by only changing its main module, then type-safety of the modified program $Prg_2$ can be checked simply by typing the local flattening $Mdl'$ relative to $\perp$ (of the modified main module) in the context of the program signature of the flattening $Prg'_2$ of $Prg_2$. This corresponds to proving the judgment $\mathrm{sig}(Prg'_2) \vdash Mdl'$ (Definition 18). Likewise, adding a product $\pi$ to a VM $Mdl_1$ of a type-safe program $Prg$, type-safety of the modified program $Prg_2$ can be checked simply by typing the local flattening $Mdl'_2$ of the modified VM $Mdl_2$ relative to $\pi$ in the context of the program signature of the modified flattening $Prg'_2$ of $Mdl_2$ relative to $\pi$. This corresponds to proving the judgment $\mathrm{sig}(Prg'_2) \vdash Mdl'_2$ (Definition 18).

Checking type-safety of a program $Prg$ by generating its overall flattening is generally unfeasible due to the number of products of each VM that may be exponential in the number of features. In the next section we provide means for partially checking type-safety in a feasible manner.

## 9. Family-based checking for ABS-VM programs

ABS-VM program sanity-conditions (Section 5.2), PEV-compliance (Definition 3), inference of the maximal set of unique annotations (Section 6.2), and adherence to normal form (Definition 5) are checkable in a family-based way. We present three family-based analyses for ABS-VM programs in normal form (see Definition 5):

* Type uniformity (Section 9.1) checks whether type declarations are uniform across the different variants of each VM.

* Pre-typing (Section 9.2) checks whether the module core part and the deltas are consistent with the uniform typing information.

* Applicability consistency (Section 9.3) checks whether overall flattening succeeds.

Type uniformity helps developing and maintaining ABS-VM programs, as in any part of a program all occurrences of a given field/method always have the same type (Damiani and Lienhardt, 2016).

Pre-typing assumes type-uniformity. Like type uniformity, it does not use any knowledge about valid feature combinations (it does not use module headers). So it does not guarantee that the overall flattening of a program is well-typed (some class/interface/method/field declared in some VM may not be present in its local flattening relative to one of its products). However, pre-typing guarantees that if each module in the overall flattening has its dependencies fulfilled (i.e., each used module/class/interface/attribute is present and, for each required subtyping relation, suitable *enriched* *implementations* clauses that define it are present), then the overall flattening is well-typed. Therefore, to ensure that a pre-typed ABS-VM program is type-safe (Definition 20) it is sufficient that: (i) its overall flattening succeeds and (ii) it has all its dependencies satisfied.

Applicability consistency checks condition (i). Therefore, the three family-based analyses presented in this section are able to guarantee type-safety modulo the fact that all the dependencies in the overall flattening are satisfied.<fnref n="11" />

### 9.1. Type uniformity

Intuitively, an ABS-VM program is type uniform when its extends-relation is acyclic and field/method types and subtyping relations are consistent across program declarations: all declarations of the same field/method in the same class/interface must have the same type.

To formalize the notion of type uniformity we introduce three auxiliary definitions that introduce types (a superset of the basic types of Definition 14), a more liberal version of program signatures (Definition 15), and a generalization of the subtype relation described by a program signature (Definition 16).

**Definition 21 (Types and Type Stripping).** A type $T$ is one of:

1. An expression type ET: a variable type VT (i.e., an interface reference or a basic type, see Fig. 6), a qualified class name of the form M.C, or M.C with KE.

2. A method type MT: it has the form $(\overline{VT}) \rightarrow VT$, where $\overline{VT} = VT_1, ..., VT_n$ ($n \ge 0$) are the types of the formal parameters, and VT is the return type.

3. A reference type RT: an interface reference IR, a qualified class name of the form M.C, or M.C with KE.

The stripping of a type $T$, denoted by strip($T$), is the basic type (Definition 14) obtained from $T$ by dropping the with-clauses occurring it.

**Definition 22 (Family class/interface/module/program signature).**

1. A family class signature, ranged over by FCS, aggregates the information of all signatures of a class in all variants.

* It contains the class name.

* It associates the keyword super with the set $R$ of the interface references that may be supertypes of the class. Let $M$ be the VM of the class. Then the set $R$ contains all interface references

- that are listed in the *enriched* *implementations*-clause of any declaration of the class in the core part of $M$ or in a delta of $M$,

- that are added to the *enriched* *implementations*-clause of the class by a *modifies*-operation on the class in a delta of $M$.

<footnote n="11">¹¹ We are working on a family-based analysis for performing this latter check as well (Section 12).</footnote>
**Definition 19 (Overall Flattening of VM and Program).** Let $Prg$ be an ABS-VM program and $M$ be a VM of $Prg$.

1. The overall flattening of $M$ is the Vf-ABS program consisting of all Vf-ABS modules $Mdl$, where $Mdl$ is the local flattening of $M$ relative to one of its extended products.

2. The overall flattening of $Prg$ is the Vf-ABS program consisting of all Vf-ABS modules $Mdl$ occurring in the overall flattening of some VM of $Prg$.

Because of sanity conditions 1, 8, and 9 (Section 5.2) we can observe that if the overall flattening of $Prg$ succeeds then for all its VMs $Mdl$, the complete flattening of $Mdl$ relative to each of its extended products succeeds (and its modules are a subset of the modules of the overall flattening of $Prg$). In contrast, if the flattening of $Prg$ succeeds this does not imply that the overall flattening of $Prg$ succeeds (the local flattening of some VM relative to one of its products not required by the main module may fail).

We can now define type-safe ABS-VM programs in terms of well-typed Vf-ABS programs (Definition 18).

**Definition 20 (Type-Safe ABS-VM Program).** The ABS-VM program $Prg$ is type-safe iff its overall flattening (i) succeeds and (ii) produces a well-typed Vf-ABS program.

We observe that when $Prg$ is type-safe, for all its VMs $Mdl$, the complete flattening of $Mdl$ relative to each of its extended products generates a well-typed Vf-ABS program. Moreover, when a type-safe ABS-VM Program $Prg_1$ is modified by only changing its main module, then type-safety of the modified program $Prg_2$ can be checked simply by typing the local flattening $Mdl'$ relative to $\perp$ (of the modified main module) in the context of the program signature of the flattening $Prg'_2$ of $Prg_2$. This corresponds to proving the judgment $\mathrm{sig}(Prg'_2) \vdash Mdl'$ (Definition 18). Likewise, adding a product $\pi$ to a VM $Mdl_1$ of a type-safe program $Prg$, type-safety of the modified program $Prg_2$ can be checked simply by typing the local flattening $Mdl'_2$ of the modified VM $Mdl_2$ relative to $\pi$ in the context of the program signature of the modified flattening $Prg'_2$ of $Mdl_2$ relative to $\pi$. This corresponds to proving the judgment $\mathrm{sig}(Prg'_2) \vdash Mdl'_2$ (Definition 18).

Checking type-safety of a program $Prg$ by generating its overall flattening is generally unfeasible due to the number of products of each VM that may be exponential in the number of features. In the next section we provide means for partially checking type-safety in a feasible manner.

## 9. Family-based checking for ABS-VM programs

ABS-VM program sanity-conditions (Section 5.2), PEV-compliance (Definition 3), inference of the maximal set of unique annotations (Section 6.2), and adherence to normal form (Definition 5) are checkable in a family-based way. We present three family-based analyses for ABS-VM programs in normal form (see Definition 5):

* Type uniformity (Section 9.1) checks whether type declarations are uniform across the different variants of each VM.

* Pre-typing (Section 9.2) checks whether the module core part and the deltas are consistent with the uniform typing information.

* Applicability consistency (Section 9.3) checks whether overall flattening succeeds.

Type uniformity helps developing and maintaining ABS-VM programs, as in any part of a program all occurrences of a given field/method always have the same type (Damiani and Lienhardt, 2016).

Pre-typing assumes type-uniformity. Like type uniformity, it does not use any knowledge about valid feature combinations (it does not use module headers). So it does not guarantee that the overall flattening of a program is well-typed (some class/interface/method/field declared in some VM may not be present in its local flattening relative to one of its products). However, pre-typing guarantees that if each module in the overall flattening has its dependencies fulfilled (i.e., each used module/class/interface/attribute is present and, for each required subtyping relation, suitable *enriched* *implementations* clauses that define it are present), then the overall flattening is well-typed. Therefore, to ensure that a pre-typed ABS-VM program is type-safe (Definition 20) it is sufficient that: (i) its overall flattening succeeds and (ii) it has all its dependencies satisfied.

Applicability consistency checks condition (i). Therefore, the three family-based analyses presented in this section are able to guarantee type-safety modulo the fact that all the dependencies in the overall flattening are satisfied.<fnref n="11" />

### 9.1. Type uniformity

Intuitively, an ABS-VM program is type uniform when its extends-relation is acyclic and field/method types and subtyping relations are consistent across program declarations: all declarations of the same field/method in the same class/interface must have the same type.

To formalize the notion of type uniformity we introduce three auxiliary definitions that introduce types (a superset of the basic types of Definition 14), a more liberal version of program signatures (Definition 15), and a generalization of the subtype relation described by a program signature (Definition 16).

**Definition 21 (Types and Type Stripping).** A type $T$ is one of:

1. An expression type ET: a variable type VT (i.e., an interface reference or a basic type, see Fig. 6), a qualified class name of the form `M.C`, or `M.C` with `KE`.

2. A method type MT: it has the form $(\overline{VT}) \rightarrow VT$, where $\overline{VT} = VT_1, \dots, VT_n$ ($n \ge 0$) are the types of the formal parameters, and $VT$ is the return type.

3. A reference type RT: an interface reference IR, a qualified class name of the form `M.C`, or `M.C` with `KE`.

The stripping of a type $T$, denoted by `strip(T)`, is the basic type (Definition 14) obtained from $T$ by dropping the `with-clauses` occurring it.

**Definition 22 (Family class/interface/module/program signature).**

1. A family class signature, ranged over by FCS, aggregates the information of all signatures of a class in all variants.

* It contains the class name.

* It associates the keyword `super` with the set $R$ of the interface references that may be supertypes of the class. Let $M$ be the VM of the class. Then the set $R$ contains all interface references

- that are listed in the *enriched* *implementations*-clause of any declaration of the class in the core part of $M$ or in a delta of $M$,

- that are added to the *enriched* *implementations*-clause of the class by a *modifies*-operation on the class in a delta of $M$.

<footnote n="11">¹¹ We are working on a family-based analysis for performing this latter check as well (Section 12).</footnote>
* It associates each field/method name a, which may be an attribute of the class, with the non-empty set of the variable/method types of a. Let M be the VM of the class. Then the domain of the mapping contains the names of the fields/methods

- that are defined in a class declaration occurring in the core part of M or in a delta of M,

- that are subject of an attribute operation in a *modifies*-operation on the class in a delta of M.

2. A family interface signature, ranged over by FIS, aggregates the information of all signatures of an interface in all variants.

* It contains the interface name.

* It associates the keyword super with the set R of interface references that may be supertypes of the interface. Let M be the VM of the interface. Then the set R contains all the interface references

- that are listed in the *extends*-clause of any definition of the interface in the core part of M or in a delta of M,

- that are added to the *extends*-clause of the interface by a *modifies*-operation on the interface in a delta of M.

* It associates each method name m, which may be a method of the interface, with the non-empty set of the method types of m. Let M be the VM of the interface. Then the domain of the mapping contains the names of the methods

- that are defined in an interface declaration occurring in the core part of M or in a delta of M,

- that are subject of a header operation in a *modifies*-operation on the interface in a delta of M.

3. A family module signature, ranged over by F, aggregates the information of all signatures of a module in all variants.

* It contains the module name M.

* It associates the keyword export with its exported trade clause tC.

* It associates the keyword import with the set of all imported pairs (tCi, Mi), where n ≥ 0 and Mi ≠ M (1 ≤ i ≤ n).

* It associates each class/interface name (defined in the core part of M and/or subject of a class/interface operation in a delta of M) with its family class/interface signature.

* It associates the name of each open product (defined in M) with its definition.

* It optionally contains a feature model, denoted with F<mod>dl<mod>.FM.

We write `fsig(Mdl)` to denote the family signature of `Mdl`.

4. A family program signature, ranged over by FPrgS, aggregates the information of all signatures of a program in all variants. It associates each module name M with its family module signature. We write `fsig(Prg)` to denote the family signature of program Prg.

It is obvious that `fsig(Prg)` can be computed by inspection of Prg.

**Definition 23** (*Subtyping Relation Induced by Family Program Signature*). The subtyping relation induced by a family program signature FPrgS, denoted by <:FPrgS, is the transitive closure of the union of the following two relations:

1. The identity relation on primitive types and on the qualified class/interface names in `dom(FPrgS)`;

2. `{(M, N, strip(IR)) | M ∈ dom(FPrgS), N ∈ dom(FPrgS(M)), IR ∈ FPrgS(M)(N)(super))}`.

When FPrgS is clear from the context, we simply write <: instead of <:FPrgS.

It is worth observing that the relation in Definition 23.2 might be cyclic.

We can now formalize type uniformity as follows.

**Definition 24** (*Type Uniformity*). A family program signature FPrgS is type uniform if the following conditions hold:

1. For every VM name M appearing anywhere in FPrgS, we have M ∈ dom(FPrgS).

2. For every qualified class/interface name M, N appearing anywhere in FPrgS, we have N ∈ dom(FPrgS(M));

3. For every VM name M ∈ dom(FPrgS), every class/interface name N ∈ dom(FPrgS(M)(N)), and every attribute name a ∈ dom(FPrgS(M)) the set FPrgS(M)(a) is a singleton.

4. For every traded name tN appearing in FPrgS(M)(export) that occurs in `dom(FPrgS(M))`, we have N ∈ `dom(FPrgS(M))`.

5. If FPrgS(M)(import) contains a pair (tC, M') then M' ≠ M and all traded names in tC occur in FPrgS(M')(export).

6. The relation given in item 2 of Definition 23 is acyclic.

7. For all VMs M, M<sub>i</sub>, M<sub>i</sub> ∈ `dom(FPrgS)`, classes/interfaces N ∈ `dom(FPrgS(M))`, interfaces I<sub>i</sub> ∈ `dom(FPrgS(M<sub>i</sub>))` (i ∈ {1, 2}): if M, N <: M<sub>i</sub>, I<sub>i</sub> and M, N <: M<sub>i</sub>, I<sub>i</sub> then for each attribute a ∈ `dom(FPrgS(M<sub>i</sub>)(I<sub>i</sub>))` ∩ `dom(FPrgS(M<sub>i</sub>)(I<sub>i</sub>))` we have FPrgS(M<sub>i</sub>)(I<sub>i</sub>)(a) = FPrgS(M<sub>i</sub>)(M<sub>i</sub>)(I<sub>i</sub>)(a).

An ABS-VM program PrgS is type uniform iff `fsig(PrgS)` is type uniform.

Type uniformity of a program can be checked by inspecting its family signature.

**Example 5** (*Type Uniformity*). Consider the program Prg in Fig. 10. The code is type uniform and the program signature `fsig(Prg) = FPrgS` is such that:

$$
\begin{align*}
\mathit{FPrgS}(M)(\mathit{export}) &= \emptyset & \mathit{FPrgS}(M)(\mathit{import}) &= \emptyset \\
\mathit{FPrgS}(I)(\mathit{super}) &= \emptyset & \mathit{FPrgS}(J)(\mathit{super}) &= \{M, I\} \\
\mathit{FPrgS}(J)(m) &= \{() \to \mathit{Unit}\}
\end{align*}
$$

The program looses type uniformity, for example, if one adds the code below to module M.

This would imply `FPrgS(J)(m) = {}(() -> Unit, (Int) -> Unit)`, which breaks type uniformity (third condition).

## 9.2. Pre-typing

We say an ABS-VM program Prg is pre-typed to mean that it is type uniform and all method declarations in the core/delta parts of VMs type check with respect to `fsig(Prg)`. This is formalized by the following by a quite straightforward adaptation of the definition well-typed Vf-ABS program (Definition 18).

**Definition 25** (*Pre-Typed ABS-VM Program*).

1. Let FPrgS be the program signature of a type uniform Vf-ABS program. A VM Mdl such that FPrgS(name(M)) = `fsig(Mdl)` is pre-typed iff the judgment FPrgS || Mdl can be derived by the rules given in Appendix C.
* It associates each field/method name a, which may be an attribute of the class, with the non-empty set of the variable/method types of a. Let M be the VM of the class. Then the domain of the mapping contains the names of the fields/methods

- that are defined in a class declaration occurring in the core part of M or in a delta of M,

- that are subject of an attribute operation in a *modifies*-operation on the class in a delta of M.

2. A family interface signature, ranged over by FIS, aggregates the information of all signatures of an interface in all variants.

* It contains the interface name.

* It associates the keyword super with the set R of interface references that may be supertypes of the interface. Let M be the VM of the interface. Then the set R contains all the interface references

- that are listed in the *extends*-clause of any definition of the interface in the core part of M or in a delta of M,

- that are added to the *extends*-clause of the interface by a *modifies*-operation on the interface in a delta of M.

* It associates each method name m, which may be a method of the interface, with the non-empty set of the method types of m. Let M be the VM of the interface. Then the domain of the mapping contains the names of the methods

- that are defined in an interface declaration occurring in the core part of M or in a delta of M,

- that are subject of a header operation in a *modifies*-operation on the interface in a delta of M.

3. A family module signature, ranged over by F, aggregates the information of all signatures of a module in all variants.

* It contains the module name M.

* It associates the keyword export with its exported trade clause tc.

* It associates the keyword import with the set of all imported pairs (tcᵢ, Mᵢ), where n ≥ 0 and Mᵢ ≠ M (1 ≤ i ≤ n).

* It associates each class/interface name (defined in the core part of M and/or subject of a class/interface operation in a delta of M) with its family class/interface signature.

* It associates the name of each open product (defined in M) with its definition.

* It optionally contains a feature model, denoted with F<mod>dl<mod>s.FM.

We write `fsig(Mdl)` to denote the family signature of `Mdl`.

4. A family program signature, ranged over by FPrgS, aggregates the information of all signatures of a program in all variants. It associates each module name M with its family module signature. We write `fsig(Prg)` to denote the family signature of program Prg.

It is obvious that `fsig(Prg)` can be computed by inspection of Prg.

**Definition 23** (*Subtyping Relation Induced by Family Program Signature*). The subtyping relation induced by a family program signature FPrgS, denoted by <:FPrgS, is the transitive closure of the union of the following two relations:

1. The identity relation on primitive types and on the qualified class/interface names in `dom(FPrgS)`;

2. `{(M, N, strip(IR)) | M ∈ dom(FPrgS), N ∈ dom(FPrgS(M)), IR ∈ FPrgS(M)(N)(super)}`.

When FPrgS is clear from the context, we simply write <: instead of <:FPrgS.

It is worth observing that the relation in Definition 23.2 might be cyclic.

We can now formalize type uniformity as follows.

**Definition 24** (*Type Uniformity*). A family program signature FPrgS is type uniform if the following conditions hold:

1. For every VM name M appearing anywhere in FPrgS, we have M ∈ dom(FPrgS).

2. For every qualified class/interface name M, N appearing anywhere in FPrgS, we have N ∈ dom(FPrgS(M));

3. For every VM name M ∈ dom(FPrgS), every class/interface name N ∈ dom(FPrgS(M)(N)), and every attribute name a ∈ dom(FPrgS(M)) the set FPrgS(M)(a) is a singleton.

4. For every traded name tN appearing in FPrgS(M)(export) that occurs in `dom(FPrgS(M))`, we have N ∈ `dom(FPrgS(M))`.

5. If FPrgS(M)(import) contains a pair (tc, M') then M' ≠ M and all traded names in tc occur in FPrgS(M')(export).

6. The relation given in item 2 of Definition 23 is acyclic.

7. For all VMs M, M₁, M₂ ∈ `dom(FPrgS)`, classes/interfaces N ∈ `dom(FPrgS(M))`, interfaces Iᵢ ∈ `dom(FPrgS(Mᵢ))` (i ∈ {1, 2}): if M, N <: M₁, I₁ and M, N <: M₂, I₂ then for each attribute a ∈ `dom(FPrgS(M₁)(I₁))` ∩ `dom(FPrgS(M₂)(I₂))` we have FPrgS(M₁)(I₁)(a) = FPrgS(M₂)(I₂)(a).

An ABS-VM program PrgS is type uniform iff `fsig(PrgS)` is type uniform.

Type uniformity of a program can be checked by inspecting its family signature.

**Example 5** (*Type Uniformity*). Consider the program Prg in Fig. 10. The code is type uniform and the program signature `fsig(Prg) = FPrgS` is such that:

$$ 
\begin{align*}
\mathit{FPrgS}(M)(\mathit{export}) &= \emptyset & \mathit{FPrgS}(M)(\mathit{import}) &= \emptyset \\
\mathit{FPrgS}(I)(\mathit{super}) &= \emptyset & \mathit{FPrgS}(J)(\mathit{super}) &= \{M, I\} \\
\mathit{FPrgS}(J)(m) &= \{() \to \mathit{Unit}\}
\end{align*}
$$

The program looses type uniformity, for example, if one adds the code below to module M.

This would imply `FPrgS(J)(m) = {() → Unit, (Int) → Unit}`, which breaks type uniformity (third condition).

## 9.2. Pre-typing

We say an ABS-VM program Prg is pre-typed to mean that it is type uniform and all method declarations in the core/delta parts of VMs type check with respect to `fsig(Prg)`. This is formalized by the following by a quite straightforward adaptation of the definition well-typed Vf-ABS program (Definition 18).

**Definition 25** (*Pre-Typed ABS-VM Program*).

1. Let FPrgS be the program signature of a type uniform Vf-ABS program. A VM Mdl such that FPrgS(name(M)) = `fsig(Mdl)` is pre-typed iff the judgment FPrgS ⊑ Mdl can be derived by the rules given in Appendix C.
delta D3; modifies interface J { adds Unit m(Int i); }
delta D3 when F2;

module M;
features F1, F2 with F1 <-> !F2;
unique interface I {}
interface J extends I {}
delta D1; modifies interface J { adds Unit m(); }
delta D2; modifies interface J { modifies Unit m(); }
delta D1 when F1;
delta D2 when F1 after D1;

<caption>Fig. 10. A type uniform program.</caption>

2. An ABS-VM program Prg is pre-typed iff the judgment $|- \text{Prg}$ can be derived by the following rule:

$$ \begin{array}{l} \text{PT:Prg} \\ \text{fsig(Prg) is type uniform} \end{array} \quad \begin{array}{l} \text{fsig(Prg)}|- \text{Mdl}, \text{ for all } \text{Mdl} \in \text{Prg} \\ \qquad |- \text{Prg} \end{array} $$

**Remark 3 (Early Error Detection).** PEV-compliance (Definition 3), normal form adherence (Definition 5), type uniformity (Definition 24), and pre-typing (Definition 25) can be relaxed by extending them to ABS-VM programs that do not satisfy the SAT sanity conditions (final bullet in Section 5.2). These relaxed properties, called SAT-free X (where $X \in \{\text{PEV-compliance, normal form, type uniformity, pre-typing}\}$) can be checked by inspection without a SAT solver. It is also obvious that, if an ABS-VM program satisfies property SAT-free X plus the SAT sanity conditions, then it satisfies property X. Therefore, ABS-VM program developers may frequently trigger an inexpensive check of the SAT-free X properties (an IDE can perform them in the background, providing immediate detection of the associated errors), while being more careful in triggering the (potentially more time consuming) checks involving a SAT solver.

### 9.3. Applicability consistency for normal form ABS-vm programs

In this section we assume each feature $f$ is qualified by the name of the VM $M$, where its feature model is defined (denoted $M.f$) and each delta name $D$ is qualified by the name of its VM (denoted $M.D$).

Let $\text{getFm}(\text{Prg}, M)$ denote the feature model formula of VM $M$ (given in its module header), let $\text{getFm}(\text{Prg})$ denote the conjunction of all feature model formulas $\bigwedge_{M \in \text{dom}(\text{PrgS})} \text{getFm}(\text{Prg}, M)$, and let $\text{getAct}(\text{Prg}, M.D)$ denote the activation condition formula of the delta with name $D$ defined in VM $M$ (given in its configuration knowledge).

Let $\mathcal{I}$ be an assignment from feature variables occurring in the feature models of Prg to Boolean values such that all feature formulas of Prg are satisfied. Then, for each $M$ and such $\mathcal{I}$, this defines the product $\pi_M^I = \{M.f | f \text{ is a feature of } M \text{ and } \mathcal{I}(M.f) = \text{true}\}$. We define the function $\text{getFmAct}$ mapping each program Prg to a formula over qualified feature names and qualified delta names (of Prg).

$$ \begin{align*} \text{getFmAct}(\text{Prg}) &= \bigwedge_{M \in \text{dom}(\text{PrgS})} \text{getFmAct}(\text{Prg}, M) \\ \text{getFmAct}(\text{Prg}, M) &= \text{getFm}(\text{Prg}, M) \wedge \\ & \quad (\bigwedge_D \text{is a delta of } M^{M.D} \Leftrightarrow \text{getAct}(\text{Prg}, M.D)) \end{align*} $$

We note that by construction for each assignment $\mathcal{I}$: formula $\text{getFmAct}(\text{Prg})$ is satisfied by $\mathcal{I}$ iff $\text{getFm}(\text{Prg})$ is satisfied by $\mathcal{I}$ and $\mathcal{I}(M.D) = \mathcal{I}(\text{getAct}(\text{Prg}, M.D))$. Hence, $\mathcal{I}(M.D) = \text{true}$ if and only if the delta $M.D$ is activated by the product $\pi_M^I$.

Let $Q$ range over fully qualified class/interface names $M.N$ and fully qualified attribute names $M.N.a$. Let $\text{FmdlS}(M.N)$ be short for

$\text{FmdlS}(M)(N)$ and let $\text{FmdlS}(M.N.a)$ be short for $\text{FmdlS}(M)(N)(a)$. The deep domain of a module $M$ such that $\text{fsig}(M)=\text{FmdlS}$ is

$$ \text{ddom}(M) = \{M.N | \text{FmdlS}(M.N) \text{ is defined}\} \\ \cup \{M.N.a | \text{FmdlS}(M.N.a) \text{ is defined}\}. $$

The deep domain of a program Prg is $\text{ddom}(\text{Prg}) = \bigcup_{M \in \text{dom}(\text{PrgS})} \text{ddom}(M)$.

Let $\Phi$ denote a Boolean formula over qualified feature names and qualified delta names of a given VM $M$ of Prg and let $\text{KE}$ be a product of $M$. Then $\text{eval}(\text{KE}, \Phi, \text{Prg})$ denotes the Boolean value of the formula $\Phi$ under the assignment $\mathcal{I}$ such that:

$$ \mathcal{I}(x) = \begin{cases} \text{true} & \text{if } x \text{ is a feature in } \text{KE} \\ \text{false} & \text{if } x \text{ is a feature not in } \text{KE} \\ \mathcal{I}(\text{getAct}(\text{Prg}, x)) & \text{if } x \text{ is a delta name} \end{cases} $$

**Definition 26 (Applicability Consistency).** Let Prg be a normal form ABS-VM program and let the judgment $|- \text{Prg} : \Theta, \Phi$ be derivable with the rules given in Appendix D, where: $\Phi$ (called applicability constraint) is as above, and $\Theta$ (called declaration presence mapping) is a mapping from $\text{ddom}(\text{Prg})$ to propositional formulas over features and delta names. We say that Prg is applicability consistent to mean that the formula $\text{getFmAct}(\text{Prg}) \Rightarrow \Phi$ is valid.

During product generation the selected deltas must be applicable in the given order, otherwise generation would not succeed (see explanation immediately after Definition 10).

The rules in Appendix D build the applicability constraint and the declaration presence mapping of the normal form ABS-VM program Prg by parsing it from the left to right. Consistent with Section 5.1, for each VM we assume the list of deltas in Prg being a total order compatible with the configuration knowledge CK: hence, this analysis assumes deltas are applied in the order of their occurrence in Prg. At any stage $t$ during the parsing process, the applicability constraint collects the information on the applicability of deltas until $t$. This constraint is defined simultaneously with the declaration presence mapping that collects for all possible subjects of delta operations the information on their presence at stage $t$. The applicability check succeeds for deltas applied until $t$, whenever the applicability constraint holds for all products.

**Theorem 2 (Soundness and Completeness of Applicability Consistency).** Let Prg be a normal form ABS-VM program such that $|- \text{Prg} : \Theta, \Phi$ holds.

1. The overall flattening of Prg succeeds iff Prg is applicability consistent.

2. Let Prg be applicability consistent. For every product $\pi$ of $M$:

(a) $\text{eval}(\pi, \Theta(M.N), \text{Prg}) = \text{true}$ iff the declaration of class/interface $N$ occurs in the flattening of $M$ (relative to $\pi$ if $M.N$ is not unique, relative to $\perp$ otherwise).
delta D3; modifies interface J { adds Unit m(Int i); }
delta D3 when F2;

module M;
features F1, F2 with F1 <-> !F2;
unique interface I {}
interface J extends I {}
delta D1; modifies interface J { adds Unit m(); }
delta D2; modifies interface J { modifies Unit m(); }
delta D1 when F1;
delta D2 when F1 after D1;

<caption>Fig. 10. A type uniform program.</caption>

2. An ABS-VM program Prg is pre-typed iff the judgment $|- \text{Prg}$ can be derived by the following rule:

PT: Prg

    fsig(Prg) is type uniform
    fsig(Prg) |- Mdl, for all Mdl ∈ Prg
    |- Prg

**Remark 3 (Early Error Detection).** PEV-compliance (Definition 3), normal form adherence (Definition 5), type uniformity (Definition 24), and pre-typing (Definition 25) can be relaxed by extending them to ABS-VM programs that do not satisfy the SAT sanity conditions (final bullet in Section 5.2). These relaxed properties, called SAT-free X (where $X \in \{\text{PEV-compliance, normal form, type uniformity, pre-typing}\}$) can be checked by inspection without a SAT solver. It is also obvious that, if an ABS-VM program satisfies property SAT-free X plus the SAT sanity conditions, then it satisfies property X. Therefore, ABS-VM program developers may frequently trigger an inexpensive check of the SAT-free X properties (an IDE can perform them in the background, providing immediate detection of the associated errors), while being more careful in triggering the (potentially more time consuming) checks involving a SAT solver.

### 9.3. Applicability consistency for normal form ABS-vm programs

In this section we assume each feature $f$ is qualified by the name of the VM $M$, where its feature model is defined (denoted $M.f$) and each delta name $D$ is qualified by the name of its VM (denoted $M.D$).

Let $getFm(Prg, M)$ denote the feature model formula of VM $M$ (given in its module header), let $getFm(Prg)$ denote the conjunction of all feature model formulas $\bigwedge_{M \in \text{dom}(PrgS)} getFm(Prg, M)$, and let $getAct(Prg, M.D)$ denote the activation condition formula of the delta with name $D$ defined in VM $M$ (given in its configuration knowledge).

Let $\mathcal{I}$ be an assignment from feature variables occurring in the feature models of Prg to Boolean values such that all feature formulas of Prg are satisfied. Then, for each $M$ and such $\mathcal{I}$, this defines the product $\pi_M^I = \{M.f | f \text{ is a feature of } M \text{ and } \mathcal{I}(M.f) = \text{true}\}$. We define the function $getFmAct$ mapping each program Prg to a formula over qualified feature names and qualified delta names (of Prg).

$$ 
\begin{align*}
getFmAct(Prg) &= \bigwedge_{M \in \text{dom}(PrgS)} getFmAct(Prg, M) \\
getFmAct(Prg, M) &= getFm(Prg, M) \wedge \\
&\quad (\bigwedge_D \text{ is a delta of } M^{M.D} \Leftrightarrow getAct(Prg, M.D))
\end{align*}
$$

We note that by construction for each assignment $\mathcal{I}$: formula $getFmAct(Prg)$ is satisfied by $\mathcal{I}$ iff $getFm(Prg)$ is satisfied by $\mathcal{I}$ and $\mathcal{I}(M.D) = \mathcal{I}(getAct(Prg, M.D))$. Hence, $\mathcal{I}(M.D) = \text{true}$ if and only if the delta $M.D$ is activated by the product $\pi_M^I$.

Let $Q$ range over fully qualified class/interface names $M.N$ and fully qualified attribute names $M.N.a$. Let $\text{FmdlS}(M.N)$ be short for

$\text{FmdlS}(M)(N)$ and let $\text{FmdlS}(M.N.a)$ be short for $\text{FmdlS}(M)(N)(a)$. The deep domain of a module $M$ such that $\text{fsig}(M)=\text{FmdlS}$ is

$$ \text{ddom}(M) = \{M.N | \text{FmdlS}(M.N) \text{ is defined}\} \\ \cup \{M.N.a | \text{FmdlS}(M.N.a) \text{ is defined}\}. $$

The deep domain of a program Prg is $\text{ddom}(Prg) = \bigcup_{M \in \text{dom}(PrgS)} \text{ddom}(M)$.

Let $\Phi$ denote a Boolean formula over qualified feature names and qualified delta names of a given VM $M$ of Prg and let $\text{KE}$ be a product of $M$. Then $\text{eval}(\text{KE}, \Phi, \text{Prg})$ denotes the Boolean value of the formula $\Phi$ under the assignment $\mathcal{I}$ such that:

$$ \mathcal{I}(x) = \begin{cases} \text{true} & \text{if } x \text{ is a feature in } \text{KE} \\ \text{false} & \text{if } x \text{ is a feature not in } \text{KE} \\ \mathcal{I}(getAct(Prg, x)) & \text{if } x \text{ is a delta name} \end{cases} $$

**Definition 26 (Applicability Consistency).** Let Prg be a normal form ABS-VM program and let the judgment $|- \text{Prg} : \Theta, \Phi$ be derivable with the rules given in Appendix D, where: $\Phi$ (called applicability constraint) is as above, and $\Theta$ (called declaration presence mapping) is a mapping from $\text{ddom}(\text{Prg})$ to propositional formulas over features and delta names. We say that Prg is applicability consistent to mean that the formula $getFmAct(Prg) \Rightarrow \Phi$ is valid.

During product generation the selected deltas must be applicable in the given order, otherwise generation would not succeed (see explanation immediately after Definition 10).

The rules in Appendix D build the applicability constraint and the declaration presence mapping of the normal form ABS-VM program Prg by parsing it from the left to right. Consistent with Section 5.1, for each VM we assume the list of deltas in Prg being a total order compatible with the configuration knowledge CK: hence, this analysis assumes deltas are applied in the order of their occurrence in Prg. At any stage $t$ during the parsing process, the applicability constraint collects the information on the applicability of deltas until $t$. This constraint is defined simultaneously with the declaration presence mapping that collects for all possible subjects of delta operations the information on their presence at stage $t$. The applicability check succeeds for deltas applied until $t$, whenever the applicability constraint holds for all products.

**Theorem 2 (Soundness and Completeness of Applicability Consistency).** Let Prg be a normal form ABS-VM program such that $|- \text{Prg} : \Theta, \Phi$ holds.

1. The overall flattening of Prg succeeds iff Prg is applicability consistent.

2. Let Prg be applicability consistent. For every product $\pi$ of $M$:

(a) $\text{eval}(\pi, \Theta(M.N), \text{Prg}) = \text{true}$ iff the declaration of class/interface $N$ occurs in the flattening of $M$ (relative to $\pi$ if $M.N$ is not unique, relative to $\perp$ otherwise).
(b) For all M:N:a ∈ dom(Θ) it holds that: eval(π,Θ(M:N:a),Prg) = true iff the declaration of N occurs in the flattening of M (relative to π if M:N is not unique, relative to ⊥ otherwise) and contains the declaration of the field/method a.

**Proof.** The proof is by rule [A:PRG] in Appendix D and Lemma 9 in Appendix E. □

It is easy to see that using Definition 3.1 we can strengthen the theorem to state that for all *unique* classes/interfaces the formulas collected in $\Theta$ are always *true*.

# 10. Integration into the ABS tool chain

We implemented the VM concept as part of the ABS compiler tool chain with the exception of open product definitions, currently under development. The implementation, together with all case studies and test cases, is available as an open source extension of the ABS compiler.<fnref n="12" /> The README file in the repository describes how to access the case studies.

To integrate VMs into the ABS compiler tool chain, only the frontend (parser and preprocessor) needed to be changed. This is, because flattening (Section 7.2) produces variability-free ABS code, keeping ABS code generation and semantic analysis (type checking of single variants) as is. The ABS parser’s grammar is extended with the constructs described in Section 5. As expected, ABS’s existing delta application mechanism, including original calls, could be fully reused.

Several sanity conditions, specifically those concerned with export and import clauses, boil down to simple checks once normal form is established. The SAT sanity conditions are solved using the Choco<fnref n="13" /> solver, which is included in the ABS tool chain and used there already for the µTVL (Clarke et al., 2010) feature modeling language of the global product line system of ABS. Pre-typing requires to have a version of the type checker that uses the pre-computed signatures, instead of resolving type names with the class table. The error reporting mechanism is reused from the standard type checker.

The VM tool chain implementation has two aspects, several helper classes, and consists of the following components: (i) Safety condition checking (Section 5.2) with error reporting in case a condition is violated (current implementation has limitations); (ii) PEV-compliance checking (Section 6) with error reporting in case the PEV is violated; (iii) flattening (Section 7.2); (iv) adjustment of the feature model (needed, because VMs use a simpler feature modeling language than ABS’s µTVL Clarke et al., 2010).

SAT-free PEV-compliance and flattening are performed as part of the standard workflow of the compiler. For backwards compatibility, pre-typing and the applicability check are implemented as optional commands rather than mandatory steps during compilation, analogous to other static analyses for product lines in ABS such as Damiani et al. (2017b). There are two command line instructions to initiate compilation: "absc varcheck <files>" performs all checks, while "absc varcheck -nosat <files>" skips all steps requiring SAT solving: it only checks the SAT-free sanity conditions and performs pre-typing.

Delta operations on *extends* and *implies* are not supported by ABS yet, and thus, consequently, neither by our VM extension of ABS.

# 11. Evaluation

## 11.1. Research questions

Qualitative and quantitative aspects of VMs are evaluated along the following research questions:

**RQ 1** Does using ABS-VM provide advantages in terms of reduced implementation effort and code readability for existing models, where variant interoperability is implemented by relying on duplicating code (possibly based on programming constructs for intra-code reuse to reduce code duplication, see Section 3) or on external tools?

**RQ 2** Does using ABS-VM provide advantages in terms of reduced model size compared to Delta-ABS and Delta-Trait-ABS?

**RQ 3** Does performing the family-based static normal form, type uniformity, applicability and pre-typing checks<fnref n="14" /> (described in Section 9) require less time than overall flattening<fnref n="15" /> (according to Definition 19) on an ABS-VM program?

**RQ 4** Does performing the family-based static normal form, type uniformity, applicability and pre-typing checks require less time than flattening (according to Definition 13) on an ABS-VM program?

## 11.2. Experiment design

### 11.2.1. Experiment design and subject for RQ 1 and RQ 2

To investigate the first two research questions, we use ABS-VM to refactor (possibly extended versions of) legacy models. The source code of the case studies is available at the URL given in footnote 12. The legacy models are as follows:

* The industrial FormbaR model of railway operations, available in two versions, see Remark 1. The first version, FormbaR-1 (Kamburjan and Hähnle, 2016), is implemented in Delta-ABS. The second version, FormbaR-2 (Kamburjan et al., 2018), is implemented in Delta-Trait-ABS. Both versions use one class per infrastructure element and, to achieve variant interoperability, different variants of the same infrastructure element are explicitly defined as separate classes without using DOP for implementing infrastructure elements.

* The second version of the *Weak Memory Model Family*, referred to as WMMF-2 and implemented in Delta-ABS. It is the extension of an ABS model of weak memory (Kamburjan and Hähnle, 2018), referred to as WMMF-1 and implemented in Delta-ABS.

In sequentially consistent memory models all read- and write-accesses in a piece of code are processed in the stated order. Weakly consistent (for short: weak) memory models permit partial or complete re-ordering of memory access to increase efficiency. WMMF-1 formalizes different relaxation strategies and hardware models to enable simulation and analysis of their effects. A weak memory model in WMMF-1 is implemented as a class managing a list of memory accesses on a device. Variability, including different types of reordering (read before write, etc.), is implemented by DOP. WMMF-2 extends WMMF-1 to include two co-existing hardware devices with two different memory systems each: any of the four combinations of memory model can be

<footnote n="12">¹² The code is available under https://github.com/Edkamb/abstools/tree/variable_mod. A runnable VM is available under https://doi.org/10.5281/zenodo.4926115.</footnote>

<footnote n="13">¹³ https://choco-solver.org.</footnote>

<footnote n="14">¹⁴ Recall that checking normal form and applicability consistency is a way to ensure that all variants of all VMs can be generated, without actually generating them.</footnote>

<footnote n="15">¹⁵ The brute force approach to check whether all variants of all VMs can be generated: by producing them.</footnote>
(b) For all M:N:a ∈ dom(Θ) it holds that: eval(π,Θ(M:N:a),Prg) = true iff the declaration of N occurs in the flattening of M (relative to π if M:N is not unique, relative to ⊥ otherwise) and contains the declaration of the field/method a.

**Proof.** The proof is by rule [A:PRG] in Appendix D and Lemma 9 in Appendix E. □

It is easy to see that using Definition 3.1 we can strengthen the theorem to state that for all *unique* classes/interfaces the formulas collected in $\Theta$ are always *true*.

# 10. Integration into the ABS tool chain

We implemented the VM concept as part of the ABS compiler tool chain with the exception of open product definitions, currently under development. The implementation, together with all case studies and test cases, is available as an open source extension of the ABS compiler.<fnref n="12" /> The README file in the repository describes how to access the case studies.

To integrate VMs into the ABS compiler tool chain, only the frontend (parser and preprocessor) needed to be changed. This is, because flattening (Section 7.2) produces variability-free ABS code, keeping ABS code generation and semantic analysis (type checking of single variants) as is. The ABS parser’s grammar is extended with the constructs described in Section 5. As expected, ABS’s existing delta application mechanism, including original calls, could be fully reused.

Several sanity conditions, specifically those concerned with export and import clauses, boil down to simple checks once normal form is established. The SAT sanity conditions are solved using the Choco<fnref n="13" /> solver, which is included in the ABS tool chain and used there already for the µTVL (Clarke et al., 2010) feature modeling language of the global product line system of ABS. Pre-typing requires to have a version of the type checker that uses the pre-computed signatures, instead of resolving type names with the class table. The error reporting mechanism is reused from the standard type checker.

The VM tool chain implementation has two aspects, several helper classes, and consists of the following components: (i) Safety condition checking (Section 5.2) with error reporting in case a condition is violated (current implementation has limitations); (ii) PEV-compliance checking (Section 6) with error reporting in case the PEV is violated; (iii) flattening (Section 7.2); (iv) adjustment of the feature model (needed, because VMs use a simpler feature modeling language than ABS’s µTVL Clarke et al., 2010).

SAT-free PEV-compliance and flattening are performed as part of the standard workflow of the compiler. For backwards compatibility, pre-typing and the applicability check are implemented as optional commands rather than mandatory steps during compilation, analogous to other static analyses for product lines in ABS such as Damiani et al. (2017b). There are two command line instructions to initiate compilation: "absc varcheck <files>" performs all checks, while "absc varcheck -nosat <files>" skips all steps requiring SAT solving: it only checks the SAT-free sanity conditions and performs pre-typing.

Delta operations on *extends* and *implies* are not supported by ABS yet, and thus, consequently, neither by our VM extension of ABS.

# 11. Evaluation

## 11.1. Research questions

Qualitative and quantitative aspects of VMs are evaluated along the following research questions:

**RQ 1** Does using ABS-VM provide advantages in terms of reduced implementation effort and code readability for existing models, where variant interoperability is implemented by relying on duplicating code (possibly based on programming constructs for intra-code reuse to reduce code duplication, see Section 3) or on external tools?

**RQ 2** Does using ABS-VM provide advantages in terms of reduced model size compared to Delta-ABS and Delta-Trait-ABS?

**RQ 3** Does performing the family-based static normal form, type uniformity, applicability and pre-typing checks<fnref n="14" /> (described in Section 9) require less time than overall flattening<fnref n="15" /> (according to Definition 19) on an ABS-VM program?

**RQ 4** Does performing the family-based static normal form, type uniformity, applicability and pre-typing checks require less time than flattening (according to Definition 13) on an ABS-VM program?

## 11.2. Experiment design

### 11.2.1. Experiment design and subject for RQ 1 and RQ 2

To investigate the first two research questions, we use ABS-VM to refactor (possibly extended versions of) legacy models. The source code of the case studies is available at the URL given in footnote 12. The legacy models are as follows:

* The industrial FormbaR model of railway operations, available in two versions, see Remark 1. The first version, FormbaR-1 (Kamburjan and Hähnle, 2016), is implemented in Delta-ABS. The second version, FormbaR-2 (Kamburjan et al., 2018), is implemented in Delta-Trait-ABS. Both versions use one class per infrastructure element and, to achieve variant interoperability, different variants of the same infrastructure element are explicitly defined as separate classes without using DOP for implementing infrastructure elements.

* The second version of the *Weak Memory Model Family*, referred to as WMMF-2 and implemented in Delta-ABS. It is the extension of an ABS model of weak memory (Kamburjan and Hähnle, 2018), referred to as WMMF-1 and implemented in Delta-ABS.

In sequentially consistent memory models all read- and write-accesses in a piece of code are processed in the stated order. Weakly consistent (for short: weak) memory models permit partial or complete re-ordering of memory access to increase efficiency. WMMF-1 formalizes different relaxation strategies and hardware models to enable simulation and analysis of their effects. A weak memory model in WMMF-1 is implemented as a class managing a list of memory accesses on a device. Variability, including different types of reordering (read before write, etc.), is implemented by DOP. WMMF-2 extends WMMF-1 to include two co-existing hardware devices with two different memory systems each: any of the four combinations of memory model can be

<footnote n="12">12 The code is available under https://github.com/Edkamb/abstools/tree/variable_mod. A runnable VM is available under https://doi.org/10.5281/zenodo.4926115.</footnote>

<footnote n="13">13 https://choco-solver.org.</footnote>

<footnote n="14">14 Recall that checking normal form and applicability consistency is a way to ensure that all variants of all VMs can be generated, without actually generating them.</footnote>

<footnote n="15">15 The brute force approach to check whether all variants of all VMs can be generated: by producing them.</footnote>
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">¹⁸ Main signal, pre-signal, speed limiter, pre-speed limiters, and point of visibility (Kamburjan et al., 2018).</footnote>