Parsing Schemata and Correctness of Parsing Algorithms

Klaas Sikkel
University of Twente, Faculty of Computer Science
PO Box 217, 7500 AE Enschede, the Netherlands
sikkel@cs.utwente.nl

Abstract

Parsing schemata give a high-level formal description of
parsers. These can be used, among others, as an intermediate level of
abstraction for deriving the formal correctness of a parser.
A parser is correct if it duly implements a parsing schema that is known
to be correct.
  We discuss how the correctness of a parsing schema can be proven and
how parsing schemata relate to some well-known classes of parsers,
viz. chart parsers and LR-type parsers.

Key words: Parsing Schemata, Chart Parsers, Correctness proof