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

Formal Validation of Pattern Matching Code

Claude Kirchner 1 Pierre-Etienne Moreau 1 Antoine Reilles 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download

Contributor : Pierre-Etienne Moreau Connect in order to contact the contributor
Submitted on : Tuesday, November 15, 2005 - 11:22:26 AM
Last modification on : Friday, February 4, 2022 - 3:22:10 AM
Long-term archiving on: : Friday, April 2, 2010 - 7:14:12 PM


  • HAL Id : inria-00000701, version 1



Claude Kirchner, Pierre-Etienne Moreau, Antoine Reilles. Formal Validation of Pattern Matching Code. Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming - PPDP'2005, Jul 2005, Lisbon/Portugal, pp.187--197. ⟨inria-00000701⟩



Record views


Files downloads