Re: Formal semantics of language semantics

"Joe Hendrix" <j*lstnme*@uiuc.edu> 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
    value".


    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


http://dochost.rz.hu-berlin.de/abstract.php3/habilitationen/prinz-andreas-2001-05-23


Regards,
Martin

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