Skip to content

Commit 0c556b9

Browse files
massimotisimassimotisi
authored
Merge pull request #107 from massimotisi/no-link
No link
2 parents 130b4e6 + 26e18b7 commit 0c556b9

36 files changed

+875
-1805
lines changed

‎.vscode/tasks.json

+2-2
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@
2525
"command": "java",
2626
"args": [
2727
"-cp",
28-
"./libs/fr.inria.atlanmod.coqtl.generators-all.jar",
28+
"./libs/coqtl-model-import-all.jar",
2929
"fr.inria.atlanmod.coqtl.ecore.core.EcoreGeneratorDriver",
3030
"${relativeFile}"
3131
],
@@ -37,7 +37,7 @@
3737
"command": "java",
3838
"args": [
3939
"-jar",
40-
"./libs/fr.inria.atlanmod.coqtl.generators-all.jar",
40+
"./libs/coqtl-model-import-all.jar",
4141
"${relativeFile}",
4242
"${input:metamodelPath}"
4343
],

‎README.md

+77-52
Original file line numberDiff line numberDiff line change
@@ -1,53 +1,78 @@
1-
Certifying an extensive rule-based model transformation engine for proof preservation
2-
=======
3-
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.
4-
5-
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.
6-
7-
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.
8-
9-
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.
10-
11-
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.
12-
13-
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.
14-
15-
Repository structure
16-
------
17-
* The CoqTL language and its examples are contained by [fr.inria.atlanmod.coqtl.coq](/fr.inria.atlanmod.coqtl.coq/)
18-
* language aspect is contained by [core](/fr.inria.atlanmod.coqtl.coq/core/), which modularized into:
19-
* Specification
20-
* [CoqTL engine specification](/fr.inria.atlanmod.coqtl.coq/core/Engine.v)
21-
* [CoqTL engine derived specification](/fr.inria.atlanmod.coqtl.coq/core/EngineProofs.v)
22-
* [Metamodel interface](/fr.inria.atlanmod.coqtl.coq/core/Metamodel.v)
23-
* [Model interface](/fr.inria.atlanmod.coqtl.coq/core/Model.v)
24-
* Implementation
25-
* [Abstract Syntax](/fr.inria.atlanmod.coqtl.coq/core/Syntax.v)
26-
* 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)
27-
* [Expression Evaluation](/fr.inria.atlanmod.coqtl.coq/core/Expressions.v)
28-
* Certification
29-
* 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)
30-
* examples is contained by [examples](/fr.inria.atlanmod.coqtl.coq/examples/):
31-
* [Class2Relational](/fr.inria.atlanmod.coqtl.coq/examples/Class2Relational/)
32-
* [HSM2FSM](/fr.inria.atlanmod.coqtl.coq/examples/HSM2FSM)
33-
* The extended CoqTL language specification includes
34-
* [CoqTL engine specification extension](/fr.inria.atlanmod.coqtl.coq/core/EngineTwoPhase.v)
35-
* [Extended Semantic functions](/fr.inria.atlanmod.coqtl.coq/core/twophases/TwoPhaseSemantics.v)
36-
* [Incremental Certification](/fr.inria.atlanmod.coqtl.coq/core/twophases/Certification_TwoPhaseSemantics.v)
37-
* The code generator from EMF metamodel/model to CoqTL is contained by [fr.inria.atlanmod.coqtl.generators](/fr.inria.atlanmod.coqtl.generators/) (experimental).
38-
39-
Compilation
40-
------
41-
See [compilation](https://github.com/atlanmod/CoqTL/wiki/Compiling-CoqTL) on the wiki.
42-
43-
Issues
44-
------
45-
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:
46-
47-
> Massimo Tisi: massimo.tisi@imt-atlantique.fr
48-
49-
> Zheng Cheng: zheng.cheng@inria.fr
50-
51-
License
52-
------
1+
# CoqTL
2+
3+
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.
4+
5+
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).
6+
7+
```coq
8+
Definition Moore2Mealy :=
9+
transformation
10+
[
11+
rule "state"
12+
from [Moore.StateClass]
13+
to [
14+
elem "s'"
15+
(fun _ _ s => BuildState (Moore.State_getName s)) nil
16+
];
17+
18+
rule "transition"
19+
from [Moore.TransitionClass]
20+
to [
21+
elem "t'"
22+
(fun _ m t =>
23+
BuildTransition
24+
(Moore.Transition_getInput t)
25+
(value (option_map Moore.State_getOutput (Moore.Transition_getTarget t m))))
26+
[
27+
link
28+
(fun tls _ m tr tr' =>
29+
maybeBuildTransitionSource tr'
30+
(maybeResolve tls m "s'" Mealy.StateClass
31+
(maybeSingleton (Moore.Transition_getSourceObject tr m))));
32+
link
33+
(fun tls _ m tr tr' =>
34+
maybeBuildTransitionTarget tr'
35+
(maybeResolve tls m "s'" Mealy.StateClass
36+
(maybeSingleton (Moore.Transition_getTargetObject tr m))))
37+
]
38+
]
39+
].
40+
```
41+
42+
## Organization of the repository
43+
44+
* [core/](https://github.com/atlanmod/coqtl/tree/master/core) - source files of the CoqTL engine.
45+
* [transformations/](https://github.com/atlanmod/coqtl/tree/master/transformations) - sample CoqTL transformations and associated proofs.
46+
* [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.
47+
* [.vscode/](https://github.com/atlanmod/coqtl/tree/master/.vscode) - convenience tasks for vscode: `make`, `clean`, `ecore2v`, `xmi2v`.
48+
49+
## Installation
50+
51+
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.
52+
53+
To install CoqTL:
54+
```
55+
git clone https://github.com/atlanmod/coqtl.git
56+
cd coqtl
57+
./compile.sh
58+
```
59+
60+
## Publications
61+
62+
Here are the publications describing CoqTL and the pointer to the version of CoqTL they refer to.
63+
64+
* 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)
65+
* 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)
66+
* 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)
67+
* Zheng Cheng, Massimo Tisi. Deep Specification and Proof Preservation for the CoqTL Transformation Language. [[git]](https://github.com/atlanmod/CoqTL/tree/948eb94)
68+
69+
## Questions and discussion
70+
71+
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:
72+
73+
* Massimo Tisi: massimo.tisi@imt-atlantique.fr
74+
* Zheng Cheng: zheng.cheng@inria.fr
75+
76+
## License
77+
5378
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

+7-11
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ core/modeling/properties/ModelingAdditivityRuleExt.v
5959
#core/modeling/iteratetraces/IterateTracesCertification.v
6060

6161
#core/modeling/byrule/ByRuleSemantics.v
62-
#core/modeling/byrule/Certification_ByRuleSemantics.v
62+
#core/modeling/byrule/Certification_ByRuleSemantics.v\
6363

6464
transformations/Class2Relational/ClassMetamodel.v
6565
transformations/Class2Relational/RelationalMetamodel.v
@@ -75,8 +75,6 @@ transformations/Class2Relational/theorems/Attribute_name_preservation.v
7575
transformations/Class2Relational/theorems/Column_name_uniqueness.v
7676
transformations/Class2Relational/theorems/Relational_resolve_spec.v
7777

78-
79-
8078
transformations/TT2BDD/TT.v
8179
transformations/TT2BDD/BDD.v
8280
transformations/TT2BDD/TT2BDDAbstract.v
@@ -95,14 +93,12 @@ transformations/RSS2ATOM/tests/Exemple1ATOM.v
9593
transformations/DBLP/DBLP.v
9694
transformations/IMDB/MOVIES.v
9795

98-
core/test/iExpressions.v
99-
core/test/iSyntax.v
100-
core/test/iSemantics.v
101-
core/test/iSyntaxCertification.v
102-
#core/test/iCertification.v
103-
core/test/properties/iConfluence.v
104-
10596
transformations/Families2Persons/tests/sampleFamilies.v
10697
transformations/Families2Persons/Families.v
10798
transformations/Families2Persons/Persons.v
108-
transformations/Families2Persons/Families2Persons.v
99+
transformations/Families2Persons/Families2Persons.v
100+
101+
transformations/Moore2Mealy/Moore.v
102+
transformations/Moore2Mealy/Mealy.v
103+
transformations/Moore2Mealy/Moore2Mealy.v
104+
transformations/Moore2Mealy/tests/sampleMoore.v

‎core/properties/Confluence.v

+25-2
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,14 @@ Require Import FunctionalExtensionality.
1616
(** * Confluence *)
1717
(*************************************************************)
1818

19+
20+
Definition well_form {tc: TransformationConfiguration} tr :=
21+
forall r1 r2 sm sp,
22+
In r1 tr /\ In r2 tr/\
23+
matchRuleOnPattern r1 sm sp = true /\
24+
matchRuleOnPattern r2 sm sp = true ->
25+
r1 = r2.
26+
1927
(* Multiset semantics: we think that the list of rules represents a multiset/bag*)
2028
(* Definition Transformation_equiv {tc: TransformationConfiguration} (t1 t2: Transformation) :=
2129
forall (r:Rule),
@@ -29,8 +37,23 @@ Require Import FunctionalExtensionality.
2937
(* Set semantics: we think that the list of rules represents a set (we don't allow two rules to have the same name)*)
3038
Definition Transformation_equiv {tc: TransformationConfiguration} (t1 t2: Transformation) :=
3139
(Transformation_getArity t1 = Transformation_getArity t2) /\
32-
forall (r:Rule),
33-
In r (Transformation_getRules t1) <-> In r (Transformation_getRules t2).
40+
set_eq (Transformation_getRules t1) (Transformation_getRules t2) /\
41+
well_form (Transformation_getRules t1) /\
42+
well_form (Transformation_getRules t2).
43+
44+
Lemma trace_eq {tc: TransformationConfiguration} :
45+
forall t1 t2 sm,
46+
Transformation_equiv t1 t2 ->
47+
(trace t1 sm) = (trace t2 sm).
48+
Proof.
49+
intros.
50+
destruct t1.
51+
destruct t2.
52+
induction l.
53+
- unfold Transformation_equiv in H.
54+
admit.
55+
Admitted.
56+
3457

3558
Definition TargetModel_equiv {tc: TransformationConfiguration} (m1 m2: TargetModel) :=
3659
forall (e: TargetModelElement) (l: TargetModelLink),

0 commit comments

Comments
 (0)