|Formal semantics of language semantics email@example.com (Joe Hendrix) (2002-09-25)|
|Re: Formal semantics of language semantics firstname.lastname@example.org (Martin v. =?iso-8859-1?q?L=F6wis?=) (2002-09-29)|
|Re: Formal semantics of language semantics email@example.com (Nick Maclaren) (2002-09-29)|
|Re: Formal semantics of language semantics firstname.lastname@example.org (Ingo Dittmer) (2002-09-29)|
|Re: Formal semantics of language semantics email@example.com (Joachim Durchholz) (2002-09-29)|
|Re: Formal semantics of language semantics firstname.lastname@example.org (Stephen J. Bevan) (2002-09-29)|
|Re: Formal semantics of language semantics email@example.com (Lex Spoon) (2002-09-29)|
|Re: Formal semantics of language semantics firstname.lastname@example.org (Mark) (2002-09-29)|
|RE: Formal semantics of language semantics email@example.com (Quinn Tyler Jackson) (2002-10-13)|
|[15 later articles]|
|From:||"Nick Maclaren" <firstname.lastname@example.org>|
|Date:||29 Sep 2002 15:44:23 -0400|
|Organization:||University of Cambridge, England|
|Posted-Date:||29 Sep 2002 15:44:23 EDT|
Joe Hendrix <email@example.com> 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
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 :-(
University of Cambridge Computing Service,
New Museums Site, Pembroke Street, Cambridge CB2 3QH, England.
Tel.: +44 1223 334761 Fax: +44 1223 334679
Return to the
Search the comp.compilers archives again.