Verification of High-Level Transformations with Inductive Refinement Types
Authors:
Ahmad Salim Al-Sibahi,
Thomas P. Jensen,
Aleksandar S. Dimovski,
Andrzej Wasowski
Abstract:
High-level transformation languages like Rascal include expressive features for manipulating large abstract syntax trees: first-class traversals, expressive pattern matching, backtracking and generalized iterators. We present the design and implementation of an abstract interpretation tool, Rabit, for verifying inductive type and shape properties for transformations written in such languages. We d…
▽ More
High-level transformation languages like Rascal include expressive features for manipulating large abstract syntax trees: first-class traversals, expressive pattern matching, backtracking and generalized iterators. We present the design and implementation of an abstract interpretation tool, Rabit, for verifying inductive type and shape properties for transformations written in such languages. We describe how to perform abstract interpretation based on operational semantics, specifically focusing on the challenges arising when analyzing the expressive traversals and pattern matching. Finally, we evaluate Rabit on a series of transformations (normalization, desugaring, refactoring, code generators, type inference, etc.) showing that we can effectively verify stated properties.
△ Less
Submitted 17 September, 2018;
originally announced September 2018.
The Formal Semantics of Rascal Light
Authors:
Ahmad Salim Al-Sibahi
Abstract:
Rascal is a high-level transformation language that aims to simplify software language engineering tasks like defining program syntax, analyzing and transforming programs, and performing code generation. The language provides several features including built-in collections (lists, sets, maps), algebraic data-types, powerful pattern matching operations with backtracking, and high-level traversals s…
▽ More
Rascal is a high-level transformation language that aims to simplify software language engineering tasks like defining program syntax, analyzing and transforming programs, and performing code generation. The language provides several features including built-in collections (lists, sets, maps), algebraic data-types, powerful pattern matching operations with backtracking, and high-level traversals supporting multiple strategies. Interaction between different language features can be difficult to comprehend, since most features are semantically rich. The report provides a well-defined formal semantics for a large subset of Rascal, called Rascal Light, suitable for develo** formal techniques, e.g., type systems and static analyses. Additionally, the report states and proofs a series of interesting properties of the semantics, including purity of backtracking, strong ty**, partial progress and the existence of a terminating subset.
△ Less
Submitted 6 February, 2018; v1 submitted 7 March, 2017;
originally announced March 2017.
