This repository contains an ongoing specification of the theory of Software Product Line Refinement using the Coq proof assistant, porting from the formalization already made in PVS. The formalization was split into modules and these were included in different files. We give a brief description of these files below.
- name.v: Here, we define configuration in Name Module as a set of feature names, specifically, a Name set, where Name is an uninterpreted type.
- form.v: The form.v file contains the Form Module where a formula is declared as a new set of data values - in this case an enumerated type.
- feature_model.v: In this file, we represent an FM as a pair of features and formulae, where features is a set of feature names and formulae is a set of formulas.
- decidability.v: In Coq, dealing with lists requires that the types of elements used in these lists be decidable. In this file, we add axioms that all elements of type Name, Formula, and Configuration are the same or different, making their type decidable.
- formula_theory.v: This file contains definitions of functions and lemmas that guarantee properties involving the Formula type.
- feature_model_semantics.v: This file contains definitions of functions, lemmas and theorems that provide a guarantee of properties involving the FM type.
- assets.v: In a product line, we specify and implement features with reusable assets. This file contains the theory of Assets.
- asset_mapping.v: This file contains the theory of Asset Mapping - mappings from asset names to actual assets.
- ck_trans.v: We must relate features related to assets, whether code or other kinds of assets that specify or realize features. The CK specifies this relation. We can express the CK in different ways. ck_trans.v contains a more advanced CK notion, that associates feature expressions with transformations over assets.
- maps.v: For AM we need a Map structure that allows the mapping of a feature name to a real artifact, so we chose to formalize a theory that deals with this structure that is contained in this file.
- spl_refinement.v: specify the general theory of LPS refinement.
Create an executable file configure.sh: coq_makefile -f _CoqProject -o Makefile To compile the project, run: make