License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.TrustworthySW.2006.697
URN: urn:nbn:de:0030-drops-6978
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/697/
Go to the corresponding OASIcs Volume Portal

Kirchner, Claude ; Moreau, Pierre-Etienne ; Reilles, Antoine

Formal Validation of Pattern Matching code

pdf-format:
06000.ReillesAntoine.Paper.697.pdf (0.3 MB)

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.

BibTeX - Entry

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

Keywords: Correctness proofs, compilers, pattern matching, validation
Collection: Workshop on Trustworthy Software
Issue Date: 2006
Date of publication: 26.09.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI