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

Hence, we have in general that some of the classes involved in the represented
metamodel will not be intended to actually contain infinite structures, namely
those participating in references in which no actual cycle at the level of objects
is admissible. But even in such cases, the definition of the classes as co-inductive
allows them to contain infinite structures. This compromises the correctness of
the representation in at least two respects: first, circularity at the level of objects
cannot be prevented at syntax (type) level and secondly, the termination of
functions on these types cannot be enforced. Although these restrictions could
be imposed on the co-inductive definition of the model, that would lead to a
representation too awkward to manage in practice.
We therefore decide to use only inductive types. This is enough for the cases
in which no circularity at the level of objects is to be allowed, since the well-
foundedness of the latter is imposed by construction. More precisely, we represent
directly only unidirectional references, using mutually inductive types whenever
circularity at the level of the objects is not allowed in the metamodel. If, on the
contrary, we should have to allow for such circularity then we use the first repre-
sentation mentioned above, i.e. associations as list of pairs of related elements.
This procedure has as a particular case that of the bi-directional associations.
Deciding which references are represented in either way in an optimal way
depends on how the model elements are used in the transformation. This is a
point in which, although possible, the automation of the representation of the
metamodel might not be desirable. In the implemented translation of [20] the
references of each class are represented as components of the corresponding type,
and circularity must be manually “cut” by the human verifier.
Multiplicities. Attributes and references have multiplicities. Each multiplicity
has a lower and an upper value and multiplicity 1 is assumed if none is declared.
When representing references as components, multiplicity reflects itself in the
type of the component. This is the same as in the case of attributes. Multiplicity
0..1 is represented with the option type constructor, which has constructors
None representing no element and Some x for elements x in the original type. If
the upper multiplicity value is greater than 1 , the multiplicity is represented
with a (possibly ordered) list type. Multiplicity 1 corresponds just to the type
of the component.
In the example we have the following multiplicities.
[1-1] -- name : string
[0-*] -- attribute : list Attribute
When representing associations as list of pairs of related elements, multiplicity is
enforced by explicit constraints on the number of pairs allowed for each element
of the participant classes.
Generalization and Abstract Classes. In ATL it is also possible to define
generalization relations between classes. The CIC does not have a notion of
subtyping between types, unlike [15]. We represent this notion as references
from the subtypes to it(s) supertype(s). With this representation we can easily