Fitting The Pieces Together:

A Machine-Checked Model of Safe Composition

Benjamin Delaware, William R. Cook, Don Batory


Programs of a software product line can be synthesized by composing features which implement a 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 compatibility. 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. If the constraints of a feature model imply these typing constraints then all programs allowed by the feature model are type-safe.

Source Files
lj_definitions.v Syntax and semantics of Lightweight Java.
lj_infrastructure.v Proof support for Lightweight Java soundness proofs.
lj_soundness.v Soundness of Lightweight Java's type system.
lj_constraint_definitions.v Definition of our constraint-based type system for Lightweight Java.
lj_constraint_infrastructure.v Proof support for constraint-based soundness proofs.
lj_constraint_soundness.v Soundness of our constraint-based type system for Lightweight Java.
LFJ_definitions.v Definition of our type system for Lightweight Feature Java.
LFJ_infrastructure.v Proof support for LFJ soundness proofs.
LFJ_soundness.v Soundness of our constraint-based type system for Lightweight Feature Java.
base2.v Custom tactics for above proofs.
Natmap.v Natural number-indexed maps used for environments.