Semantic Correctness of a Compiler for an Algol-Like Language

Abstract

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 10, 1967
Accession Number
ADA003619

Entities

People

  • James A. Painter

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Alphabets
  • Arithmetic
  • Artificial Intelligence
  • Automata
  • Compilers
  • Computations
  • Computer Languages
  • Computer Programming
  • Computer Science
  • Computers
  • Formal Languages
  • Language
  • Machine Languages
  • Machines
  • Notation
  • Programming Languages

Fields of Study

  • Computer science

Readers

  • Computational Linguistics