Re: Formal semantics of language semantics

"Nick Maclaren" <nmm1@cus.cam.ac.uk>
29 Sep 2002 15:44:23 -0400

          From comp.compilers

Related articles
Formal semantics of language semantics j*lstnme*@uiuc.edu (Joe Hendrix) (2002-09-25)
Re: Formal semantics of language semantics loewis@informatik.hu-berlin.de (Martin v. =?iso-8859-1?q?L=F6wis?=) (2002-09-29)
Re: Formal semantics of language semantics nmm1@cus.cam.ac.uk (Nick Maclaren) (2002-09-29)
Re: Formal semantics of language semantics i.dittmer@fh-osnabrueck.de (Ingo Dittmer) (2002-09-29)
Re: Formal semantics of language semantics joachim_d@gmx.de (Joachim Durchholz) (2002-09-29)
Re: Formal semantics of language semantics stephen@dino.dnsalias.com (Stephen J. Bevan) (2002-09-29)
Re: Formal semantics of language semantics lex@cc.gatech.edu (Lex Spoon) (2002-09-29)
Re: Formal semantics of language semantics whopkins@alpha2.csd.uwm.edu (Mark) (2002-09-29)
RE: Formal semantics of language semantics qjackson@shaw.ca (Quinn Tyler Jackson) (2002-10-13)
[15 later articles]
| List of all articles for this month |

From: "Nick Maclaren" <nmm1@cus.cam.ac.uk>
Newsgroups: comp.compilers
Date: 29 Sep 2002 15:44:23 -0400
Organization: University of Cambridge, England
References: 02-09-149
Keywords: semantics
Posted-Date: 29 Sep 2002 15:44:23 EDT

Joe Hendrix <j*lstnme*@uiuc.edu> wrote:
>Are there any notations commonly used to define the semantics of a
>programming language? (Similar to how BNF defines the syntax).
>
>Has there been much work on figuring out what the requirements for
>such a notation? This seems like it would be a relatively active area
>due to the current industry focus on common language runtimes, but I
>haven't found any good links in my brief google searches.


Sigh, no :-( I asked precisely your question and spent some time
tracking down what was available. Here is a summary of what I
found:


        1) Almost all languages are defined formally at the syntax level
only (if at all), and use hand-waving descriptions for the semantics.
Yes, I do mean hand-waving, because their English (or whatever) is
almost always ambiguous to anyone who doesn't know the background.
Some are better, and some are worse, as usual.


        2) The program-proving and formal semantics people DO specify
things precisely, but use a gratuitously perverse set of notations
that cannot easily be linearised, let alone handled as plain text
or read by a non-specialist. I have spent some hours studying
recommended books, only to discover that the first half was simply
truisms hidden behind that notation. There may be better ones, but
I don't have infinite time to waste.


        3) There were quite a few reasonable projects without that
failing, but all tackled only one or two of the simpler tasks, such
as specifying the domain of a type. I found none that would help
with what I was looking for, which is the specification of aliasing
and parallelism constraints.


My guess is that the second approach would pay if you have a year to
spend learning the notation and the use of its tools. Whether you
would then be able to use it for a programming language that was
not designed ab initio to be described by that notation, I don't know.
It has often been claimed to be possible but, as far as I know, has
never been done for any of the mainstream languages.


If any acolytes of that religion wish to take me to task on this one
by Email, I should welcome them. But PLEASE don't waste your time
and mine by telling me of the innumerable projects that have put the
more-or-less trivial semantics of (say) Fortran or C into such a
notation and have then claimed that the rest can be done similarly.
I wish that it could be :-(




Regards,
Nick Maclaren,
University of Cambridge Computing Service,
New Museums Site, Pembroke Street, Cambridge CB2 3QH, England.
Email: nmm1@cam.ac.uk
Tel.: +44 1223 334761 Fax: +44 1223 334679


Post a followup to this message

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