DROPS

Document

DOI: 10.4230/LIPIcs.RTA.2015.74

A faithful encoding of programmable strategies into term rewriting systems

Authors: Horatiu Cirstea, Serguei Lenglet, and Pierre-Etienne Moreau

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract

Rewriting is a formalism widely used in computer science and mathematical logic. When using rewriting as a programming or modeling paradigm, the rewrite rules describe the transformations one wants to operate and declarative rewriting strategies are used to control their application. The operational semantics of these strategies are generally accepted and approaches for analyzing the termination of specific strategies have been studied. We propose in this paper a generic encoding of classic control and traversal strategies used in rewrite based languages such as Maude, Stratego and Tom into a plain term rewriting system. The encoding is proven sound and complete and, as a direct consequence, established termination methods used for term rewriting systems can be applied to analyze the termination of strategy controlled term rewriting systems. The corresponding implementation in Tom generates term rewriting systems compatible with the syntax of termination tools such as AAProVE and TTT2, tools which turned out to be very effective in (dis)proving the termination of the generated term rewriting systems. The approach can also be seen as a generic strategy compiler which can be integrated into languages providing pattern matching primitives; this has been experimented for Tom and performances comparable to the native Tom strategies have been observed.

Cite as

Horatiu Cirstea, Serguei Lenglet, and Pierre-Etienne Moreau. A faithful encoding of programmable strategies into term rewriting systems. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 74-88, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cirstea_et_al:LIPIcs.RTA.2015.74,
  author =	{Cirstea, Horatiu and Lenglet, Serguei and Moreau, Pierre-Etienne},
  title =	{{A faithful encoding of programmable strategies into term rewriting systems}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{74--88},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.74},
  URN =		{urn:nbn:de:0030-drops-51908},
  doi =		{10.4230/LIPIcs.RTA.2015.74},
  annote =	{Keywords: Programmable strategies, termination, term rewriting systems}
}

Document

DOI: 10.4230/OASIcs.TrustworthySW.2006.697

Formal Validation of Pattern Matching code

Authors: Claude Kirchner, Pierre-Etienne Moreau, and Antoine Reilles

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)

Abstract

When addressing the formal validation of generated software, two main alternatives consist either to prove the correctness of compilers or to directly validate the generated code. Here, we focus on directly proving the correctness of compiled code issued from powerful pattern matching constructions typical of ML like languages or rewrite based languages such as ELAN, MAUDE or Tom. In this context, our first contribution is to define a general framework for anchoring algebraic pattern-matching capabilities in existing languages like C, Java or ML. Then, using a just enough powerful intermediate language, we formalize the behavior of compiled code and define the correctness of compiled code with respect to pattern-matching behavior. This allows us to prove the equivalence of compiled code correctness with a generic first-order proposition whose proof could be achieved via a proof assistant or an automated theorem prover. We then extend these results to the multi-match situation characteristic of the ML like languages. The whole approach has been implemented on top of the Tom compiler and used to validate the syntactic matching code of the Tom compiler itself.

Cite as

Claude Kirchner, Pierre-Etienne Moreau, and Antoine Reilles. Formal Validation of Pattern Matching code. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{kirchner_et_al:OASIcs.TrustworthySW.2006.697,
  author =	{Kirchner, Claude and Moreau, Pierre-Etienne and Reilles, Antoine},
  title =	{{Formal Validation of Pattern Matching code}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.697},
  URN =		{urn:nbn:de:0030-drops-6978},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.697},
  annote =	{Keywords: Correctness proofs, compilers, pattern matching, validation}
}

Search Results

Documents authored by Moreau, Pierre-Etienne

A faithful encoding of programmable strategies into term rewriting systems

Abstract

Cite as

Formal Validation of Pattern Matching code

Abstract

Cite as

Thanks for your feedback!

Could not send message