Magenta text is new
TB (short for There and Back again)
is an experimental document to specify formal proofs of correctness for
metamodel refactorings. The name TB is a subtitle to The Hobbit
by J.R.R. Tolkien, but it has similar relevance here. To prove two MDE
metamodels, mm1 and mm2, are refactorings of each other, one
mapping is defined to convert every mm1 instance to a
corresponding mm2 instance, and a second mapping converts every mm2
instance to a corresponding mm1 instance. By showing these mappings are the inverses of each other, mm1
and mm2 contain the same information and thus are refactorings of each
other.
TB
is an ongoing experiment whose design will evolve
over time. This document explains its current incarnation.
1. A Basic TB Specification
Our best understanding at this time is that a TB spec contains:
- The definition of two MDELite schemas -- not OO schemas, but database schemas whose inherited attributes have been propagated. See tool OO2DBSchema.
- A
set of functions to express key mappings in a proof.
- A set of axioms or identities that relate functions, expressed in an algebraic-spec-like- way.
- Metamodel constraints for each schema and perhap constraints that cover both schemas, also expressed using TB-spec functions.
At present, all of these specifications are combined into a single document, an example of which named PersonCarWOpts.tb.tb is shown below. It has the following keywords and regions::::test/TB3/TestData/PersonCarWOpts.tb.tb:::
Here is an explanation of each region:
#variables
x : E. // says foreach x in E
y : F. // says foreach y in F
#axioms
A1 : pop(push(x))=x. // says foreach x in E: pop(push(x))=x.
#constraints
C1 : join(x,y)=reverse(join(y,x)). // says foreach x in E, y in F : join(x,y)=reverse(join(y,x)).
- The
lines following #axioms are axioms that hold among the functions
(declared and implicit). Every axiom has a name, colon (:),
expression '=' expression, dot (.).
Consider the circleLeft axiom. It says foreach x in Person2: P12(P21(x)) = x. Or in English, P12 and P21 are inverses of each other. - The
lines following #constraints are constraints in schema1, schema2, and among elements in schema1 and schema2. Each
constraint has a name, colon (:), expression, dot (.).
Consider axiom applycon1. It says foreach c in Car1: con1( owned1(c), favored1(c)) is always true. Note that owned1:Car1->Person1 and favored1:Car1->option_Person1
are functions that are derived from attribute definitions in schema1.
(Such function defs are implicitly added to a tb spec by MDELite
tools; same for schema2).
Note: Primitive types are already defined -- and of course can be extended. The set of primitive types now supported are:
- int - integer
- bool - boolean
- string - string, quoted and unquoted
- float - single precision
- double - double precision
2. Available Tools
There are three provisional tools that have been released (and are likely full of bugs): TB.Parser, TB.Conform, and TB.UnParser.
2.1 TB.Parser
Converts a TB spec file into a TB datbse. A typical invocation is:
> java TB.Parser PersonCarWOpts.tb.tb
// produces personCarWOpts.tb.pl or reports a parsing error
The current output of this tool is the MDELite datbse below:
:::test/TB3/Correct/PersonCarWOpts.tb.pl:::
Note
that a polish expression is stored in tuples that represent axioms and
constraints. These expressions are reparsed when needed to
evaluate their structural properties (ex: being type correct) and for
M2T mappings. Also Note that the implicit attribute functions
that are derivable from a schema are present in this database.
2.2 TB.Conform
Checks if a given TB datbse satisfies standard contraints. A typical invocation is:
> java TB.Conform PersonCarWOpts.tb.pl
// returns nothing if no errors are found or reports a constraint violation
2.3 TB.UnParser
Translates a TB databse into a TB spec. A typical invocation is:
> java PersonCarWOpts.tb.pl PersonCarPrime.tb.pl
// produces personCarPrime.tb.tb
Advice: when creating round trip tests, be sure to rename the output file above, so as not to destroy the original file, like:
java TB.Parser PersonCarWOpts.tb.tb
java TB.Conform PersonCarWOpts.tb.pl
java TB.UnParser PpersonCarWOpts.tb.pl PersonCarPrime.tb.tb
// check equality of personCarWOpts.tb.tb and personCarPrime.tb.tb
In
general, a round trip from alpha.tb.tb (for any alpha) to alpha.tb.pl
back to alphaPrime.tb.tb should produce two semantically equivalent but
syntactically different (ex: difference in white space, missing
comments) files.
Big Picture
The
figure below shows the big picture w.r.t. the above tools. A TB
spec can be translated into a TB datbse by parsing and
recovered by unparsing.
3. What is Next?
Lots!
A tb file simply is a high-level definition of a metamodel
refactoring. It needs to be translated into a rooster spec to be
proven. There needs to be implementation details added so that
real constraints can be applied. And so on. Here's a list of some possibilities:
- Tools
need to be exercised to ensure that (a) they work, (b) output useful,
not cryptic, error messages, and (c) provide a "natural" language in
which to write metamodel refactoring specifications.
- Add optional to domain declarations.
- Add implementation specs for constraints and maybe functions.
- And
adding tools that implement the following M2T arrows: Translating
a tb datbse into a rooster specification and into a Java program +
regression test.
Stay Tuned....