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 fixedpoint 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 highlevel 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.