Foundational Analysis Techniques for High-Level Transformation Programs

High-level transformation languages like TXL and Rascal, simplify writing and
maintaining transformations such as refactorings and optimizations, by providing
specialized language constructs that include powerful pattern matching, generic
traversals, and fixed-point iteration. This expressivity unfortunately makes
it hard to reason about the semantics of these languages, and there exists few
automated validation and verification tools for these languages.
The goal of this dissertation is to develop foundational techniques and prototype
tools for verifying transformation programs, based on techniques from traditional
programming language research. At first, I present a systematic analysis
of declarative high-level transformation languages, like QVT and ATL, seeking
to clarify their expressiveness. The analysis showed that virtually all examined
languages were Turing-complete and thus could not be treated specially for verification.
I describe a joint effort in designing and validating an industrial modernization
project using the high-level transformation language TXL. The transformation
was validated using the translation validation and symbolic execution, catching
50 serious bug cases in an otherwise well-tested expert-written transformation,
and thus showing the need for verification tools in this domain.
Using these experiences, I develop a formal symbolic execution algorithm for a
small transformation language capturing key high-level constructs. A proto-type
white-box test generation tool was implemented using the algorithm, and evaluated
on a series of refactorings and model transformations comparing favorably
against baseline black-box test generator in terms of test coverage.
I present the first formal operational semantics for a large subset of Rascal,
called Rascal Light, which has been validated by formally proving a series of
semantic properties regarding strong typing, safety and termination. This creates
a solid basis for further foundational work on high-level transformation languages.
Finally, I develop a formal abstract interpreter for Rascal Light, with a modular
abstract domain design and a Schmidt-style abstract operational semantics,
adapting the idea of widening by trace memoization to work with inputs from
infinite domains. The technique is evaluated on real Rascal transformations,
showing that it is possible to effectively verify target type and shape properties.