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

Matched Rules. The matched rules constitute the core of an ATL declarative
transformation since they make it possible to specify the kind of source elements
for which target elements must be generated, and the way the generated target
elements have to be initialized. A matched rule is introduced by the following
construction.
rule rule_name {
from in_var : in_type [(condition)]
[using { var1 : var_type1 = init_exp1;
... }]
to out_var1 : out_type1 (bindings1),
...
}
The source pattern is defined after the keyword from . It enables to specify a
model element variable that corresponds to the type of source elements that
the rule has to match. When defined, the local variable section is introduced
by the keyword using . The target pattern of a matched rule is introduced by
the keyword to . It serves to specify the elements to be generated when the
source pattern of the rule is matched, and how these generated elements are
initialized (bindings). An optional condition (expressed as an ATL expression)
within the rule source pattern is used to select the subset of the source elements
that conform to the matching type.
Matched rules are generally translated into propositions of the form
∀ a:A. (a ∈ InstA ∧ Cond(a) →∃ b:B. (b ∈ InstB ∧ Rel(a,b)))
expressing that for every object a of the type A (of the source model element
in the matched rule) in the set InstA of all instances of type A which satisfies
certain condition Cond , there exists an object b of the type B (of the target
model element in the matched rule) in the set InstB of all instances of type B ,
for whom the relation Rel holds. The relation Rel is a conjunction of the bindings
defined in the matched rule. If there are no other matched rules that define the
existence of a target model element for whom the same relation Rel holds, then
the proposition must state the unique existence of the target model element.
There are also propositions describing the relation in the reverse direction (i.e.
from the target to the source elements).
The formulæ thus obtained amount to (basic) specifications of the transfor-
mation rules at a propositional level. This stands in contrast to the approach
in [17] where transformations were represented as functions about which the
relevant properties had to be proven, leading to lengthy work that can now be
avoided.
In the example we have the following matched rule that transforms an
Attribute of a class diagram into a Column of the database. The name of the
column will be the name of the attribute, and the type of the column will be the
name of the PrimitiveDataType associated to the attribute (the helper already
introduced is used in this case).