Re: Formal semantics for C

Matthias Felleisen writes:
> 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. One
> could specify a very small kernel of C, but as soon as you admit
> arrays you're not going to produce anything that will predict the
> behavior in a reliable manner.
I apologise if this sounds as if I'm belabouring the point, but the C
Standard explicitly defines the notion of a "strictly conforming
program", one whose execution is guaranteed to produce the same
behaviour on all platforms.  

Other programs might be guaranteed to work, but because of
non-determinism will give different answers in different
circumstances.  Other programs are beyond the pale. 

A formal semantics for C would classify programs according to the
above, allowing you to predict, for example, that program X will
always run, producing the answer 42; will run, producing a number in
the range 10-15; or that it's illegal, and that its behaviour is thus
unpredictable, or at least, completely dependent on the vagaries of
the implementation.


Follow-Ups: References: