X-Sieve: CMU Sieve 2.2 X-Sender: linday@linday.pobox.stanford.edu X-Mailer: QUALCOMM Windows Eudora Version 6.1.2.0 Date: Mon, 25 Jul 2005 13:59:35 -0700 To: Rebecca Wesley From: Linda Yamamoto Subject: Re: still not attached Hi Rebecca, Having problems with my reply being rejected by the mail server. Will keep trying. Linda At 01:57 PM 7/25/2005, you wrote: Linda, Sorry still not attached. Rebecca At 01:43 PM 7/25/2005, you wrote: Linda, Do you have the pdf? Can you send it to me? Rebecca At 11:12 AM 7/25/2005, you wrote: Hi Rebecca, Please add the following 3 items to the CS tech report server: 1. To be added to :
Report Number: CS-TR-75-498
Institution: Stanford University, Department of Computer Science
Title: Automatically Proving the Correctness of Translations Involving Optimized Code
Author: Samet, Hanan
Date: May 1975
Abstract: A formalism is described for proving that programs written in a higher level language are correctly translated to assembly language. In order to demonstrate the validity of the formalism a system has been designed and implemented for proving that programs written in a subset of LISP 1.6 as the high level language are correctly translated to LAP (an assembly language for the PDP-10) as the low level language. This work involves the identification of critical semantic properties of the language and their interrelationship to the instruction repertoire of the computer executing these programs. A primary use of the system is as a postoptimization step in code generation as well as a compiler debugger.
The assembly language programs need not have been generated by a compiler and in fact may be handcoded. The primary restrictions on the assembly language programs relate to calling sequences and well-formedness. The assembly language programs are processed by a program understanding system which simulates their effect and returns as its result a representation of the program in the form of a tree.
The proof procedure is independent of the intermediary mechanism which translates the high level language into the low level language. A proof consists of applying valid transformations to show the equivalence of the forms corresponding to the assembly language program and the original higher level language program, for which there also exists a tree-like intermediate form.
Some interesting results include the ability to handle programs where recursion is implemented by bypassing the start of the program, the detection and pinpointing of a wide class of errors in the assembly language programs, and a deeper understanding of the question of how to deal automatically with translations between high and extremely low level languages.
This disseration was submitted to the Department of Computer Science and the Committee on Graduate Studies of Stanford University in partial fulfillment of the requirements for the degree of Doctor of Philosophy.
CS-TR-75-498
2. To be saved and loaded as : Report Number: CS-TR-75-498 Institution: Stanford University, Department of Computer Science Title: Automatically Proving the Correctness of Translations Involving Optimized Code Author: Samet, Hanan Date: May 1975 Abstract: A formalism is described for proving that programs written in a higher level language are correctly translated to assembly language. In order to demonstrate the validity of the formalism a system has been designed and implemented for proving that programs written in a subset of LISP 1.6 as the high level language are correctly translated to LAP (an assembly language for the PDP-10) as the low level language. This work involves the identification of critical semantic properties of the language and their interrelationship to the instruction repertoire of the computer executing these programs. A primary use of the system is as a postoptimization step in code generation as well as a compiler debugger. The assembly language programs need not have been generated by a compiler and in fact may be handcoded. The primary restrictions on the assembly language programs relate to calling sequences and well-formedness. The assembly language programs are processed by a program understanding system which simulates their effect and returns as its result a representation of the program in the form of a tree. The proof procedure is independent of the intermediary mechanism which translates the high level language into the low level language. A proof consists of applying valid transformations to show the equivalence of the forms corresponding to the assembly language program and the original higher level language program, for which there also exists a tree-like intermediate form. Some interesting results include the ability to handle programs where recursion is implemented by bypassing the start of the program, the detection and pinpointing of a wide class of errors in the assembly language programs, and a deeper understanding of the question of how to deal automatically with translations between high and extremely low level languages. This disseration was submitted to the Department of Computer Science and the Committee on Graduate Studies of Stanford University in partial fulfillment of the requirements for the degree of Doctor of Philosophy. ftp://reports.stanford.edu/pub/cstr/reports/cs/tr/75/498/CS-TR-75-498.pdf 3. Please add or forward to Andy to add the file to the server (attached). Please let me know when this is done. If possible please have them uploaded by the end of this week. We're trying to get it ready for a conference this weekend. Thanks much, Linda ---------------------------------------------------------------- Linda Yamamoto Head Librarian & Bibliographer Mathematical & Computer Sciences Library Stanford University 650.723.0864 650.725.8998 fax