There and Back again (TB) Refactoring Specifications

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:
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)).
Note: Primitive types are already defined -- and of course can be extended.  The set of primitive types now supported are:

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:

Stay Tuned....