Re: Reuse of Semantic Specifications

pdm@daimi.aau.dk (Peter D. Mosses)
Tue, 2 May 1995 13:42:37 GMT

          From comp.compilers

Related articles
Reuse of Semantic Specifications vaidyana@willis.cis.uab.edu (1995-04-28)
Re: Reuse of Semantic Specifications pdm@daimi.aau.dk (1995-05-02)
Re: Reuse of Semantic Specifications Martin.Jourdan@inria.fr (1995-05-03)
Re: Reuse of Semantic Specifications reidmp@athena.mit.edu (1995-05-16)
| List of all articles for this month |

Newsgroups: comp.specification,comp.object,comp.compilers,comp.lang.functional
From: pdm@daimi.aau.dk (Peter D. Mosses)
Summary: `action semantics' supports reusing semantic specifications!
Keywords: semantics
Organization: DAIMI, Computer Science Dept. of Aarhus Univ.
References: 95-04-154
Date: Tue, 2 May 1995 13:42:37 GMT

vaidyana@willis.cis.uab.edu (Viswanathan Vaidyana) writes:


> I am working on a project of developing a framework for Reusing Semantic
> Specifications of one programming language in order to define that of
> another. I am developing an object-oriented framework (or semantic
> workbench, if you may) from which it will be easy to design the semantics
> of different languages.
>
> I am interested in knowing about any other work in this area
> of reusing specifications of languages, reusing compiler components, etc.


The large-scale reuse of semantic descriptions - quite impractical in
most semantic frameworks - is well supported by the framework of
`action semantics'. The same goes for the closely related issues of
modifying or extending the semantic description of a single language,
often necessary during the development of larger semantic descriptions.


Perhaps it is worthwhile to recall the main pragmatic problems with
denotational semantics. (Skip the rest of this paragraph if you
aren't familiar with that framework.) There, the semantic entities
are generally (higher-order) functions, expressed using a typed
lambda-notation. To specify the semantics even of something as simple
as statement sequencing in imperative languages, one has to be aware
of the *chosen* representation of statements in terms of pure
functions - because e.g. the form of composition needed in so-called
`direct semantics' is precisely the opposite of that needed in
`continuation semantics'! Such dependency of the notation used (to
express such fundamental operational concepts as sequencing) on
details of the chosen representation, is contrary to common principles
of information hiding, and the resulting lack of modularity causes
many of the pragmatic problems that make it very difficult to `scale
up' to denotational descriptions of larger, realistic programming
languages.


How does action semantics avoid such problems? Two key points:


* It uses `actions' as semantic entities, instead of pure mathematical
functions. Actions directly support concepts such as sequential
execution, imperative updates, scope rules for bindings,
communication, nondeterminism, etc. Thus there is no choice about how
to represent statements: simply as actions!


* The combinator-based notation used to express actions is such that
e.g. sequential execution is indicated by the same symbol, regardless
of how `rich' the actions being sequenced might be. Even if statements
are extended to become nondeterministic, or to involve communication
between processes, we continue expressing statement sequencing by the
same semantic equation, viz.:


    execute [[ S1:Statement ";" S2:Statement ]] =
                    execute S1 and then execute S2 .


The action combinator `and then' has a fixed *operational*
interpretation (in contrast to composition in lambda-notation).
Action combinators are provided for most other fundamental concepts,
e.g., implementation-dependent order, nondeterministic choice,
iteration.


For further information about action semantics, see e.g.,
    - P. D. Mosses, Action semantics, Tracts in TCS 26,
        Cambridge University Press, 1992
    - D. A. Watt, Programming language syntax and semantics,
        Prentice Hall, 1991
    - http://www.daimi.aau.dk/~thales/as/AS.html


Apart from action semantics, it seems to me that `evolving algebra
semantics' is the only semantic description framework seriously
supporting reuse (the notation used for expressing updates on
configurations is independent of their structure), see e.g.,
    - Y. Gurevich, Evolving algebras 1993: Lipari Guide. Specifi-
        cation and Validation Methods, E. B\"orger, editor, Oxford
        University Press, 1994
    - http://www.engin.umich.edu/~huggins/ea/


BTW, the above references are taken from Peter Baumann's list
concerning frameworks for formal semantics of real-world programming
languages, available at http://www.ifi.unizh.ch/groups/baumann/sol.html.
(I'll be sending him references to existing complete action semantic
descriptions, such as for Pascal and ANDF, real soon now... in the
meantime, you can find them through the action semantics page cited above.)


I hope that some of this will be useful to you, and that proponents of
other semantic frameworks supporting reuse will post their responses
to the net - I guess comp.specification is the right place for follow-up
technical discussions. But I'm currently quite busy with TAPSOFT '95
organization (see http://www.brics.aau.dk/tapsoft/ :-) so don't expect
much further response from me until after that finishes, at the end of May.


Cheers


========= Peter D. Mosses | pdmosses@brics.aau.dk |
==== ==== BRICS | BRICS: Basic Research |
========= Dept. of Computer Science | in Computer Science |
==== ==== University of Aarhus | Phone: +45 8942 3360 |
==== ==== Ny Munkegade, Bldg. 540 | Direct: +45 8942 3364 |
==== ==== DK-8000 Aarhus C, Denmark | Fax: +45 8942 3255 |
--


Post a followup to this message

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