An approach to compiler correctness
1975; Association for Computing Machinery; Volume: 10; Issue: 6 Linguagem: Inglês
10.1145/390016.808428
ISSN1558-1160
AutoresLaurian M. Chirica, David F. Martin,
Tópico(s)Logic, Reasoning, and Knowledge
ResumoThis paper is a preliminary report on an experiment in applying Floyd's method of inductive assertions to the compiler correctness problem. Practical postfix translators are considered, and the semantics of source and object languages are characterized by Floyd verification conditions. Compiler correctness proofs are partitioned into two parts. The first part deals with proofs of the syntactic and translational phase of compilation, and generates semantic equivalence theorems which are proved in the second part. These techniques are illustrated by a small example.
Referência(s)