|Formal semantics of language semantics firstname.lastname@example.org (Joe Hendrix) (2002-09-25)|
|Re: Formal semantics of language semantics email@example.com (Martin v. =?iso-8859-1?q?L=F6wis?=) (2002-09-29)|
|Re: Formal semantics of language semantics firstname.lastname@example.org (Nick Maclaren) (2002-09-29)|
|Re: Formal semantics of language semantics email@example.com (Ingo Dittmer) (2002-09-29)|
|Re: Formal semantics of language semantics firstname.lastname@example.org (Joachim Durchholz) (2002-09-29)|
|Re: Formal semantics of language semantics email@example.com (Stephen J. Bevan) (2002-09-29)|
|Re: Formal semantics of language semantics firstname.lastname@example.org (Lex Spoon) (2002-09-29)|
|Re: Formal semantics of language semantics email@example.com (Mark) (2002-09-29)|
|[15 later articles]|
|From:||"Martin v. =?iso-8859-1?q?L=F6wis?=" <firstname.lastname@example.org>|
|Date:||29 Sep 2002 15:37:59 -0400|
|Organization:||Humboldt University Berlin, Department of Computer Science|
|Posted-Date:||29 Sep 2002 15:37:59 EDT|
"Joe Hendrix" <email@example.com> writes:
> 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.
Formal semantics of languages are indeed a research area with quite
some activity. There are various strategies and calculi (sp?) used.
Some of them come with a formal notation.
Notice that there are typically two areas you might want to formalize:
- well-formedness. Is a given sentence that meets the formal syntax
(i.e. derives from the start symbol) "correct"? This is usually
described by a set of predicates, e.g.
"For every identifier occuring in an expression, there must be a
definition of that identifer, and that definition must denote a
To formalize such predicates, predicate calculus is often used. In a
rich type setting system (e.g. if Unicode is available), you can use
the traditional mathematical symbols to write down
predicates. Alternatively, you can use an ASCII syntax. Common
syntaxes are the one of TeX, and the Object Constraint Language (OCL).
- "meaning". This is much harder to grasp. For a programming language,
you typically want to formalize execution semantics, i.e. What does
it mean to execute a program?
This is where a wide range of theories are used. In general, the
idea is that there is a potentially-infinite machine executing the
algorithm, and the formal semantics describes properties of that
machine. One approach is to define the notion of traces (series of
states in the machine), and then give constraints on the set of
"correct" traces. The calculus of Abstract State Machines (ASM),
from Gurevich, can be used to formalize such traces.
A recent habilitation thesis by Andreas Prinz describes all this in
more detail; the abstract and full text of this is available at
Return to the
Search the comp.compilers archives again.