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-lineaware 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-lineaware 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.
- Christian Kästner, Sven Apel, Thomas Thüm, and Gunter Saake. Type Checking Annotation-Based Product Lines. ACM Transactions on Software Engineering and Methodology, 21(3):14:1-14:39, July 2012.
- Thomas Thüm. A Machine-Checked Proof for a Product-LineAware Type System. Master thesis (Diplomarbeit), University of Magdeburg, Germany, January 2010.
- Christian Kästner and Sven Apel. Type-checking Software Product Lines - A Formal Approach. In Proceedings on the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 258-267. IEEE Computer Society, September 2008.
- Formalization and type soundness proof of CFJ in Coq including a separate formalization with meta-expressions: CFJ_CFJme_2010-08-31.zip.
- An older version of the formalization and type soundness proof of CFJ in Coq described in Thüm's Master's thesis: CFJ_2010-01-06.zip.
- Our formalization is based on a Featherweight Java formalization by de Fraine that we adapted for our purposes: FJ_2010-01-06.zip.
- The proof assistant Coq can be downloaded elsewhere.