Skip Navigation

The Computer Journal 1979 22(3):240-245; doi:10.1093/comjnl/22.3.240
© 1979 by British Computer Society
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrow Search for citing articles in:
ISI Web of Science (2)
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Deransart, P.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

Proof by semantic attributes of a LISP compiler

P. Deransart *

IRIA, Domaine de Voluceau, BP 5-Rocquencourt, Le Chesnay, France

This paper illustrates the possibility to prove correctness of a compiler defined by semantic attributes. Source language and object code are first described. The source language corresponds to LISP compilable functions and the object code to an abstract machine. Then the translation between them is defined and the proof technique is described and illustrated by some examples. The interest of this technique is the modularity of the proof.

Cet article montre comment il est possible de prouver la correction d'un compilateur décrit par attributs sémantiques. Le language source et le code objet sont introduits en premier lieu. Le premier correspond aux fonctions LISP compilables et le second à une machine abstraite. La traduction de l'un dans l'autre est ensuite définie et la méthode de preuve est exposée. L'intérêt de cette méthode repose sur l'extrême modularité de ce type de preuve.

Received September 1977.

* IRIA, Domaine de Voluceau, BP 5-Rocquencourt, 78150 Le Chesnay, France


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.