TRX: A FORMALLY VERIFIED PARSER INTERPRETER

被引:17
作者
Koprowski, Adam [1 ]
Binsztok, Henri [1 ]
机构
[1] MLstate, Paris, France
关键词
parser generation; formal verification; coq proof assistant; parsing expression grammars; recursive descent parsing;
D O I
10.2168/LMCS-7(2:18)2011
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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-freegrammars (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.
引用
收藏
页数:26
相关论文
共 35 条
[1]  
Aho A. V., 1972, The Theory of Parsing, Translation, and Compiling
[2]  
[Anonymous], P OWASP APP IN PRESS
[3]  
[Anonymous], WORKSH CONC SPEC PRO
[4]  
[Anonymous], 2009, P 5 INT WORKSH AUT S
[5]  
[Anonymous], AGADA WIKI
[6]  
[Anonymous], 1992, J FUNCT PROGRAM
[7]  
[Anonymous], STRUCTURALL IN PRESS
[8]  
[Anonymous], TEXTS THEORETICAL CO
[9]  
[Anonymous], P 12 ACM SIGPLAN INT
[10]  
[Anonymous], 31 ACM SIGPLAN SIGAC