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

Fig. 3. UML metamodel and RDBMS metamodel
languages. For this reason, it will be used in the following sections in order to
exemplify the verification process steps.
3 Formalization of Metamodels and Models
In this section we show how to represent metamodels and models in the CIC.
For metamodels we show how every KM3 construction is translated into Coq no-
tation, using the UML metamodel of the example mentioned in Figure 3 above.
The whole translation has been defined and implemented as an ATL transfor-
mation. For space reasons we cannot include it here but it can be found in [20].
Data Types and Enumerations. Coq supports primitive data types like
strings, booleans and natural numbers, among others, via libraries equipped
with many useful functions. This is enough to represent ATL primitive types.
In ATL it is also possible to define enumeration types and use them to define
class attributes. Enumeration types are directly represented in Coq as inductive
types with one constructor for each enumeration literal.
Classes and Attributes. A class has attributes. An attribute has a name,
a multiplicity and a type. We represent classes using inductive types. For each
class its attributes are represented as components of the corresponding type by
means of a constructor which has its attributes as parameters. A class can be
abstract, meaning that there are no direct instances of it. This impacts on the