A Proof of the Correctness of a Simple Parser of Expressions by the Boyer-Moore System.

reportActive / Technical Report | Accession Number: ADA058615 | Open PDF

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

Author(s):
Gloess, Paul Y.
Author Organization(s):
SRI INTERNATIONAL MENLO PARK CA
Descriptive Note:
Technical rept.,
Pagination:
0054

Security Markings

DOCUMENT & CONTEXTUAL SUMMARY

Distribution:
Approved For Public Release

RECORD

Collection: TR
Identifying Numbers
Report Number(s):
SRI-TR-7
Contract/Grant Number(s):
N00014-75-C-0816
 Subject Terms
Joint Capability Areas:
JCA_1.2.5_Lessons Learned; JCA_5_Command and Control
Modernization Areas:
Directed Energy; Autonomy
Communities of Interest:
Advanced Electronics
Descriptor(s):
*PROBLEM SOLVING, *PARSERS, RECURSIVE FUNCTIONS, OPERATORS(MATHEMATICS), COMPUTER PROGRAM VERIFICATION, THEOREMS
Field(s)/Group(s):
Linguistics, Numerical Mathematics
Keyword(s):
Boyer Moore Theorem, WUNR049 378
Report Date:
1978 Aug 01