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

(forall t:Table, In t (MRelational_tableAllInstances mb) ->
exists! c:Class, In c (MClass_classAllInstances ma) /\
Class_kind c = "Persistent" /\
Class_name c = Table_name t /\
AttributeToColumn c t).
5 Verification of Properties
OCL invariants of both source and target metamodels are translated into propo-
sitions in the CIC. This, at a large measure, can be done automatically follow-
ing the ideas presented in [22]. The desired properties of the transformation are
specified in the CIC by the verifier using the full potential of the logic. These pro-
perties will in general establish relations between (any instances of) the source
and target metamodel connected by the transformation.
A simple property of the example transformation is that the length of the
Column swithina Table must be grater than zero. This can be written in OCL as
follows.
context Table inv:
self.column->length() > 0
In Coq, this property can be expressed as follows.
Definition TableAtLeastOneCol (model : SimpleRDBMS) : Prop :=
forall t:Table, (In t (MRelational_tableAllInstances model)) ->
length (Table_column t) > 0.
This property holds by the fact that every Attribute is transformed into a Column
and that every Class has at least one Attribute . This information is given in the
transformation rules and in the source invariants, respectively.
The invariants of the target metamodel and any other desired properties of
the transformation ( Post ) are interactively verified in Coq by assuming that the
invariants of the source metamodel ( Pre ), and the transformation rules ( TRules )
hold. In this way, the correctness proposition becomes:
∀ Ma:MMa. (Pre(Ma) →∀ Mb:MMb. (TRules(Ma,Mb) → Post(Ma,Mb)))
In the example, the Coq lemma to prove is as follows.
Definition Post (ma : SimpleUML) (mb : SimpleRDBMS) : Prop :=
TableAtLeastOneCol mb.
Definition TRules (ma : SimpleUML) (mb : SimpleRDBMS) : Prop :=
ClassToTable ma mb.
Lemma Cert_Class2Relational:
forall ma:SimpleUML, Pre ma -> forall mb:SimpleRDBMS, TRules ma mb
-> Post ma mb.