Merge pull request #107 from massimotisi/no-link

No link

.vscode/tasks.json

@@ -25,7 +25,7 @@
             "command": "java",
             "args": [
                 "-cp",
-                "./libs/fr.inria.atlanmod.coqtl.generators-all.jar",
+                "./libs/coqtl-model-import-all.jar",
                 "fr.inria.atlanmod.coqtl.ecore.core.EcoreGeneratorDriver",
                 "${relativeFile}"
             ],
@@ -37,7 +37,7 @@
             "command": "java",
             "args": [
                 "-jar",
-                "./libs/fr.inria.atlanmod.coqtl.generators-all.jar",
+                "./libs/coqtl-model-import-all.jar",
                 "${relativeFile}",
                 "${input:metamodelPath}"
             ],

README.md

@@ -1,53 +1,78 @@
-Certifying an extensive rule-based model transformation engine for proof preservation
-=======
-Executable engines for relational model-transformation languages evolve continuously because of language extension, performance improvement and bug fixes. While new versions generally change the engine semantics, end-users expect to get backward-compatibility guarantees, so that existing transformations do not need to be adapted at every engine update.
-
-The CoqTL model-transformation language allows users to define model transformations, theorems on their behavior and machine-checked proofs of these theorems in Coq. Backward-compatibility for CoqTL involves also the preservation of these proofs. However, proof preservation is challenging, as proofs are easily broken even by small refactorings of the code they verify.
-
-In this paper we present the solution we designed for the evolution of CoqTL, and by extension, of rule-based transformation engines. We provide a deep specification of the transformation engine, including a set of theorems that must hold against the engine implementation. Then, at each milestone in the engine development, we certify the new version of the engine against this specification, by providing proofs of the impacted theorems. The certification formally guarantees end-users that all the proofs they write using the provided theorems will be preserved through engine updates.
-
-We illustrate the structure of the deep specification theorems, we produce a machine-checked certification of three versions of CoqTL against it, and we show examples of user theorems that leverage this specification and are thus preserved through the updates.
-
-Our [previous work](https://dl.acm.org/doi/10.1145/3365438.3410949) focuses on proof preservation in the presence of engine implementation evolution. The evolved implementations has to be certified against the same deep specfication of CoqTL for users' stable proofs.
-
-Such deep specification is just another kind of software, which is prone to evolution. Therefore, in this branch, we demonstrate how to address the problem of proof preservation in the presence of deep specification evolution. 
-
-Repository structure
-------
-* The CoqTL language and its examples are contained by [fr.inria.atlanmod.coqtl.coq](/fr.inria.atlanmod.coqtl.coq/)
-  * language aspect is contained by [core](/fr.inria.atlanmod.coqtl.coq/core/), which modularized into:
-    * Specification
-      * [CoqTL engine specification](/fr.inria.atlanmod.coqtl.coq/core/Engine.v)
-      * [CoqTL engine derived specification](/fr.inria.atlanmod.coqtl.coq/core/EngineProofs.v)
-      * [Metamodel interface](/fr.inria.atlanmod.coqtl.coq/core/Metamodel.v)
-      * [Model interface](/fr.inria.atlanmod.coqtl.coq/core/Model.v)
-    * Implementation
-      * [Abstract Syntax](/fr.inria.atlanmod.coqtl.coq/core/Syntax.v)
-      * Semantic functions [(v1)](/fr.inria.atlanmod.coqtl.coq/core/Semantics.v) [(v2)](/fr.inria.atlanmod.coqtl.coq/core/Semantics_v2.v) [(v3)](/fr.inria.atlanmod.coqtl.coq/core/Semantics_v3.v)
-      * [Expression Evaluation](/fr.inria.atlanmod.coqtl.coq/core/Expressions.v)
-    * Certification 
-      * Implementation against specification [(v1)](/fr.inria.atlanmod.coqtl.coq/core/Certification.v) [(v2)](/fr.inria.atlanmod.coqtl.coq/core/Certification_v2.v) [(v3)](/fr.inria.atlanmod.coqtl.coq/core/Certification_v3.v)
-  * examples is contained by [examples](/fr.inria.atlanmod.coqtl.coq/examples/):
-    * [Class2Relational](/fr.inria.atlanmod.coqtl.coq/examples/Class2Relational/)
-    * [HSM2FSM](/fr.inria.atlanmod.coqtl.coq/examples/HSM2FSM)
-* The extended CoqTL language specification includes
-  * [CoqTL engine specification extension](/fr.inria.atlanmod.coqtl.coq/core/EngineTwoPhase.v)
-  * [Extended Semantic functions](/fr.inria.atlanmod.coqtl.coq/core/twophases/TwoPhaseSemantics.v)
-  * [Incremental Certification](/fr.inria.atlanmod.coqtl.coq/core/twophases/Certification_TwoPhaseSemantics.v)
-* The code generator from EMF metamodel/model to CoqTL is contained by [fr.inria.atlanmod.coqtl.generators](/fr.inria.atlanmod.coqtl.generators/) (experimental).
-
-Compilation
-------
-See [compilation](https://github.com/atlanmod/CoqTL/wiki/Compiling-CoqTL) on the wiki.
-
-Issues
-------
-If you experience issues installing or using CoqTL, you can submit an issue on [github](https://github.com/atlanmod/CoqTL/issues) or contact us at:
-
-> Massimo Tisi: [email protected]
-
-> Zheng Cheng: [email protected]
-
-License
-------
+# CoqTL
+
+CoqTL is an internal language in Coq, for writing rule-based model- and graph- transformations. The language is associated with a library to simplify proving transformation correctness in Coq. 
+
+For instance, the following CoqTL code transforms [Moore machines](https://en.wikipedia.org/wiki/Moore_machine) into [Mealy machines](https://en.wikipedia.org/wiki/Mealy_machine) (if we disregard the first output symbol of the Moore machine). The full transformation, including type annotations, is available [here](./transformations/Moore2Mealy/Moore2Mealy.v).
+
+```coq
+Definition Moore2Mealy :=
+  transformation
+  [
+    rule "state"
+    from [Moore.StateClass]
+    to [
+      elem "s'"
+        (fun _ _ s => BuildState (Moore.State_getName s)) nil
+    ];
+    
+    rule "transition"
+    from [Moore.TransitionClass]
+    to [
+      elem "t'"
+        (fun _ m t => 
+          BuildTransition 
+            (Moore.Transition_getInput t)
+            (value (option_map Moore.State_getOutput (Moore.Transition_getTarget t m))))
+        [
+          link
+            (fun tls _ m tr tr' =>
+              maybeBuildTransitionSource tr'
+                (maybeResolve tls m "s'" Mealy.StateClass 
+                  (maybeSingleton (Moore.Transition_getSourceObject tr m))));
+          link 
+            (fun tls _ m tr tr' =>
+              maybeBuildTransitionTarget tr'
+                (maybeResolve tls m "s'" Mealy.StateClass 
+                  (maybeSingleton (Moore.Transition_getTargetObject tr m))))
+        ]
+  ]
+].
+```
+
+## Organization of the repository 
+
+* [core/](https://github.com/atlanmod/coqtl/tree/master/core) - source files of the CoqTL engine.
+* [transformations/](https://github.com/atlanmod/coqtl/tree/master/transformations) - sample CoqTL transformations and associated proofs.
+* [libs/](https://github.com/atlanmod/coqtl/tree/master/libs) - an importer that translates `ecore` metamodels and `xmi` models into Coq. While not necessary to run CoqTL, the sources of the importer are in the [coqtl-model-import](https://github.com/atlanmod/coqtl-model-import) repository.
+* [.vscode/](https://github.com/atlanmod/coqtl/tree/master/.vscode) - convenience tasks for vscode: `make`, `clean`, `ecore2v`,  `xmi2v`.
+
+## Installation
+
+CoqTL requires a working installation of [Coq](https://coq.inria.fr/) (`coqc` and `coq_makefile` in the path). It is tested under Coq 8.15.0.
+
+To install CoqTL:
+```
+git clone https://github.com/atlanmod/coqtl.git
+cd coqtl
+./compile.sh
+```
+
+## Publications
+
+Here are the publications describing CoqTL and the pointer to the version of CoqTL they refer to. 
+
+* Massimo Tisi, Zheng Cheng. CoqTL: an Internal DSL for Model Transformation in Coq. ICMT'2018. [[pdf]](https://hal.inria.fr/hal-01828344/document) [[git]](https://github.com/atlanmod/CoqTL/tree/eee344e)
+* Zheng Cheng, Massimo Tisi, Rémi Douence. CoqTL: A Coq DSL for Rule-Based Model Transformation. SOSYM'2019. [[pdf]](https://hal.archives-ouvertes.fr/hal-02333564/document) [[git]](https://github.com/atlanmod/CoqTL/tree/eee344e)
+* Zheng Cheng, Massimo Tisi, Joachim Hotonnier. Certifying a Rule-Based Model Transformation Engine for Proof Preservation. MODELS'2020. [[pdf]](https://hal.inria.fr/hal-02907622/document) [[git]](https://github.com/atlanmod/CoqTL/tree/2a8cea5)
+* Zheng Cheng, Massimo Tisi. Deep Specification and Proof Preservation for the CoqTL Transformation Language. [[git]](https://github.com/atlanmod/CoqTL/tree/948eb94)
+
+## Questions and discussion
+
+If you experience issues installing or using CoqTL, you can submit an issue on [github](https://github.com/atlanmod/coqtl/issues) or contact us at:
+
+* Massimo Tisi: [email protected]
+* Zheng Cheng: [email protected]
+
+## License
+
 CoqTL itself is licensed under Eclipse Public License (v2). See LICENSE.md in the root directory for details. Third party libraries are under independent licenses, see their source files for details.

_CoqProject

@@ -59,7 +59,7 @@ core/modeling/properties/ModelingAdditivityRuleExt.v
 #core/modeling/iteratetraces/IterateTracesCertification.v
 
 #core/modeling/byrule/ByRuleSemantics.v
-#core/modeling/byrule/Certification_ByRuleSemantics.v
+#core/modeling/byrule/Certification_ByRuleSemantics.v\
 
 transformations/Class2Relational/ClassMetamodel.v
 transformations/Class2Relational/RelationalMetamodel.v
@@ -75,8 +75,6 @@ transformations/Class2Relational/theorems/Attribute_name_preservation.v
 transformations/Class2Relational/theorems/Column_name_uniqueness.v
 transformations/Class2Relational/theorems/Relational_resolve_spec.v
 
-
-
 transformations/TT2BDD/TT.v
 transformations/TT2BDD/BDD.v
 transformations/TT2BDD/TT2BDDAbstract.v
@@ -95,14 +93,12 @@ transformations/RSS2ATOM/tests/Exemple1ATOM.v
 transformations/DBLP/DBLP.v
 transformations/IMDB/MOVIES.v
 
-core/test/iExpressions.v
-core/test/iSyntax.v
-core/test/iSemantics.v
-core/test/iSyntaxCertification.v
-#core/test/iCertification.v
-core/test/properties/iConfluence.v
-
 transformations/Families2Persons/tests/sampleFamilies.v
 transformations/Families2Persons/Families.v
 transformations/Families2Persons/Persons.v
-transformations/Families2Persons/Families2Persons.v
+transformations/Families2Persons/Families2Persons.v
+
+transformations/Moore2Mealy/Moore.v
+transformations/Moore2Mealy/Mealy.v
+transformations/Moore2Mealy/Moore2Mealy.v
+transformations/Moore2Mealy/tests/sampleMoore.v

core/properties/Confluence.v

@@ -16,6 +16,14 @@ Require Import FunctionalExtensionality.
 (** * Confluence                                             *)
 (*************************************************************)
 
+
+Definition well_form  {tc: TransformationConfiguration} tr :=
+  forall r1 r2 sm sp, 
+    In r1 tr /\ In r2 tr/\
+    matchRuleOnPattern r1 sm sp = true /\
+    matchRuleOnPattern r2 sm sp = true ->
+      r1 = r2.
+
 (* Multiset semantics: we think that the list of rules represents a multiset/bag*)
 (* Definition Transformation_equiv {tc: TransformationConfiguration} (t1 t2: Transformation) := 
   forall (r:Rule),
@@ -29,8 +37,23 @@ Require Import FunctionalExtensionality.
 (* Set semantics: we think that the list of rules represents a set (we don't allow two rules to have the same name)*)
 Definition Transformation_equiv {tc: TransformationConfiguration} (t1 t2: Transformation) := 
   (Transformation_getArity t1 = Transformation_getArity t2) /\ 
-  forall (r:Rule),
-  In r (Transformation_getRules t1) <-> In r (Transformation_getRules t2).
+  set_eq (Transformation_getRules t1) (Transformation_getRules t2) /\
+  well_form (Transformation_getRules t1) /\ 
+  well_form (Transformation_getRules t2).
+
+Lemma trace_eq {tc: TransformationConfiguration} :
+  forall  t1 t2 sm,
+   Transformation_equiv t1 t2 ->
+   (trace t1 sm) = (trace t2 sm).
+Proof.
+  intros.
+  destruct t1.
+  destruct t2.
+  induction l.
+  - unfold Transformation_equiv in H.
+    admit.
+Admitted. 
+
 
 Definition TargetModel_equiv {tc: TransformationConfiguration} (m1 m2: TargetModel) :=
   forall (e: TargetModelElement) (l: TargetModelLink),