A Proof of the Correctness of a Simple Parser of Expressions by the Boyer-Moore System.
Abstract
The objective of this report is to convey the essential idea of a proof by the Boyer-Moore Theorem Prover of the correctness of a parser. The proof required a total of 147 definitions and lemmas--all of which have been listed in the appendix. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 01, 1978
- Accession Number
- ADA058615
Entities
People
- Paul Y. Gloess
Organizations
- SRI International