Program Verification Using Production Grammars

Emre Demiralp

Wolfram Research / University of Illinois

This paper focuses on the particular applications of production grammars to verification of the functional Mathematica language. There will be a large number of instances where the design of the grammars and the bundled tools will be tailored toward this purpose. In most cases, the properties and the benefits of production grammars can be generalized to a large number and variety of systems. There will also be a discussion of certain properties of how the Mathematica language affected the design and implementation of the actual production grammars.