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

Notice that in this case the transformations rules are only the satisfaction of
the ClassToTable rule, since every source model element involved in the trans-
formation is reached from the class elements. The postcondition is the property
TableAtLeastOneCol , defined above.
The Coq proof assistant helps building proofs using tactics (inference rules).
We refer to the Coq documentation [13] for further details. The proof of this
property can be found in [20].
There are other properties which can be proved for this transformation, for
example the following OCL invariants.
context Table inv:
Table.allInstances()->isUnique(name)
context Table inv:
self.cols->isUnique(name)
The first one states that the name of a Table is unique. This holds because every
Class is transformed into a Table and because the name of a Class is unique.
The second property states that the name of a Column is unique within a Table ,
which holds because the name of an Attribute is unique within a Class .
The framework allows stating and proving more interesting properties which
involve both the source and target metamodels. In these cases the properties
cannot be expressed in OCL but can be expressed in Coq. For example, we
proved that the number of tables is equal to the number of persistent classes, in
Coq notation:
Definition ClassTableEqLen (ma : SimpleUML)
(mb : SimpleRDBMS) : Prop :=
length (filter isPersistent (MClass_classAllInstances ma)) =
length (MRelational_tableAllInstances mb).
The proof of this property is done by induction on both
MClass_classAllInstances and MRelational_tableAllInstances which are the
lists of all the instances of type Class and Table , respectively. This proof can also
be found in [20]. In a similar way, we can prove that the number of Column swithin
any Table is equal to the number of Attribute s of the corresponding Class .
6 Conclusions and Further Work
We have described a type-theoretic framework that allows the full formal ve-
rification of model transformations, at a metamodel level, and considering any
kind of transformations and properties. We have proposed a separation of duties
between developers and verifiers, based on a semi-automatic translation pro-
cess switching from the ATL to the CIC (Calculus of Inductive Constructions)
technical space as implemented on Coq. Within this framework, source and tar-
get metamodels ( MMa and MMb ) are represented as inductive types, and each