A Type-Theoretic Framework for Certified Model Transformations - Formal Methods: Foundations and Applications - page 120

navigate from a subclass to a property of it superclass. Notice that when a
generalization exists, the oid s are located only at the topmost supertype.
In the example, the PrimitiveDataType class has a reference to its supertype
UMLModelElement .
PrimitiveDataType : Set :=
| Build_PrimitiveDataType (super : UMLModelElement)
The whole UML metamodel in Figure 3 is defined in Coq as follows.
Inductive UMLModelElement : Set :=
| Build_UMLModelElement (oid : nat) (name : string) (kind : string).
Inductive Class : Set :=
| Build_Class (super : UMLModelElement)
(attribute : list Attribute)
with
Attribute : Set :=
| Build_Attribute (super : UMLModelElement)
(type : PrimitiveDataType)
with
PrimitiveDataType : Set :=
| Build_PrimitiveDataType (super : UMLModelElement).
Finally, a model that conforms to a metamodel is represented as a record contain-
ing the lists of instances of each non-abstract metamodel element, as suggested
in [21]. In the example a model conforming to the UML metamodel would be a
record of the following type.
Record SimpleUML : Set :=
mkSimpleUML {classAllInstances : list Class;
primitiveDataTypeAllInstances : list PrimitiveDataType;
attributeAllInstances : list Attribute
}.
In the example every element in the model is reachable from the Class instances,
so the record can in fact be reduced to just a list of classes.
4 Translation of the Model Transformation
We show next how ATL constructs can be translated into Coq notation, using
the example transformation in Section 2.3. Briefly, every ATL declarative trans-
formation rule is transformed into a logical proposition, and helper (auxiliary)
functions are translated into Coq functions. Not every ATL construct is consid-
ered since some of them (e.g. modules) are not relevant for our study. The whole
transformation of the example can be found in [20].