Re: Formal semantics for C

On 22-Dec-2001, Matthias Felleisen <matthias@ccs.neu.edu> wrote:
> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
> There is also the work by Gurevitch (Michigan) using evolving algebras: 
>   Yuri Gurevich and James K. Huggins, "The Semantics of the C Programming
>   Language". First appeared in Selected papers from CSL'92 (Computer
>   Science Logic), Springer Lecture Notes in Computer Science 702, 1993,
>   274--308.
>   http://www.eecs.umich.edu/gasm/papers/calgebra.html
> The question that I have is what does it mean to have a semantics of C?  In
> my mind, a semantics is a mathematical model that predicts the behavior of
> a program in some programming language.
> Unless you nail down the precise hardware, os specs, compiler specs, I
> can't see how one can possibly specify the semantics of C.

A semantics doesn't need to be deterministic.  It can specify a set of
possible behaviours.  Indeed for almost all programming languages the
semantics is not deterministic.

The semantics for a programming language can also be parameterized
(i.e. dependent on certain implementation-defined characteristics).

Fergus Henderson <fjh@cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.