Mon, 15 Mar 1993 15:44:57 GMT

Related articles |
---|

Operational Semantics and Compiler Generation. moura@dcs.glasgow.ac.uk (Hermano Moura) (1993-02-26) |

SUMMARY: Operational semantics and compiler generation. moura@dcs.glasgow.ac.uk (Hermano Moura) (1993-03-15) |

Newsgroups: | comp.compilers |

From: | Hermano Moura <moura@dcs.glasgow.ac.uk> |

Keywords: | summary, semantics |

Organization: | Compilers Central |

References: | 93-02-154 |

Date: | Mon, 15 Mar 1993 15:44:57 GMT |

Many thanks to all the kind people who replied to my message about the

use of operational semantics for semantics-directed compiler

generation. Certainly all the messages will be of great help. As many

people demonstrated interest, I include below all the received messages.

Cheers,

-- Hermano Moura

Contribution from John Michael Ashley <jashley@olympus.cs.indiana.edu>

------

The following is the bibliography from the action semantics mailing

list. The book "Action Semantics" has a fairly large bibliography

(althought probably a subset of this one).

Lately, Gurevich has been looking at evolving algebras as an

operational semantics, but I don't believe there has been any work in

generating compilers from such specifications.

------

The mentioned bibliography (action.bib) is available from

ftp.daimi.aau.dk under /pub/action/

Contribution from Kurt Bischoff <bischoff@cs.iastate.edu>:

------

I'm not quite sure what you're looking for ... I've built a tool that

generates semantic analyzers/compilers from attribute grammars. It

generalizes the syntaxes and functionalities of Yacc and Lex. I can

send some information if you're interested.

------

Contribution from Arie van Deursen <Arie.van.Deursen@nl.cwi>:

------

I know of some references which may be of some interest for you.

In Edinburgh D.Berry had his Ph.D. thesis titled ``Generating Program

Animators from Programming Language Semantics'' (1991). He describes

semantics using SOS.

Moreover, at INRIA Sophia-Antipolis the specification formalism Typol

is in heavy use; Officially, Typol is ``natural semantics'', but that

is very close to SOS. Typol specifications can be executed using the

Centaur system. Reference: G.Kahn, ``Natural Semantics'', TACS4, 1987,

LNCS 247, pp 22-39.

Finally, in our group at CWI - Amsterdam we have a lot of experience with

algebraic specifications which we execute as term rewriting systems.

In practice, an executable (functional) term rewriting specification is

very similar to a definition using structural operational semantics.

At the end of the mail, I appended our default "advertisement" folder.

Perhaps it's useful.

The ASF+SDF Project

To allow for programming environments (integrated collections of tools)

that are both easy to obtain and provably correct, it is investigated

how tools can be generated from algebraic specifications of programming

languages.

Algebraic Specification using ASF+SDF

All specifications are algebraic specifications, using the ASF+SDF

formalism. The ASF+SDF formalism combines the elder "Algebraic

Specification Formalism" with the "Syntax Definition Formalism". By

viewing signatures also as grammars, concrete syntax can be used for terms

(e.g., in the equations). The formalism supports modularization,

conditional equations (both positive and negative), and built-in

associative lists. The formalism is suited to provide specifications for

arbitrary abstract data types (traditional algebraic specification), as

well as definitions of any (formal) language (e.g. programming, query,

text-processing, specification, etc.).

The ASF+SDF Meta-environment

A system, called the ASF+SDF Meta-environment, has been built around the

ASF+SDF formalism. It allows for rapid prototyping of ASF+SDF

specifications. >From the signature, parsers are geneated, and from the

equations, term rewriting systems are generated. Terms can be edited using

syntax-directed editors. It is possible to attach specified functionality

to user-interface events such as mouse-clicks, buttons, etc. The ASF+SDF

Meta-environment has an incremental implementation; if the specification

is changed the prototyped tools are adapted rather than regenerated from

scratch. This supports inter-active developing and testing of

specifications. The system is still under development, but stable enough

for external use. A tape with the system is available.

Availability of Reports

There is an annotated bibliography list of abstracts of papers and

publications of the ASF+SDF group. This abstract list can be obtained

by ftp to "ftp.cwi.nl", directory "pub/gipe". In this directory also

electronic versions of several reports can be found.

Some References:

@book{BHK89,

editor = {J.A. Bergstra and J. Heering and P. Klint},

title = {{A}lgebraic {S}pecification},

series = {ACM Press Frontier Series},

publisher = {The ACM Press in co-operation with Addison-Wesley},

year = {1989}}

@inproceedings{Kli91.meta,

author = {P. Klint},

booktitle = {Proceedings of the METEOR workshop on Methods Based on

Formal Specification},

editor = {J.A. Bergstra and L.M.G. Feijs},

pages = {105-124},

publisher = {Springer-Verlag},

series = {Lecture Notes in Computer Science},

title = {A meta-environment for generating programming environments},

volume = {490},

year = {1991},

institution = {Centrum voor Wiskunde en Informatica (CWI)},

type = {Report {CS}-{R}9064}}

@article{HKR90,

author = {J. Heering and P. Klint and J. Rekers},

title = {{I}ncremental generation of parsers},

journal = {IEEE Transactions on Software Engineering},

volume = {16},

number = {12},

pages = {1344-1351},

year = {1990},

note = {Also in: {\it SIGPLAN Notices}, 24(7):179-191, 1989} }

@techreport{Deu92.lambda,

key = {Deu92},

author = {Deursen, A. van},

title = {Specification and Generation of a $\lambda$-calculus

Environment},

institution = {Centrum voor Wiskunde en Informatica (CWI)},

type = {{R}eport {CS}-{R}9233},

address = {Amsterdam},

year = {1992},

note = {Available by {\em ftp} from ftp.cwi.nl: pub/gipe}

*}*

------

Contribution from Trejos-Zelaya <Ignacio.Trejos-Zelaya@uk.ac.oxford.prg>:

------

I'm not directly into that, but some of the following might be useful:

Hannan and Miller. From operational semantics to abstract machines:

preliminary results. Lisp and Functional Programming Conf. 1990.

Hannan and Miller. From operational semantics to abstract machines.

Mathematical Structures in Computer Science 2(4), dec 1992.

(seems to be an extended version of the above one)

Hannan. Staging transformations for abstract machines. Proc. symp.

on partial evaluation and semantics-based program manipulation.

jun 1991 (check Sigplan Notices).

Hannan. Making abstract machines less abstract. Funct. prog. langs.

and computer arch. (5th. conf.) aug 1991. LNCS 523.

Though I don't know how "automatic" the process might be.

I suggest that you also check the work done by Kahn and collaborators on

the Centaur system. It's not compiler generation, but rather both high-

level description of programming environments and tools for (executable)

semantics definitions suitable for prototyping. An article illustrating

the style (oldish):

Kahn. Natural semantics. 4th ann. symp. theo. aspects of Comp. Sci.

LNCS 247. 1987.

They execute (Typol) programs through a translation to Prolog.

Also a thesis shows how to deal with a subclass of Typol programs,

via attribute grammar evaluators:

Attali. Compilation de programmes TYPOL par attribut se'mantiques.

U. Nice. 1989.

On "animation", see Dave Berry's thesis:

Berry. Generating program animators from programming language semantics.

U. Edinburgh. CST-79-91 (ECS-LFCS-91-163)

And on correctness of compilers and debuggers, your compatriot:

da Silva. Correctness proofs of compilers and debuggers: an approach

based on structural operational semantics. U. Edinburgh 1992.

(Our friend Augusto Sampaio told me that da Silva is now at

Recife)

At Oxford, Steve MacKeever (swm@ac.ox.prg) is precisely working on

obtaining compilers automatically from operational semantics.

An I am using a subclass of "inference systems" (by imposing restrictions

on the form of rules) for _programming_, resulting in a simple extension

of Standard ML's purely functional subset of the Core. My notation is

directly executable, though I am not able (yet) to compile it.

I strongly suggest that you contact Steve MacKeever, who is really into

that and might give you useful pointers. His work is very interesting.

------

Contribution from Mitchell Wand <wand@dec5120z.ccs.northeastern.edu>:

------

You might want to look at our paper

@InProceedings{WandOliva92,

author = "Mitchell Wand and Dino P. Oliva",

title = "Proving the Correctness of Storage Representations",

booktitle = "1992 ACM Conference on Lisp and Functional Programming",

year = "1992",

pages = "151--160",

*}*

and at the references therein.

------

Stephen.McKeever@uk.ac.oxford.prg:

------

I haven't published anything yet, however this is exactly what my PhD thesis

is all about. The core idea is based on converting the SOS rules down to

term rewriting machines on which Pass Separation is performed. This technique

was first elaborated for a lambda calculus machine in the following papers:

[1] ``From Operational Semantics to Abstract Machines,'' with Dale Miller.

Invited to appear in a special issue of {\em Mathematical

Structures in Computer Science} dedicated to 1990

ACM Conference on Lisp and Functional Programming.

56 pages. Accepted.

[2] ``Staging Transformations for Abstract Machines.''

In {\em Proceedings of the ACM SIGPLAN Symposium on

Partial Evaluation and Semantics Based Program Manipulation},

ACM SIGPLAN Notices, September 1991.

[3] ``Making Abstract Machines Less Abstract.''

In {\em Proceedings of the ACM Conference on Functional Programming

Languages and Computer Architecture}, Lecture Notes in

Computer Science, Vol. 523, Springer-Verlag, 1991.

It's in some ways the opposite of Action Semantics as we use the semantics

to derive the actions rather then using actions, which have been formally

defined, to define the semantics. This message is rather brief but if you

would like any more assistance then please ask.

------

Contribution from David Bruce <"ISIS::dib"@uk.mod.hermes>:

------

Peter Lee, "Realistic Compiler Generation", MIT Press, 1989, 0-262-12141-7.

(a revision of his 1987 U. Michigan doctoral thesis)

------

Contribution from Fabio Queda Bueno da Silva <fabio@BR.UFPE.DI>:

------

In my PhD thesis I address the problem of compiler correctness using a

variant of Plotkin's Structural Operational Semantics, called Relational

Semantics. In my work I don't address automatic compiler generation

directly, but I believe it may provide a theoretical basis for such

generations. One of the goals of my research was to define a general

criterion for compiler correctness. I used the concept of Observational

Equivalence from algebraic specification to define an equivalence relation

between two Relational Semantics which provides a suitable criterion for

compiler correctness. The thesis gives extensive arguments on why I

believe that is a suitable notion of compiler correctness.

Furthermore, I also defined a powerfull proof method to be used in

compiler correctness proofs. This method also use ideas from algebraic

specification, namely the notion of Strong Correspondences developed

by Oliver Schoett in his PhD thesis.

Another issue in my thesis that might interest you is the evaluation of

Relational Semantics. There the idea is to define an evaluation model

for evaluating semantics which leads to interpreter generation. This

idea is not new and appears in systems like CENTAUR and The Animator

Generator. I studied this problem from a theoretical perspective, and

defined an evaluation model that is proved sound and complete wrt the

model-semantics of Relational Semantics.

Finally, I also studied the problem of debugger specification and

correctness using Relational Semantics. I gave an abstract definition of

debuggers and then defined a language for specification of debuggers. I

also defined an equivalence relation between debuggers based on the

concept of a bisimulation. This provides both a criterion for debugger

correctness and also a proof method for debugger correctness proofs.

If you are interested in these issues my thesis is available from the

department of computer science. There is a small charge to cover

printing costs. There are two LFCS technical reports (free):

one summarizes the PhD thesis and the other discuss compiler correctness

in detail. The references are in BibTeX format:

@PhdThesis{cpcdabsos,

author = "Fabio Q. B. da Silva",

title = "Correctness Proofs of Compilers and Debuggers: an

Approach Based on Structural Operational Semantics",

school = LFCS,

year = "1992",

address = "Edinburgh, EH9 3JZ, Scotland",

month = "September",

note = "Available as LFCS Report Series ECS-LFCS-92-241 or

CST-95-92"

*}*

@TechReport{oecc,

author = "Fabio Q. B. da Silva",

title = "Observational Equivalence and Compiler Correctness",

institution = LFCS,

year = "1992",

OPTtype = "",

number = "ECS-LFCS-92-240",

address = "Edinburgh, EH9 3JZ, Scotland",

month = "September",

OPTnote = "Available from Lorraine Edgar (\ml{lme@dcs.ed.ac.uk})

or in writing to the Department of Computer Science"

*}*

@TechReport{cpcdoabsos,

author = "Fabio Q. B. da Silva",

title = "Correctness Proofs of Compilers and Debuggers: an

Overview of an Approach Based on Structural

Operational Semantics",

institution = LFCS,

year = "1992",

OPTtype = "",

number = "ECS-LFCS-92-233",

address = "Edinburgh, EH9 3JZ, Scotland",

month = "September",

OPTnote = "Available from Lorraine Edgar (\ml{lme@dcs.ed.ac.uk})

or in writing to the Department of Computer Science"

*}*

--

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.