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

Data Types. ATL's data types are based on the OCL. They include primitive
types (boolean, integer, real, string), tuples, enumerates, collections (set, ordered
set, bag, sequence), among others. All these types can be represented in Coq as
described in section 3.

OCL Declarative Expressions. ATL uses additional OCL declarative expre-
ssions in order to structure the code. ATL's If-Then-Else , Let (which enables
the definition of variables) and constant expressions (constant values of any sup-
ported data type) are natively supported in Coq. Finally, the collection iterative
expressions are supported in Coq with recursion operators on lists.

Helpers and Attributes. Helper/attribute call expressions as well as opera-
tion call expressions are OCL-based expressions. ATL helpers factorize code that
can be called from different points of an ATL transformation. An ATL helper is
defined by the following elements: a name, a context type, a return value type,
an ATL expression that represents the code of the ATL helper, and an optional
set of parameters, in which a parameter is identified by a pair (parameter name,
parameter type). From a functional point of view an attribute is a helper that
accepts no parameters. Both helpers and attributes are represented as functions
in the richly-typed functional programming language provided by Coq. The main
issue in this translation is that Coq imposes the condition that every recursion
be well-founded, which has to be proven in each case.
In the example there is the following helper function that transforms a
PrimitiveDataType

into a string which represents the type of a column in the

database.

helper context SimpleUML!PrimitiveDataType def :
primitiveTypeToStringType : String =
if (self.name = 'INTEGER')
then 'NUMBER'
else if (self.name = 'BOOLEAN')
then 'BOOLEAN'
else 'VARCHAR'
endif
endif;

The Coq function resulting from its translation is as follows. Notice that the
comparison between strings ( = ) is performed by an auxiliary function
string_eq_bool which returns a boolean value.

Definition primitiveTypeToStringType (primitiveType : string) : string :=
match (string_eq_bool primitiveType "INTEGER") with
| true => "NUMBER"
| false => match (string_eq_bool primitiveType "BOOLEAN") with
| true => "BOOLEAN"
| false => "VARCHAR"
end

end.