View on GitHub


Encoding QVT-R Transformations in Coq

Download this project as a .zip file Download this project as a tar.gz file

QVTr2Coq is a systematic embedding of the QVT Relations (QVT-R) transformation language in Constructive Type Theory (CTT) as implemented by the Coq proof assistant. The framework allows to manually construct and verify implementations of QVT-R transformation programs in Coq. Verified transformations can be used as a test oracle, i.e., for testing existing QVT-R transformation tools if they are in compliance with standardised semantics.


QVT-R semantics are complex and not well understood. At the present time, QVT-R semantics are implicitly modeled in tooling, but we cannot be sure if interpreters do what we expect the QVT-R specification to do.

The overall approach

One solution to this problem is to build a test oracle that can be utilised to semi-automatically construct reference implementations of individual transformations to test QVT-R execution engines. Because of the problem-oriented nature of the QVT-R language, there is a gap between specification and the actual interpretation of QVT-R programs. To ensure that a model transformation specified in QVT-R results in the intended behaviour, it must be tested.

For demonstration, we used the framework to generate a CTT specification from the well-known UML2RDBMS example transformation. The specification is then verified in a manual step and an implementation is extracted.


The project consists of three Xtend-based model transformations for encoding QVT-R in Coq,

Additionally, we provide a verified implementation of UML2RDBMS as an example use case.


QVTr2Coq runs on the Eclipse Modeling Tools. The following steps assume a fresh installation of Eclipse.

  1. Download Eclipse Modeling Tools 4.3 (Kepler) (Kepler) and launch it;

  2. Install through menu Help > Install Modeling Components... Eclipse Xtext 2.5+ of the Model Development Tools (MDT) project;

  3. Choose Help > Install New Software... to install Eclipse QVTd 0.10+ of the Model to Model Transformation (MMT) project, update site;

  4. Download QVTr2Coq and import contained projects through File > Import > Existing Projects into Workspace… into your Eclipse workspace.

You are ready to use the code generator to produce Coq specifications from QVT-R programs, Ecore metamodels and instances thereof. To do so, use the run configuration Generate Coq Code. The transformation searches in subfolder model for files ending with .qvtr, .ecore, and .xmi. Resulting Coq specifications (.v files) are placed into src-gen.

To run a proof on generated Coq files, you need to install the Coq proof assistant, version 8.4 or higher. We recommend to download Coq bundled with CoqIDE.

Example Proof

Folder model already contains QVT-R implementations together with their Ecore metamodels. One of them is the example transformation UML2RDBMS that maps UML to RDBMS models. It is the same version as that provided by the Eclipse QVTd project.

In folder proof you will find the generated Coq specification of UML2RDBMS, complemented by an example proof and a Haskell program, UML2RDBMS.hs, which has been extracted from the proof. Several of the lemmas are general enough to be used in your own proofs, these are contained in package ListHelpers.v.



This research is a cooperation between King's College London (KCL) and Karlsruhe Institute of Technology (KIT). Work has partly been funded by the German Research Foundation (DFG) under grant No. RE 1674/5-1: Model-Driven Methods and Tools for Performance Prediction and Capacity Planning of Component-Based Software Systems (codenamed FERDINAND project) and the Priority Programme SPP 1593: Design For Future – Managed Software Evolution (more specifically, the ADVERT project).