Pattern eliminating transformations

Pierre Lermusiaux 1, 2 Horatiu Cirstea 3 Pierre-Etienne Moreau 3
2 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
3 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 metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-02186325
Contributor : Pierre Lermusiaux <>
Submitted on : Wednesday, July 17, 2019 - 11:47:59 AM
Last modification on : Wednesday, August 28, 2019 - 2:57:15 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02186325, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

49

Files downloads

422