Re: Formal semantics of language semantics

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

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