Formal methods are increasingly used in software engineering. They ofer a formal frame that guarentees the correctness of developments. However, they use complex notations that might be dificult to understand for unaccustomed users. It thus becomes interesting to formally specify the core components of a language, implement a provably correct development, and manipulate its components in a graphical/textual editor. This paper constitutes a first step towards using Model Driven Engineering (MDE) technology in an interactive proof development. It presents a transformation process from functional data structures, commonly used in proof assistants, to Ecore Models. The transformation is based on an MDE methodology. The resulting meta-models are used to generate graphical or textual editors. We will take an example to illustrate our approach: a simple domain specific language. This guiding example is a Java-like language enriched with assertions.
Domain Specific Languages (DSL) have conquered many diferent aspects of
computer science. They are used in diferent fields such as aerospace,
webservices, multi-media, etc. [
Interactive proof assistants such as Coq [
In order to improve the user interface for interacting with a DSL, we aim at a textual or graphical concrete syntax as provided, for example, by the Eclipse Xtext or GMF environments. Frequent changes of the DSL during the design phase make it necessary to adapt this interface easily and to re-generate it automatically, as far as possible.
Xtext
DSL Textual Syntax
MDE
This paper studies the interplay of these formalisms (see Figure 1), and thus
constitutes a first step towards using Model Driven Engineering (MDE) [
Section 2 constitutes the technical core of the article; it describes a translation from data models in the functional programming world, used in verification environments, to meta models in Ecore: the core language of the Eclipse Modeling Framework. We illustrate the methodology in Section 3 with a case study. In Section 4 we compare our work to other approaches, before concluding in Section 5 with perspectives of further work.
In this part, we present in detail the translation process from functional data types to meta-models. We start in Section 2.1 by giving an overview of our methodology, then we introduce the source and the target of the transformation in Sections 2.2 and 2.3 respectively. The essence of the translation is further developed in Section 2.4. 2.1
Model Driven Engineering (MDE) is a software development methodology where
the (meta-)models are the central elements in the development process. A
metamodel defines the elements of a language. The instances of theses elements are
used to construct a model of the language. A model transformation is defined
by a mapping from elements of the source meta-model to those of the target
meta-model. Consequently, each model conforms to the source meta-model can
be automatically translated to an instance model of the target meta-model. The
Object Management Group (OMG) [
We apply this method in order to define a generic transformation process from
datatypes (used in functional programming) to Ecore models. Figure 2 shows an
overview of our approach. Using an EBNF representation of the datatype
definition grammar [
EBNF representation of a Datatype’s
Grammar
Functional Datatype
Meta−Model <<ConformsTo>>
<<ConformsTo>> Datatype Definition
Datatype Model
Transformation Rules <<Implements>>
Datatype To
Ecore
Ecore
Meta−Model <<ConformsTo>>
Ecore Model Fig. 2. Overview of the Transformation Method
Functional programming supplies us with a rich way to describe data structures.
However, since some features are not supported by Ecore, we have only defined
a subset, that contains the essential elements composing datatypes. Figure 3
depicts the datatype metamodel that is constructed from a subset of datatype’s
declarations grammar [
A Module may contain several Type Definition s. Each Type Definition has a Type Constructor. It corresponds to the data types’ name. It is also composed of at least one Constructor Declaration. These declarations are used to express variant types. Type declarations have names, it is the name of a particular type case. It takes as argument some (optional) type expressions which can either represent a Primitive Type (int, bool, float, etc.) or also a data type defined previously in the module. The list option is used to represent lists in functional programming. The type option feature describes the presence or the absence of a value. The ref option is used for references (pointers).
We enriched the type definition grammar with a new element named Accessor. It is a function introduced by a special annotation (*@accessor*). It allows to assign a name to a special field of the type declaration. This element is essential for the transformation process, its absence would lead to nameless structural features.
Our target metamodel is a subset of the Ecore metamodel. Ecore is the core
language of Eclipse Modeling Framework (EMF) [
The Meta Object Facility (MOF) standardized by the OMG defines a subset
of UML class diagram [
Figure 4 represents a subset of the Ecore language. This subset contains essentially the elements that are needed for the transformation process. Its main components are: – The EPackage is the root element in serialized Ecore models. It encompasses
EClasses and EDataTypes. – The EClass component represents classes in Ecore. It describes the structure of objects. It contains EAttributes and EOperations. – The EDataType component represents the types of EAttributes, either predefined (types: Integer, Boolean, Float, etc.) or defined by the user. There is a special datatype to represent enumerated types EEnum, each enumeration is called EEnumLiteral. – EReferences is comparable to the UML Association link. It defines the kinds of the objects that can be linked together. The containment feature is a Boolean value that makes a stronger type of relations. When it is set to true, it represents a whole/part relationship known as “by-value aggregation” in UML. 2.4
The transformation method is from functional datatypes to Ecore meta-models. To precisely define transformation rules, the transformation method is presented in a formal notation by the Tr() function. In each case we start by an informal description, then we present it formally and finally we show an efective exemple.
T r : DataT ypes −→ Ecore M eta-model
The following translation functions are given for a concrete syntax in the
style of Caml [
Rule DatatypeToEClass When the datatype is formed of only one constructor, it is translated to an EClass. The EClass name is the name of the type constructor.
T r(tpConstr = cn t1...tn) = createEClass(); setN ame(tpConstr); T rtype(acci, ti) / 1 ≤ i ≤ n Example: datatype tpConstr =
Cn of int ∗ string ∗ ...∗ bool Rule DatatypeToEEnum Datatypes composed only of constructors (without typexpr s) are translated to EEnums which are usually employed to model enumerated types in Ecore. There, each constructor from the datatype model is translated into an EEnumLiteral. T r(tpConstr = cn1|...|cnp) = createEEnum(); setN ame(tpConstr);
T rconstrNm(cni) / 1 ≤ i ≤ p
T rconstrNm(cni) = EEnumLiteral(cni) / 1 ≤ i ≤ p Example: datatype tpConstr =
Cn1 |Cn2 |... | CnN Rule DatatypeToEClasses When constructor declarations are composed of more than one constructor declaration containing type expressions: a first EClass is created to represent the type constructor (tpConstr ). Then, for each constructor, an EClass is created too, and inherits from the tpConstr one.
T r(tpConstr = cd1|...|cdn) = createEClass(); setN ame(tpConstr); T rdecl(cdi) / 1 ≤ i ≤ n T rdecl : ConstructorDeclaration −→ EClass T rdecl(cni t1...tm) = createEClass(); setN ame(cni); setSuperT ype (EClass(tpConstr)); T rtype(accj , tj ) / 1 ≤ j ≤ m Example: datatype tpConstr =
Cn1 of string |Cn2 of int |...
|CnN of bool Rule PrimitivTypeToEAttribute If a type expression is formed of a primitive type, the translation function generates a new EAttribute. The name of this EAttribute is the name of its corresponding accessor, and its type is the EMF representation of the the primitive type : EInt for int, EBoolean for bool, EString for string, etc.
T rtype : (accessor, type) −→ EStructualF eature T rtype(acc, primT p) = createEAtrribute(); setN ame(acc); setT ype(primT pEMF ); Example: datatype tpConstr =
Cn of int ∗ string ∗ ...∗ bool Rule TypeToEReference When a type expression contains a type which is not a primitive type, the latter has to be previously defined in the Isabelle theory. Then, a containment link is created between the current EClass and the EClass referenced by type constructor, and the multiplicity is set to 1. Example: datatype tpConstr =
Cn oftpConstr2 Rule TypeOptionToMultiplicity The type expressions can also appear in the form of a type list. In this case the multiplicity is set to 0...*. The type expression type option is used to express whether a value is present or not. It returns None, if it is absent and Some value, if it is present. This is modeled by changing the cardinality to 0...1.
T rtype : (accessor, type) −→ EStructualF eature T rtype(acc, t list) = T rtype(acc, t) setLowerBound(0); setU pperBound(∗); T rtype(acc, t option) = T rtype(acc, t) setLowerBound(0); setU pperBound(1); Example: datatype tpConstr =
Cn oftpConstr2 list
The last case that we deal with, is type ref which is used to represent pointers. It is translated to references without containments.
T rtype(acc, t ref) = T rtype(acc, t)
setContainment(F alse); Example: datatype tpConstr =
Cn of tpConstr2 ref 3
In this section, we apply the method presented in Section 2 on a detailed example that consist of a Domain Specific Language. We start by the DSL definition, then we show the architecture of the application before finishing with the efective results of the transformation. 3.1
We are currently working on a real-time dialect of the Java language allowing
us to carry out specific static analyses of Java programs. We only sketch this
language here; details are described in [
All this made us opt for writing our own syntax analysis, which is integrated
into the Eclipse Xtext environment [
The formal aspect comes into play at the following point: We are currently developing a real-time semantics of Java in the proof assistant Isabelle, based on an execution semantics using inductive relations. Performing the translation for the whole language description would generate a huge metamodel that couldn’t be presented in the paper. We thus choose to present a only an excerpt of it, corresponding to a method definition.
Figure 6 shows the datatype definitions in the Isabelle proof assistant, where a method definition is composed of a method declaration, a list of variables, and statements. Each method declaration has an access modifier that specifies its kind. It also has a type, a name, and some variable declarations. The stmt datatype describes the statements allowed in the method body: Assignments, Conditions, Sequence of statements, Return and the annotation statement (for timing annotations). In this example we use Booleans, integers, strings for types and values. 3.2
Our approach is implemented using the Eclipse environment which includes
among others
– Eclipse Modeling Framework (EMF) [
Figure 5 shows the architecture of our application. There, green arrows represent model transformations or code generation. The base element is an Isabelle theory where both of the datatypes and the properties to be checked are defined. The corresponding meta-model is generated using the translation function described in Section 2.4. Starting from a generated Ecore meta-model, we use the Xtext tool to define a textual concrete syntax. First, Xtext builds an EBNF grammar depending on the structure of the metamodel. The grammar is then adapted using the right key words of the language, yielding a textual editor as an Eclipse plug-in.
Theory
DSL Graphical /Textual Notation
This part of the theory was given as input to the implementation of our translation rules presented in Section 2.4. The resulting Ecore diagram is presented in Figure 7.
As it is shown on the figure, data type definitions built only of type constructors (Tp, AccModifier , Binop, Binding ) are treated as enumerations in the metamodel. Whereas Datatype MethodDecl composed of only one constructor derive a single class. As for type expressions that represent list of types (like accModifier list in varDecl ), they generate a structural feature in the corresponding class and their multiplicities are set to (0...*). The result of type definitions containing more than one constructor and at least a type expression (stmt and expr ) is modeled as a number of classes inheriting from a main one. Finally, the translation of the int, bool and string types is straightforward. They are translated to respectively EInt, EBoolean and EString.
Fig. 6. Datatypes in Isabelle
EMF models are comparable to Unified Modeling Language Class diagrams. For
this fact we are interested in the mappings from other formal languages to UML
Class diagrams. Some research is dedicated to establishing the link between these
two formalisms. We cite the work of Idani & al. that consists of a generic
transformation of UML models to B constructs [
Similarly, there is an MDE based transformation approach for generating
Alloy (a textual modeling language based on first order logic) specifications
from UML class diagrams and backwards [
Delahaye & al. describe in [
These methods enable to generate UML component from a formal description but their formal representation is significantly diferent from our needs: functional data structures.
Also, graph transformation tools [
Our approach combines the two views by ofering the possibility to define the abstract syntax of a DSL, to run some verifications on the top of it and to generate the corresponding metamodel to graphically document the formal developments. Furthermore, this metamodel can be used to easily generate a textual editor using Xtext facilities. 5
Our work constitutes a first step towards a combination of interactive proof and Model Driven Engineering. We have presented a generic method based on MDE for transforming data type definitions used in proof assistants to Class diagrams.
The approach is illustrated with the help of a Domain Specific Language developed by ourselves. It is a Java-like language enriched with annotations. Starting from data type definitions, set up for the semantic modeling of the DSL we have been able to generate an EMF meta-model. In addition to its benefits for documenting and visualizing the DSL, it is manipulated in the Eclipse workbench to generate a textual editor as an Eclipse plug-in.
Currently, we are working on extending subset of data type definitions by adding a way to transform parameterized types to generic types in Ecore. And coupling our work with the generation of provably correct object oriented code from proof assistants. Moreover, we intend to work on the opposite side of transformation, the possibility to generate data structure definitions from class diagrams.