首页    期刊浏览 2024年12月05日 星期四
登录注册

文章基本信息

  • 标题:Formal Validation of Pattern Matching code
  • 作者:Claude Kirchner ; Pierre-Etienne Moreau ; Antoine Reilles
  • 期刊名称:OASIcs : OpenAccess Series in Informatics
  • 电子版ISSN:2190-6807
  • 出版年度:2006
  • 卷号:3
  • DOI:10.4230/OASIcs.TrustworthySW.2006.697
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要: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.
  • 关键词:Correctness proofs; compilers; pattern matching; validation
Loading...
联系我们|关于我们|网站声明
国家哲学社会科学文献中心版权所有