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).
>
> 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.




I found Benjamin Pierce's new book "Types and Programming Languages"
be an excellent introduction to specifying and using semantics, as
well as on types. It's aimed at a fairly low reading level, so that
you don't need a math degree to understand it.


I have no idea how well the methods in the book scale to larger, more
complicated programming languages. In industry, everyone seems to use
natural language most of the time. Then, if they really want a formal
sematics, then they may write one up in a theorem prover such as HOL.
These after-the-fact semantics are almost certainly horrendous to
read, though I admit I haven't even bothered to try. It's interesting
to consider what it wold be like if languages were formally specified
from the beginning.


On the other hand, it is common that formalizing an existing spec will
point out ambiguities or unintentional "features" of the language.
Someone (I forget who) formalized SML--a relatively clean
language!--and found several problems with it. It was the same fellow
who wrote an SML interpreter that didn't require static typing.




Lex Spoon

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