Formal Validation of Pattern Matching Code
Identifieur interne : 004017 ( Crin/Curation ); précédent : 004016; suivant : 004018Formal Validation of Pattern Matching Code
Auteurs : Claude Kirchner ; Pierre-Étienne Moreau ; Antoine ReillesSource :
English descriptors
Abstract
When addressing the problem of software formal validation, two main alternatives consist either to prove the correctness of compilers or to directly validate the generated code. We address here the specific problem of directly proving the correctness of compiled code issued from powerful pattern matching constructions appearing in high-level programming languages as ML like languages or rewrite based languages such as ELAN or Tom. In this context, our first contribution is to define a general framework allowing to anchor 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.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: Pour aller vers cette notice dans l'étape Curation :004017
Links to Exploration step
CRIN:kirchner05aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="341">Formal Validation of Pattern Matching Code</title></titleStmt><publicationStmt><idno type="RBID">CRIN:kirchner05a</idno><date when="2005" year="2005">2005</date><idno type="wicri:Area/Crin/Corpus">004017</idno><idno type="wicri:Area/Crin/Curation">004017</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">004017</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Formal Validation of Pattern Matching Code</title><author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name></author><author><name sortKey="Moreau, Pierre Etienne" sort="Moreau, Pierre Etienne" uniqKey="Moreau P" first="Pierre-Étienne" last="Moreau">Pierre-Étienne Moreau</name></author><author><name sortKey="Reilles, Antoine" sort="Reilles, Antoine" uniqKey="Reilles A" first="Antoine" last="Reilles">Antoine Reilles</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>compilation</term><term>multi-match</term><term>pattern matching</term><term>term rewriting</term><term>verified code</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="3800">When addressing the problem of software formal validation, two main alternatives consist either to prove the correctness of compilers or to directly validate the generated code. We address here the specific problem of directly proving the correctness of compiled code issued from powerful pattern matching constructions appearing in high-level programming languages as ML like languages or rewrite based languages such as ELAN or Tom. In this context, our first contribution is to define a general framework allowing to anchor 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.</div></front></TEI><BibTex type="inproceedings"><ref>kirchner05a</ref><crinnumber>A05-R-005</crinnumber><category>3</category><equipe>PROTHEO</equipe><author><e>Kirchner, Claude</e><e>Moreau, Pierre-Étienne</e><e>Reilles, Antoine</e></author><title>Formal Validation of Pattern Matching Code</title><booktitle>{Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming - PPDP'2005, Lisbon, Portugal}</booktitle><year>2005</year><editor>Barahone, Pedro and Felty, Amy</editor><pages>187--197</pages><month>Jul</month><publisher>ACM</publisher><keywords><e>compilation</e><e>pattern matching</e><e>multi-match</e><e>term rewriting</e><e>verified code</e></keywords><abstract>When addressing the problem of software formal validation, two main alternatives consist either to prove the correctness of compilers or to directly validate the generated code. We address here the specific problem of directly proving the correctness of compiled code issued from powerful pattern matching constructions appearing in high-level programming languages as ML like languages or rewrite based languages such as ELAN or Tom. In this context, our first contribution is to define a general framework allowing to anchor 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.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004017 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Curation/biblio.hfd -nk 004017 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Curation
|type= RBID
|clé= CRIN:kirchner05a
|texte= Formal Validation of Pattern Matching Code
}}
| This area was generated with Dilib version V0.6.33. |  |