Typechecking for software product lines

Software product lines (SPL) describes how to assemble and customise software for different customers or devices. Around a common core, a description language defines for each product which differences to apply. #ifdefs from the C preprocessor are a low-tech solution to this problem.

In the C/C++ world, the draw back is that only one product—defined through the preprocessor flags— is checked or compiled into a product. This leads to an exponential number of potential products. After each change to the software, in the worst case, all products must be compiled again to check e.g. for type errors! Clearly this does not scale.

Recently, there have been improvements in that regard in the high(er)-level language community: product lines can now be easily specified for Java, e.g. in DeltaJ or in CIDE (Colored Integrated Development Environment). To some degree, type checking is applied to all products simultaneously, without running into complexity issues of the exponential number of products. These has even been extended to static analysis for such code, e.g. in SPLlift.

In the PMA group, we have developed a modelling language with support for SPLs, called ABS (Abstract Behaviour Specification language). It can be compiled into various languages like Java and Erlang. However, the type checker has not been extended to the SPL-domain yet, making it unfortunately difficult to develop larger modular projects.

In this thesis, you will (building on the existing code) extend the type checker to consider all possible products, using similar techniques. Here is a fragment of ABS code, with the core at the top, then the deltas, and the final product line description at the end:

module CoCoME;

import * from Datatypes;

class Store implements Store {
  Catalog cat = insert(EmptyMap, Pair(1,Item(1,1)));
  Item lookup(Int code) { return lookupDefault(cat,code,Item(1,1)); }
  // Golden +5 AmEx:
  Bool authorize(CCData cc) { return True; }
  
  Unit log(Sale s) { skip; } // not relevant
}

delta Credit;
 modifies class CoCoME.Cashdesk {
  adds Bool cardPay(CCData cc)
    { return store.authorize(cc);}
  adds Int cashPay(Int given)
    { return this.pay(given); }
 }
...

delta Express(Int k);
 modifies class CoCoME.Cashdesk {
  adds Bool mode = False; // initially in normal mode
  adds Unit setExpress(Bool m) { mode = m; }
  modifies Unit enterItem(Int code, Int qty) {
  // You are allowed to buy k items in ExpressMode
    if (mode && length(items) == k) { assert False;}
                               else { original(code,qty);}
  }
...

productline CoCoME;
  features Mon, Express, Credit;
  delta Monitor when Mon;
  delta Credit when Credit;
  delta CreditMon after Credit when Credit && Mon;
  delta Express(10) when Express;
  delta ExpressMon after Express when Express && Mon;
  delta ExpressCC after Credit when Express && Credit;
  delta ExpressCCMon after Credit,ExpressMon when Express && Credit && Mon;

product BaseMon(Mon);
product Credit(Credit);
product CreditMon(Credit,Mon);
product Ex(Express);
product ExMon(Express,Mon);
product CCEx(Express,Credit);
product CreditExMon(Express,Credit,Mon);

The trick is to collect the boolean features that enable a particular delta (the description of the modifications to the program), and, since delta applications can be stacked, develop a partial order of products that can be successively checked.

This thesis is within the Envisage project.