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

rule AttributeToColumn{
from a : SimpleUML!Attribute ()
to c : SimpleRDBMS!Column (
name <- a.name,
type <- a.type.primitiveTypeToStringType
)
}
We represent this matched rule as follows:
Definition AttributeToColumn (c : Class) (t : Table) : Prop :=
(forall atr:Attribute, In atr (Class_attribute c) ->
exists! col:Column, In col (Table_column t) /\
RModelElement_name (Column_super col) = Attribute_name atr /\
Column_type col = primitiveTypeToStringType
(PrimitiveDataType_name (Attribute_type atr)))
/\
(forall col:Column, In col (Table_column t) ->
exists! atr:Attribute, In atr (Class_attribute c) /\
RModelElement_name (Column_super col) = Attribute_name atr /\
Column_type col = primitiveTypeToStringType
(PrimitiveDataType_name (Attribute_type atr))).
Notice that the relation is described in both directions, and also that there is
only one source and target elements for which the proposition holds.
For the sake of completeness we present the other matched rule that trans-
forms every persistent Class into a Table of the database. The name of the table
must be the same as the class, and the columns of the table will be the trans-
formation of the attributes of the class which is performed by the matched rule
AttributeToColumn .
rule ClassToTable{
from c : SimpleUML!Class (c.kind = 'Persistent')
to t : SimpleRDBMS!Table (
name <- c.name,
cols <- c.attribute
)
}
This matched rule is represented in Coq as follows.
Definition ClassToTable (ma : SimpleUML) (mb : SimpleRDBMS) : Prop :=
(forall c:Class, In c (MClass_classAllInstances ma) /\
Class_kind c = "Persistent" ->
exists! t:Table, In t (MRelational_tableAllInstances mb) /\
Class_name c = Table_name t /\
AttributeToColumn c t)
/\