A Language and Framework for Invariant-Driven Transformations
Yanhong A. Liu, Michael Gorbovitski, and Scott D. Stoller

This paper describes a language and framework that allow coordinated transformations driven by invariants to be specified declaratively and applied automatically. The framework supports incremental maintenance of invariants for program design and optimization, as well as general transformations for instrumentation, refactoring, and other purposes. We also describe our implementations for transforming Python and C programs and experiments with successful applications of the systems in generating efficient implementations from clear and modular specifications, in instrumenting programs for runtime verification, profiling, and debugging, and in code refactoring.