A machine-checked model of safe composition

Programs of a software product line can be synthesized by composing features which implement some unit of program functionality. In most product lines, only some combination of features are meaningful; feature models express the high-level domain constraints that govern feature compatability. Product line developers also face the problem of safe composition– whether every product allowed by a feature model is type-safe when compiled and run. To study the problem of safe composition, we present Lightweight Feature Java (LFJ), an extension of Lightweight Java with support for features. We define a constraint-based type system for LFJ and prove its soundness using a full formalization of LFJ in Coq. In LFJ, soundness means that any composition of features that satisfies the typing constraints will generate a well-formed LJ program. Categories and Subject Descriptors F.3.3 [Studies of Program Constructs]: Type structure General Terms Design, Languages Keywords Product lines, Type safe...

• Type: Conference
• Year: 2009
• Where: FOAL
• Authors: Benjamin Delaware, William R. Cook, Don S. Batory
• Keywords: Feature Model, FOAL 2009, Natural Language Processing, Product Lines, Software Product Line