TRX: A Formally Verified Parser Interpreter
TRX: A Formally Verified Parser Interpreter
复制标题
TRX：经过正式验证的解析器解释器
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Henri Binsztok
中科院分区：
文献类型：
--
作者：
A. Koprowski;Henri Binsztok
解析是计算机科学中的一个重要问题，但令人惊讶的是，很少有人关注它的形式验证。本文介绍了在证明助手Coq中正式开发的一个分析器解释器TRX，它能够产生形式上正确的分析器。我们正在使用解析表达式语法(PEGS)，这是一种本质上代表递归下降解析的形式主义，我们认为它是上下文无关语法(CFGs)的一个有吸引力的替代方案。从这种形式化中，我们可以提取具有完全正确性保证的任意PEG语法的解析器，即，所得到的解析器是终止的，并且关于其语法和peg的语义是正确的；这两个属性在Coq中被正式证明。
Parsing is an important problem in computer science and yet surprisingly little attention has been devoted to its formal verification. In this paper, we present TRX: a parser interpreter formally developed in the proof assistant Coq, capable of producing formally correct parsers. We are using parsing expression grammars (PEGs), a formalism essentially representing recursive descent parsing, which we consider an attractive alternative to context-free grammars (CFGs). From this formalization we can extract a parser for an arbitrary PEG grammar with the warranty of total correctness, i.e., the resulting parser is terminating and correct with respect to its grammar and the semantics of PEGs; both properties formally proven in Coq.
总解析器组合器
影响因子：
--
作者：
Danielsson N
通讯作者：
Danielsson N