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.
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.
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.
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.
| (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) |
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
Contact: Peter Höfner: peter <at> hoefner-online.de
Last update: 2015