Semantic Correctness of a Compiler for an Algol-Like Language,
STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
This is a semantic proof of the correctness of a compiler. The abstract syntax and semantic definition are given for the language Mickey, an extension of Micro-ALGOL. The abstract syntax and semantics are given for a hypothetical one-register single-address computer with 14 operations. A compiler, using recursive descent, is defined. Formal definitions are also given for state vector, a and c functions, and correctness of a compiler. Using these definitions, the compiler is proven correct.
- Computer Programming and Software