HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Pattern eliminating transformations

Pierre Lermusiaux 1 Horatiu Cirstea 2 Pierre-Etienne Moreau 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : Program transformation is a common practice in computer science, and its many applications can have a range of dierent objectives. For example, a program written in an original high level language could be either translated into machine code for execution purposes, or towards a language suitable for formal verication. Languages often have a lot of dierent constructions, and thus, transformations often focus on eliminating some of these constructions, or at least processing some specic sequence of constructions. Rewriting is a widely established formalism to describe the mechanism and the logic behind such transformations. It relies mainly on the principle of rewrite rules to describe the dier-ent operations performed. Generally type-preserving, these rewrite rules can ensure that the transformation result has a given type and thus give syntactic guarantees on the constructions it consists of. However, we sometimes want the transformation to provide more guarantees on the shape of its result by specifying that some patterns of constructions does not appear. For this purpose, we propose in this paper an approach based on annotating transformation function symbols with (anti-)pattern in order for such transformation to guarantee stronger properties on the shape of its result. With the generic principles governing term algebra and rewriting, we believe this approach to be an accurate formalism to any language providing pattern-matching primitives.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download

Contributor : Pierre Lermusiaux Connect in order to contact the contributor
Submitted on : Wednesday, July 17, 2019 - 11:47:59 AM
Last modification on : Wednesday, November 3, 2021 - 7:09:25 AM


Files produced by the author(s)


  • HAL Id : hal-02186325, version 1



Pierre Lermusiaux, Horatiu Cirstea, Pierre-Etienne Moreau. Pattern eliminating transformations. CIEL 2019 - 8ème Conférence en IngénieriE du Logiciel, Jun 2019, Toulouse, France. ⟨hal-02186325⟩



Record views


Files downloads