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

representation of models as explained below, but not on the inductive represen-
tation of the class. In the example above, the class UMLModelElement is defined in
Coq as follows.
Inductive UMLModelElement : Set :=
| Build_UMLModelElement (oid : nat) (name : string) (kind : string)
Notice the presence of the component named oid in the representation of the
UMLModelElement . This provides a means for identifying the actual objects that
are to be instances of the various classes, i.e. the oid s implement object identity,
beyond the constructor identity provided by the CIC.
In order to manipulate the components of the classes we define projections for
each attribute. They are trivially defined using pattern matching. As an example
we show just the projection of the attribute name of the UMLModelElement class.
Definition UMLModelElement_name (o : UMLModelElement) : string :=
match o with
| (Build_UMLModelElement _ n _) => n
end.
References. A reference represents an association between classes. It has a
name, a multiplicity and a type (of the element been referenced), and it may
have an opposite reference (bidirectional association). The natural choice for
representing associations is by lists of pairs of related elements. In order to opti-
mize navigability, the references of each class can be considered as components
of the corresponding type, in the same way as attributes. This results in using
mutually inductive types for representing related classes.
In the example below, the references from a Class to its Attribute sisrepre-
sented as a component within the constructor of the Class type.
Inductive Class : Set :=
| Build_Class ...
(attribute : list Attribute)
Now, if for a given class and reference an opposite reference exists, the elements of
the source class must form part of those of the target class and viceversa, i.e. the
objects of both classes are not well-founded. In general, this situation might arise
whenever several classes are mutually related through cycling associations and
we can characterize it as the admissibility of circularity in the actual construction
of (thereby infinite) objects. In these cases we seem to need co-inductive types,
as pointed out in [15,17]. However, taking such an approach forces us in the
general case to introduce all the mutually connected classes as mutually defined
co-inductive types. And then some disadvantages arise, concerning both the
correctness of the representation and its ease of use. The main problem is that
there will in general be cycles of references of classes of the model for which no
actual cycle at the level of object formation is intended to occur, even when some
other reference cycles in the same model allow the circularity of object formation.