Interactive Compiler Proving Using Hoare Proof Rules
Abstract
This report demonstrates the proofs by structural induction of two compilers. The larger is a compiler from a subset of pure LISP into a machine language, and is similar to a compiler proved by London. The smaller is the compiler proved by McCarthy and Painter. In addition a portion of another compiler is proved. It is the compiler given by Wirth to compile a simple Pascal-like language (PL/0) into code for a hypothetical stack-oriented machine. We here employ several methods of proof, different from the previous methods, which are amenable to machine-aided proofs. These new methods include the use of Hoare proof rules to describe the semantics of the source and target languages, as well as the language in which the compiler was written, a new formalization of substitution, and axiomatic definition of functions, both in the compiler and in the assertion language. The machine assistance was provided by the Xivus program verification system, which is a later version of the system described by Good, London, and Bledsoe. We believe the methods of compiler proof given here are of general application in the proving of compilers including such source language features as assignment, conditional, repetition, (WHILE), and go to statements, recursive and non-recursive function calls, and statement- or expression-oriented languages.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1978
- Accession Number
- ADA052911
Entities
People
- Donald S. Lynn
Organizations
- University of Southern California