SUMMARY: Operational semantics and compiler generation.

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"
}
--

Return to the comp.compilers page.
Search the comp.compilers archives again.