A machine-checked model of safe composition

ABSTRACT

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 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.

REFERENCES

• 1: Davide Ancona , Ferruccio Damiani , Sophia Drossopoulou , Elena Zucca, Polymorphic bytecode: compositional compilation for Java-like languages, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.26-37, January 12-14, 2005, Long Beach, California, USA
• 2: S. Apel and D. Hutchins. An overview of the gDEEP calculus. Technical Report Technical Report MIP-0712, Department of Informatics and Mathematics, University of Passau, November 2007.
• 3: Sven Apel , Christian Kästner , Christian Lengauer, Feature featherweight java: a calculus for feature-oriented programming and stepwise refinement, Proceedings of the 7th international conference on Generative programming and component engineering, October 19-23, 2008, Nashville, TN, USA [doi>10.1145/1449913.1449931]
• 4: Don Batory, Feature-Oriented Programming and the AHEAD Tool Suite, Proceedings of the 26th International Conference on Software Engineering, p.702-703, May 23-28, 2004
• 5: D. Batory. Feature models, grammars, and propositional formulas. In Software Product Lines Conference, LNCS 3714, pages 7--20. Springer, 2005.
• 6: Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
• 7: Krzysztof Czarnecki , Krzysztof Pietroszek, Verifying feature-based model templates against well-formedness OCL constraints, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA [doi>10.1145/1173706.1173738]
• 8: Benjamin Delaware , William Cook , Don Batory, A machine-checked model of safe composition, Proceedings of the 2009 workshop on Foundations of aspect-oriented languages, March 02-02, 2009, Charlottesville, Virginia, USA [doi>10.1145/1509837.1509846]
• 9: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 10: R. Prieto-Diaz and J. Neighbors. Module interconnection languages: A survey. Technical report, University of California at Irvine, August 1982. ICS Technical Report 189.
• 11: Peter Sewell , Francesco Zappa Nardelli , Scott Owens , Gilles Peskine , Thomas Ridge , Susmit Sarkar , Rok Strniša, Ott: effective tool support for the working semanticist, Proceedings of the 12th ACM SIGPLAN international conference on Functional programming, October 01-03, 2007, Freiburg, Germany
• 12: Rok Strniša , Peter Sewell , Matthew Parkinson, The java module system: core design and semantic definition, Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 13: Sahil Thaker , Don Batory , David Kitchin , William Cook, Safe composition of product lines, Proceedings of the 6th international conference on Generative programming and component engineering, October 01-03, 2007, Salzburg, Austria [doi>10.1145/1289971.1289989]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Design, Languages

Keywords:
feature model, product lines, type safety