Re: Formal semantics of language semantics

"Joe Hendrix" <j*lstnme*@uiuc.edu> writes:
> Are there any notations commonly used to define the semantics of a
> programming language? (Similar to how BNF defines the syntax).


I'm not sure any of the notations that have been proposed are commonly
used. A couple of languages which do have a formal definition of the
semantics as part of the language definition are: Algol 68 which is
defined [rrala68:1976] using two level grammars
(http://www.cwi.nl/~steven/vw.html) and Scheme which is defined
(http://www.schemers.org/Documents/Standards/R5RS/HTML/) using
denotational semantics
(http://www.cl.cam.ac.uk/Teaching/Lectures/dens/dens.ps.gz).


A gentle introduction to various notations used for the
semantics of programming languages can be found in [Watt:plss:1991].
This covers denotational semantics, structured operational semantics
(http://www.daimi.aau.dk/~pdm/ModularSOS.html) and action
semantics (http://www.brics.dk/Projects/AS/).


Various attempts have been made to produce specific tools to support
one particular approach or another. For example, Centaur
(http://www-sop.inria.fr/croap/centaur/centaur.html) and Typol
[Despeyroux:sdt:1984] for natural semantics and [Paulson:acm:popl:1982],
[Bodwin:Bradley:Kanda:Litle:Pleban:acm:cc:1982] and
[Michaelson:phd:1993] all produced systems for executing denotational
semantics and a list of action semantics tools can be found at
http://www.brics.dk/Projects/AS/AvailableTools.html.


Some have suggested that one might as well use an existing
(programming) language in which to write language defintions e.g.
Algol 68 [Pagan:bcs:cj:1979] and Prolog [Moss:acm:lfp:1982].


There are also some notations/approaches that concentrate specifically
on the static semantics of programming languages
e.g. [Rosslet:phd:1984], [Odersky:phd:1989] and
[Poetzsch-Heffter:plilp:1991].


You might notice most of the references I gave are at least 10 years
old. That is not meant to imply that no work has been done since
then, only that I haven't followed the area in any detail since then.




@book
{ rrala68:1976
, editor= "van Wijngaarden, A and B. J. Mailloux and J. E. L. Peck
                            and C. H. A. Koster and M. Sintzoff and C. H. Lindsey and
                            L. G. L. T. Meertens and R. G. Fisker"
, title= "Revised Report on the Algorithmic Language Algol 68"
, publisher= "Springer-Verlag"
, year= 1976
, refs= 19
, source= "own"
, isbn= "3-540-07592-5"
, isbn= "0-387-07592-5"
, errata= "My (second hand) copy came with a single sheet in it
    containing some corrections."
, sjb= "In section 0.4.1 it is noted that ``predicates'' have
    been introduced to the two-level-grammar. With these it has been
    possible to remove all ``context conditions'' contained in the
    original report."
, reffrom= Tafvelin:bit:1976
, reffrom= Pagan:bcs:cj:1979
, reffrom= Williams:acm:toplas:jan:1982
, reffrom= Allison:pids:1986
, reffrom= Garrison:phd:1987
}


@string{bcs:cj = "The Computer Journal"}


@article
{ Pagan:bcs:cj:1979
, author= "F. G. Pagan"
, title= "Algol 68 as a metalanguage for denotational semantics"
, journal= bcs:cj
, volume= 22
, pages= "63--66"
, year= 1979
, refs= 12
, checked= 19971222
, source= "Main Library, University of Manchester"
, abstract= "The possibility of using ALGOL 68 as a metalanguage for
``denotational'' definitions of the semantics of programming languages
is considered, using the simple language LOOP as an example. The
approach is found to be a viable one if the ``partial
parameterisation'' feature is added to ALGOL 68. The advantages of
using a general purpose programming language as a definitional medium
are briefly discussed."
, sjb= "Many take the view that formal definitions should be
expressed in terms of a meta-language, possibly an actual programming
languages itself.
See~\cite{Anderson;Belz:Blum:acta:1976,Pagan:bcs:cj:1976} for
this view in an operational (implementation oriented view)
and~\cite{Mosses:focs:1975} who proposes a specially designed
language.


The author considers that this may be viewed as an extension
of~\cite{Pagan:bcs:cj:1976}. The author is not concerned with the
adequacy of the denotational approach, only with how ALGOL serves as
its meta-lanugage.


Examples are given for a simple language LOOP (used
in~\cite{Tennent:cacm:1976}). Algol 68 per se, is difficult to work
with, but with the extension of ``partial
parameterisation''~\cite{Lindsey:ab:1974,Lindsey:ab:1976} to allow
closures to be generated, the language is much more useful.


The main advantage of using a programming language is that the
resulting definition is executable (or at least ``compilable'', it may
be that execution is so inefficient that it is to all intents and
purposes impossible). This helps construct a clear, consistent,
``bug-free'' specification. The author claims that a ``mainstream''
language like ALGOL is better than, say Lisp, as it has strong
typechecking.


The paper closes with a note about the implementation of the ALGOL
definition given in the paper. For the example of \(\lambda x 2x + 2\)
in LOOP, it takes about 70 function calls with a recursion depth of
18."
, reffrom= Pagan:spe:1984
, reffrom= Allison:pids:1986
, reffrom= Watt:spe:1986
}


@inproceedings
{ Mosses:icfpc:1981
, author= "Peter. Mosses"
, title= "A semantic algebra for binding constructs"
, crossref= "icfpc:1981"
, pages= "408--418"
, refs= 4
, checked= 19960317
, source= "Main Library, University of Manchester"
, keywords= "programming languages, semantics, abstract data types,
    formalization of programming concepts, algebras, binding constructs"
, abstract= "This paper presents a sesmantic algebra, suitable for use
    in giving the denotational semantics of various forms of
    declarations and binding constructs in programming languages. The
    emphasis of the paper is on the development of semantic descriptions
    which are easy to understand at an intuitive level, being based on
    algebraic operators corresponding to fundamental concepts of
    programming languages. Some familiarity with denotational semantics
    and abstract data types is assumed."
, sjb= "Early work on action semantics."
, reffrom= Sethi:acm:cc:1982
, reffrom= Watt:spe:1986
}


@proceedings
{ icfpc:1981
, editor= "J. D{\'i}az and I. Ramos"
, title= "Formalization of Programming Concepts"
, publisher= "Springer Verlag"
, series= lncs
, volume= 107
, year= 1981
}


@inproceedings
{ Paulson:acm:popl:1982
, author= "L. Paulson"
, title= "A Semantics-Directed Compiler Generator"
, crossref= "acm:popl:1982"
, pages= "224--233"
, checked= 19940215
, source= "Computer Science Library, University of Manchester"
, sjb= "Overview of Paulson's thesis work. This is a merge of a
    functional language and an LALR parser so that the denotational
    semantics of the language can be written around the concrete syntax
    (eek!). Notes that perhaps the static and dynamic semantics could
    be separated, but this is on the grounds of efficiency!"
, reffrom= Ganzinger:Giegerich:Moncke:Wilhelm:acm:cc:1982
, reffrom= Bahlke:Moritz:Snelting:iait:1987
, reffrom= Raskovsky:acm:cc:1982
, reffrom= Ganzinger:Giegerich:acm:cc:1984
, reffrom= Pleban:acm:cc:1984
, reffrom= Wand:acm:cc:1984
, reffrom= Schmidt:ds:1986
, reffrom= Kaiser:acm:toplas:1989
, reffrom= Rosendahl:agata:1990
}


@proceedings
{ acm:popl:1982
, title= "Conference Record of the Ninth Annual ACM Symposium
on Principles of Programming Languages"
, booktitle= "Conference Record of the Ninth Annual ACM Symposium
on Principles of Programming Languages"
, organization= "ACM"
, publisher= "ACM"
, source= "Computer Science Library, University of Manchester"
, month= jan
, year= 1982
, sjb= "The papers were not formally refereed but were
accepted on the basis of extended abstracts."
}


@inproceedings
{ Moss:acm:lfp:1982
, author= "Christopher D. S. Moss"
, title= "How to Define a Language using PROLOG"
, crossref= "acm:lfp:1982"
, pages= "67--73"
, refs= 22
, checked= 19940213
, source= "Computer Science Library, University of Manchester"
, keywords= "Prolog, programming language definition,
    dynamic semantics, context conditions"
, sjb= "Effectively proposes Prolog as a meta-language for
    describing {\em all} aspects of a formal language, from the lexical,
    through the syntactic, context conditions and dynamic semantics.
    The actual methods used in each case is the standard recursive
    approach using and passing an environment to handle name resolution.
    Uses some syntactic sugar to sweeten the notation."
}


@inproceedings
{ Bodwin:Bradley:Kanda:Litle:Pleban:acm:cc:1982
, author= "James Bodwin and Laurette Bradley and Kohji Kanda and
Diane Litle and Uwe Pleban"
, title= "Experience with an Experimental Compiler Generator Based
on Denotational Semantics"
, crossref= "acm:cc:1982"
, pages= "216--229"
, refs= 23
, checked= 19940216
, source= "Computer Science Library, University of Manchester"
, abstract= "Compiler generation based on formal semantics has
    received considerable attention in recent years from a number of
    semanticists. Compiler writers, on the other hand, know relatively
    little about these efforts. This paper tries to remedy this
    situation by discussing our experimentation with the Semantics
    Implementation system (SIS) of Peter Mosses. SIS allows the user to
    generate a complete compiler from a formal specification of the
    syntax and semantics of a programming language. In particular, the
    translator component of a compiler is obtained by directly
    implementing a denotational semantics. Consequently, a compiler is
    expressed as a higher order function. A program is compiled by
    formally applying the compiler to a tree representation of the
    program and simplifying this application. The experimentation with
    SIS indicates that compiler generation based on denotational
    semantics is feasible, though not yet viable. We argue that SIS
    constitutes an important first step towards the automatic
    construction of provably correct, complete, and reasonably efficient
    compilers from formal syntactic and semantic specifications."
, sjb= "Allows a complete compiler to be generated from a syntax
    and semantic definition of a language. The generator takes as its
    input three definitions, and from these produces a compiler for the
    language.


    \begin{enumerate}
    \item A BNF description of the language. This is given in GRAM, an
                extension of standard BNF.
    \item A description of the static semantics of the language. This is
                given in the language DSL.
    \item A description of the dynamic semantics of the language. This is
                also given in DSL.
    \end{enumerate}


    To check a program in the desired language, it is passed through a
    lexer, a parser and a tree builder. Once these three phases are
    complete the parse-tree is passed to a function which checks the
    static semantics of the language, by walking the tree. When an
    error is discovered, processing stops and no indication is given as
    to what or where the error was. This is due to the way the semantic
    checks are defined (they are purely boolean functions and thus have
    no output at all).


    The designers of SIS regard it as a tool for debugging small
    denotational definitions rather than as a means for generating
    production compilers. This is mainly due to the inefficient way
    some of the stages of parsing are done.


    A more efficient system, called GENSIS, based on SIS and tools such
    as Lex and YACC, has been designed, but as yet has not been
    implemented."
, reffrom= Clinger:acm:lfp:1984
, reffrom= Pleban:acm:cc:1984
, reffrom= Reiss:acm:cc:1984
, reffrom= Rosslet:phd:1984
, reffrom= Wand:acm:cc:1984
, reffrom= Schmidt:ds:1986
, reffrom= Kaiser:acm:toplas:1989
}


@proceedings
{ acm:cc:1982
, title= "Proceedings of the SIGPLAN '82 Symposium on Compiler
Construction"
, booktitle= "Proceedings of the SIGPLAN '82 Symposium on Compiler
Construction"
, organization= "ACM"
, publisher= "ACM"
, source= "Computer Science Library, University of Manchester"
, year= 1982
, note= "Available as SIGPLAN Notices 17(6) June 1982."
, sjb= "Note that the papers were not formally refereed."
}


@proceedings
{ acm:lfp:1982
, title= "Conference Record of the 1982 ACM Symposium on Lisp
and Functional Programming"
, booktitle= "Conference Record of the 1982 ACM Symposium on Lisp
and Functional Programming"
, organization= "ACM"
, publisher= "ACM"
, month= aug
, year= 1982
, source= "Computer Science Library, University of Manchester"
, sjb= "The papers were not formally refereed but were
    accepted on the basis of extended abstracts."
}


@inproceedings
{ Despeyroux:sdt:1984
, author= "Thierry Despeyroux"
, title= "Executable Specification of Static Semantics"
, crossref= "sdt:1984"
, pages= "215--233"
, refs= 23
, source= "partial copy / Main Library, University of Manchester"
, keywords= "Typol, natural semantics"
, reffrom= Aho:Sethi:Ullman:cptt:1986
, reffrom= Bahlke:Snelting:acm:toplas:1986
, reffrom= Kaiser:acm:toplas:1989
, reffrom= Attali:Chazarain:agata:1990
, reffrom= Grosch:Snelting:plilp:1990
, reffrom= Snelting:acta:1991
, reffrom= Poetzsch-Heffter:munich:222:1992
, reffrom= Odersky:acm:toplas:1993
}


@proceeedings
{ sdt:1984
, editor= "G. Kahn and D. B. MacQueen and G. Plotkin"
, title= "Semantics of Data Types"
, publisher= "Springer Verlag"
, series= lncs
, volume= 173
, year= 1984
, reffrom= Allison:pids:1986
, reffrom= Schmidt:ds:1986
, reffrom= Field:Harrison:fp:1988
}


@phdthesis
{ Rosslet:phd:1984
, author= "Jonathan Alan Rosselet"
, title= "Definition and Implementation of Context Conditions for
                              Programming Languages"
, school= "University of Toronto, Canada"
, year= 1984
, checked= 19940313
, source= "Inter-library loan"
, supervisor= "R. C. Holt"
, examiner= "J. V. Guttag"
, abstract= "Context conditions are the parts of a language that
    cannot be described by a grammar e.g. scope rules, type
    compatibility, aliasing, \ldots etc. Context condition play an
    increasingly important role in language definitions.


    A syntax directed approach is given using the meta-language ADL.
    This is strongly typed and can be mechanically verified. ADL has
    first order semantics and therefore proofs can be done on it. Has
    an operational semantics, so it can be executed.


    A definition of Turing and ADL has been done in ADL. ADL compiler
    (maps to RLisp) has been implemented. Parts of the Turing
    definition has been verified by mapping to a Concurrent Euclid
    verifier system."
}


@book
{ Odersky:phd:1989
, author= "Martin Odersky"
, title= "A New Approach to Formal Language Definition and its
Application to Oberon"
, publisher= "Verlag de Fachvereine"
, year= 1989
, source= "original"
, checked= 19940225
, note= "(Revised?) version of authors Ph.D thesis."
, abstract= "This thesis presents a new method and notation for the
definition of the syntax of programming languages. With syntax, we
mean the set of all rules which determine whether a text belongs a
given language. A subset of these rules is commonly and successfully
defined with context-free grammars. For other areas, like scope- or
type-rules, there does not yet exist a satisfactory formalism.


Our method, CADET, is based on the idea that predicate calculus can be
employed for the characterization of legal derivation trees. A
context-free grammar is used for defining a superset of a given
language, which is then restricted by imposing legality criteria on
derivation trees. The critera are expressed with logic predicates
which we call context-rules. A text belongs to the defined language
if and only if its derivation tree is a model of all context-rules.


A CADET language definition is precise and often considerably shorter
than definitions with other formal methods. Its structure can be
closely related to descriptions formulated in natural language.


The first part of this thesis contains a detailed introduction to the
CADET notation and a critical comparison with other methods. In the
second part, we present a commented CADET definition of the
programming language Oberon~\cite{Wirth:spe:tplo:1988}. The results
obtained from this first application of our method are quite
encouraging: the complete Oberon definition has a size of
approximately 700 lines.


In the final part of the thesis we discuss a rule checking program
which generates from a CADET specification the analysis part of a
compiler. The program is used for determining whether test-inputs
belong to the defined language. Test runs can be a valuable help in
locating and correcting errors in a definition."
, reffrom= Poetzsch-Heffter:plilp:1991
, reffrom= Poetzsch-Heffter:munich:222:1992
, reffrom= Poetzsch-Heffter:iccc:1992
, reffrom= Odersky:acm:toplas:1993
}


@inproceedings
{ Poetzsch-Heffter:plilp:1991
, author= "Ard Poetzsch-Heffter"
, email= "poetzsch@informatik.tu-muenchen.de"
, title= "Implementing High-Level Identification Specifications"
, crossref= "plilp:1991"
, pages= "63--74"
, refs= 12
, source= "copy"
, checked= 19940313
, abstract= "The paper describes a new, declarative method for the
    formal specification of visibility rules. In contrast to common
    methods that are based on the specification of a symboltable (or
    environment), of appropriate update operations and of passing rules,
    the presented method is related to visibility descriptions in
    language reports. It consists of three steps: First, the program
    entities are specified, i.e. the candidates for the meaning of an
    identifier; the next step defines the ranges where the program
    entities are valid or hidden; finally, visibility is expressed in
    terms of these ranges. To formally define the semantics of these
    visibility specifications, a model theoretic view of abstract syntax
    trees is sketched. Using this framework, we give a fixpoint
    semantics for such specifications."
, reffrom= Poetzsch-Heffter:munich:222:1992
, reffrom= Poetzsch-Heffter:iccc:1992
, reffrom= Poetzsch-Heffter:plilp:1993
}


@proceedings
{ plilp:1991
, editor= "J. Maluszyn{\'n}ski and M. Wirsing"
, title= "Programming Language Implementation and Logic Programming"
, booktitle= "Programming Language Implementation and Logic Programming"
, year= 1991
, note= "LNCS 528"
}


@book
{ Watt:plss:1991
, author= "David A. Watt"
, title= "Programming Language Syntax and Semantics"
, publisher= "Prentice-Hall"
, year= 1991
, refs= 58
, source= "own"
, checked= 19960310
, isbn= "0-13-726274-4"
, blurb= "Programming Language Syntax and Semantics introduces
methods for formaly specifying the syntax and semantics of programming
languages.


Chapter 2 introduces the topic of syntax, covering both context-free
grammars and regular expressions. Chapters 3-5 introduce denotational
semantics, the most commonly used method for specifying semantics.
Chapter 6 introduces algebraic semantics, applying it to specify new
data types. Chapters 7-8 introduce action semantics, a new method
that promises to make semantic specifications unusually readable. the
text concentrates on practical specification techniques, but the
underlying theory is briefly covered where appropriate.


Numerous examples, exercises, and case studies support the text."
}


@phdthesis
{ Michaelson:phd:1993
, author= "Gregory Michaelson"
, email= "greg@cee.hw.ac.uk"
, title= "Interpreter prototypes from formal language definitions"
, school= "Heriot-Watt University"
, month= apr
, year= 1993
, pages= 160
, source= "URL"
, url= "ftp://ftp.cee.hw.ac.uk/pub/funcprog/gjm.phd.ps.Z"
, checked= 19930302
, abstract= "Denotational semantics is now used widely for the formal
    definition of programming languages but there is a lack of
    appropriate tools to support language development. General purpose
    language implementation systems are oriented to syntax with poor
    support for semantics. Specialised denotational semantics based
    systems correspond closely to the formalism but are rendered
    inflexible for language experimentation by their monolithic multiple
    stages.


    Exploratory language development with formal definitions is better
    served by a unitary notation, encompassing syntax and semantics,
    which is close to but simpler than denotational semantics.
    Interactive implementatin of the notation then facilitates language
    invenstigation through the direct execution of a formal definition
    as an interpreter for the defined language.


    This thesis presents Navel, a run-time typed, applicative order,
    pure functional programming language with integrated context free
    grammar rules. Navel has been used to develop prototype
    implementations from substantial language definitions, including for
    Navel itself. The Navel implementation achieves a performance which
    enables interactive language experimentation and compares well with
    that of contemporaneous declarative language implementations.


    Denotational semantics does not address concrete syntax issues and
    denotational semantics based systems either ignore orhave ad-hoc
    provision for context sensitivity. In Navel, rules are full
    values. Abstraction over rules enables the concise expression of
    context sensitivity in a style similar to dynamic syntax."
, sjb= "Not clear to me why a) Navel is any better than using an
    existing (functional) programming language to define the
    denotational semantics (preferably ML/Haskell with a simple
    combinator parser) and b) why Navel isn't compared with Typol (even
    though the latter is based on structured operational semantics)."
}

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