An Extension of Feature Algebra

P. Höfner, B. Möller

Abstract: Feature algebra was introduced as an abstract framework for feature oriented software development. One goal is to provide a common, clearly defined basis for the key ideas of feature orientation. So far, feature algebra captures major aspects of feature orientation, like the hierarchical structure of features and feature composition. However, as we will show, it is not able to model aspects at the level of code, i.e., situations where code fragments of different features have to be merged. With other words, it does not reflect details of concret implementations. In the paper we first present concrete models for the original axioms of feature algebra which represent the main concepts of feature oriented programs. This shows that the abstract feature algebra can be interpreted in different ways. We then use these models to show that the axioms of feature algebra do not reflect all aspects of feature orientation properly. This gives the motivation to extend the abstract algebra — which is the second main contribution of the paper. We modify the axioms and introduce the concept of an extended feature algebra. The original algebra can be retrieved by a single additional axiom. As third contribution we introduce more operators to coveer concepts like overriding in the abstract setting.

Paper: pdf


For proving the lemmata and theorems presented in the paper we made use of the following tools:

Waldmeister [BHF96] is a theorem prover for unit equational logic. Its proof procedure is unfailing Knuth-Bendix completion [BDP89]. Waldmeister's main advantage is that efficiency has been reached in terms of time as well as of space. The provided files were tested with Version July 99.

Isabelle/HOL [NPW02] is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The provided theories were tested using Isabelle 2015.

Haskell (e.g. [Pey03]) is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing.

Feature Algebra

A Feature Algebra is a tuple (M, I, +, ⚬,·, 0,1) such that for all m,n∈M and all i,j∈I

We have used Waldmeister and Isabelle/HOL to prove various facts about Feature Algebra.

An input file for Waldmeister for the original Feature Algebra can be downloaded here. All theorems presented in our paper can be proven in no time. The input file contains all proof goals; just uncomment the goals you want to prove.

The Isabelle theory containing all presented lemmas and proofs of Feature Algebra can be found here.

Models of Feature Algebra

In our paper we presented two different models for Feature algebra. The first one is based on prefix-closed sets, the other is based on prefix-free lists.

The first Isabelle theory shows that sets (under set union) and prefix-closed sets form a distant-idempotent monoid. The former is not mentioned in the paper, but a nice exercise in formalise the algebra in Isabelle/HOL. If the models are equipped with the right rewrite-functions, the two models form a feature algebra.

The second Isabelle theory showing that the list-based model forms a feature algebra is also available.

Extended Feature Algebra

An Extended Feature Algebra (EFA) is a tuple (M, I, C, E, +, ⚬, ·, ▻, 0,1) such that the following properties hold for all m,n∈M, i,j∈I, x∈E and a,b∈C.

We proved all facts presented in the paper using Isabelle and Waldmeister; the input files can be found here and here.

Abstract Interfaces and Updates

The restriction ⇂: L × N → L and the removal -:L × N→ L have to satisfy the following axioms:
(a⊔ b) ⇂ p = (a ⇂ p) ⊔ (b ⇂ p)(2)a=(a⇂ p) ⊔ (a-p)(7)
a ⇂ (p⊔ q) = (a ⇂ p) ⊔ (a ⇂ q)(3)a⇂(q-p) = (a-p)⇂ q = (a⇂ q) - p(8)
(a⊔ b)-p = (a-p)⊔ (b-p)(4)p-p=0C(9)
a-(p⊔ q) = (a-p)-q(5)p⇂ q ⊑ q(10)
a ⇂ 0C = 0C(6)
where a,b∈L, p,q∈N. Moreover we assume that N is closed under $⇂$ and $-$, i.e.,if p,q∈N then also p ⇂ q, p-q∈N.

The Isabelle sources can be found here; the theory uses two files from the AFP entry about Kleene Algebra; the two files can be found here.1


L. Bachmair, N. Dershowitz, D.A. Plaisted:Completion Without Failure.In H. Ait-Kaci, M. Nivat (eds.)Resolution of Equations in Algebraic Structures, 1-30.Academic Press, 1989.
A. Buch, Th. Hillenbrand, R. Fettig:WALDMEISTER: High performance equational theorem proving.In J. Calmet, C. Limongelli (eds.)Symposium on Design and Implementation of Symbolic Computation Systems, 63-64.Lecture Notes in Computer Science 1128, 1996.
S. Peyton Jones:Haskell 98 Language and Libraries: The Revised Report.Cambridge University Press, 2003.
T. Nipkow, L.C. Paulson, M. Wenzel:Isabelle/HOL: A Proof Assistant for Higher-Order LogicIn Lecture Notes in Computer Science 2283. Springer, 2002.
1In our submission we had a typo in Cor. 8.9(c); the typo has been fixed in the corresponding Isabelle Files.

Contact: Peter Höfner: peter <at>

Last update: 2015