Colored Featherweight Java (CFJ)

Colored Featherweight Java (CFJ) is a calculus of a language and type system for software product lines. We designed CFJ for a subset of Java on top of disciplined annotations. It fulfills both desired properties: generation preserves typing and backward compatibility. (The calculus is named colored due to a peculiarity of our product-line tool CIDE which uses background colors to represent annotations.)

We decided to provide a formalization and proof for both properties, after an initial implementation of our type system for Java. We soon found that our implementation was incomplete: We could not give a guarantee and sometimes generated ill-typed variants because we forgot some checks. We found similar problems in other product-line–aware type systems. At the same time, a formalization of our type checks for the entire Java language is not feasible because of Java's complexity and rather informal, textual specification (688 pages!). Instead, we formalize product-line–aware type checking mechanism for Featherweight Java, a subset of Java, and describe how we implemented and extended it toward full Java and other languages.

Although CFJ is based on the existing language FJ (and CFJ's type system is an extension of FJ's type system, due to backward compatibility), CFJ must be considered as a separate language, not as an extended one, to describe an entire software product line instead of a single program. Although technically possible, product lines written in CFJ are not directly executed, but are used to generate FJ programs.



  • Formalization and type soundness proof of CFJ in Coq including a separate formalization with meta-expressions:

  • An older version of the formalization and type soundness proof of CFJ in Coq described in Thüm's Master's thesis:

  • Our formalization is based on a Featherweight Java formalization by de Fraine that we adapted for our purposes:

  • The proof assistant Coq can be downloaded elsewhere.