29 Sep 2002 15:37:59 -0400

Related articles |
---|

Formal semantics of language semantics j*lstnme*@uiuc.edu (Joe Hendrix) (2002-09-25) |

Re: Formal semantics of language semantics loewis@informatik.hu-berlin.de (Martin v. =?iso-8859-1?q?L=F6wis?=) (2002-09-29) |

Re: Formal semantics of language semantics nmm1@cus.cam.ac.uk (Nick Maclaren) (2002-09-29) |

Re: Formal semantics of language semantics i.dittmer@fh-osnabrueck.de (Ingo Dittmer) (2002-09-29) |

Re: Formal semantics of language semantics joachim_d@gmx.de (Joachim Durchholz) (2002-09-29) |

Re: Formal semantics of language semantics stephen@dino.dnsalias.com (Stephen J. Bevan) (2002-09-29) |

Re: Formal semantics of language semantics lex@cc.gatech.edu (Lex Spoon) (2002-09-29) |

Re: Formal semantics of language semantics whopkins@alpha2.csd.uwm.edu (Mark) (2002-09-29) |

[15 later articles] |

From: | "Martin v. =?iso-8859-1?q?L=F6wis?=" <loewis@informatik.hu-berlin.de> |

Newsgroups: | comp.compilers |

Date: | 29 Sep 2002 15:37:59 -0400 |

Organization: | Humboldt University Berlin, Department of Computer Science |

References: | 02-09-149 |

Keywords: | semantics |

Posted-Date: | 29 Sep 2002 15:37:59 EDT |

"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

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.