skip to main content
10.1145/1069774.1069792acmconferencesArticle/Chapter ViewAbstractPublication PagesppdpConference Proceedingsconference-collections
Article

Formal validation of pattern matching code

Published: 11 July 2005 Publication History

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.

References

[1]
Franz Baader and Tobias Nipkow. Term Rewriting and all That. Cambridge University Press, 1998.]]
[2]
Don Batory, Bernie Lofaso, and Yannis Smaragdakis. JTS: tools for implementing domain-specific languages. In Proceedings Fifth International Conference on Software Reuse, pages 143--153, Victoria, BC, Canada, 1998. IEEE.]]
[3]
Robert S. Boyer and Yuan Yu. Automated correctness proofs of machine code programs for a commercial microprocessor. In D. Kapur, editor, Proceedings of the Eleventh International Conference on Automated Deduction, pages 416--430. Springer-Verlag, 1992.]]
[4]
Horatiu Cirstea, Claude Kirchner, and Luigi Liquori. Matching Power. In Aart Middeldorp, editor, Proceedings of RTA'2001, volume 2051 of LNCS, Utrecht (The Netherlands), May 2001. Springer-Verlag.]]
[5]
Damien Doligez. Zenon: an automatic theorem prover for first-order logic. Available as part of the Focal system at http://focal.inria.fr/download.]]
[6]
Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Theorem proving modulo. Journal of Automated Reasoning, 31(1):33--72, Nov 2003.]]
[7]
Fabrice Le Fessant and Luc Maranget. Optimizing pattern matching. In Proceedings of the sixth ACM SIGPLAN International Conference on Functional Programming, pages 26--37. ACM Press, 2001.]]
[8]
Sumit Gulwani and George C. Necula. Global value numbering using random interpretation. In POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 342--352. ACM Press, 2004.]]
[9]
Gilles Kahn. Natural semantics. In 4th Annual Symposium on Theoretical Aspects of Computer Sciences on STACS 87, pages 22--39, London, UK, 1987. Springer-Verlag.]]
[10]
Hélène Kirchner and Pierre-Etienne Moreau. Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associative-commutative theories. Journal of Functional Programming, 11(2):207--251, 2001.]]
[11]
Andreas Krall and Jan Vitek. On extending java. In Proceedings of the Joint Modular Languages Conference on Modular Programming Languages, pages 321--335. Springer-Verlag, 1997.]]
[12]
David Lacey, Neil D. Jones, Eric Van Wyk, and Carl Christian Frederiksen. Proving correctness of compiler optimizations by temporal logic. In Proc. 29th ACM Symposium on Principles of Programming Languages, pages 283--294. ACM Press, 2002.]]
[13]
John McCarthy and James Painter. Correctness of a compiler for arithmetic expressions. In J. T. Schwartz, editor, Proceedings Symposium in Applied Mathematics, Vol. 19, pages 33--41. AMS, 1967.]]
[14]
Pierre-Etienne Moreau, Christophe Ringeissen, and Marian Vittek. A Pattern Matching Compiler for Multiple Target Languages. In G. Hedin, editor, 12th Conference on Compiler Construction, volume 2622 of LNCS, pages 61--76. Springer-Verlag, May 2003.]]
[15]
F. Lockwood Morris. Advice on structuring compilers and proving them correct. In Proceedings of the 1st annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 144--152. ACM Press, 1973.]]
[16]
George C. Necula. Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106--119. ACM Press, 1997.]]
[17]
George C. Necula and Peter Lee. The design and implementation of a certifying compiler. SIGPLAN Not., 39(4):612--625, 2004.]]
[18]
Dino P. Oliva, John D. Ramsdell, and Mitchell Wand. The VLISP verified PreScheme compiler. Lisp Symb. Comput., 8(1-2):111--182, 1995.]]
[19]
Amir Pnueli, Michael Siegel, and Eli Singerman. Translation validation. In Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, pages 151--166. Springer-Verlag, 1998.]]
[20]
Martin C. Rinard and Darko Marinov. Credible compilation with pointers. In Proceedings of the FLoC Workshop on Run-Time Result Verification, Trento, Italy, July 1999.]]
[21]
Xavier Rival. Symbolic transfer function-based approaches to certified compilation. In Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 1--13. ACM Press, 2004.]]
[22]
Mark. G. J. van den Brand, Pierre-Etienne Moreau, and Jurgen Vinju. Generator of efficient strongly typed abstract syntax trees in Java. IEE Proceedings - Software Engineering, 152(2):70--79, April 2005.]]
[23]
Philip Wadler. Views: a way for pattern matching to cohabit with data abstraction. In Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 307--313. ACM Press, 1987.]]
[24]
Dinghao Wu, Andrew W. Appel, and Aaron Stump. Foundational proof checkers with small witnesses. In Proceedings of the 5th ACM SIGPLAN international Conference on Principles and Practice of Declarative Programming, pages 264--274. ACM Press, 2003.]]

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
PPDP '05: Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming
July 2005
260 pages
ISBN:1595930906
DOI:10.1145/1069774
  • General Chair:
  • Pedro Barahona,
  • Program Chair:
  • Amy Felty
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 July 2005

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. compilation
  2. multi-match
  3. pattern matching
  4. term rewriting
  5. verified code

Qualifiers

  • Article

Conference

PPDP05
Sponsor:

Acceptance Rates

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)3
  • Downloads (Last 6 weeks)0
Reflects downloads up to 18 Feb 2025

Other Metrics

Citations

Cited By

View all

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media