Re: Formal semantics for C

To: matthias@ccs.neu.edu
Subject: Re: Formal semantics for C
From: Michael Norrish <Michael.Norrish@cl.cam.ac.uk>
Date: Fri, 28 Dec 2001 13:02:04 +0000
Cc: kfl@it.edu, types@cis.upenn.edu, S.J.Thompson@ukc.ac.uk
In-Reply-To: <20011222192305.2D9C9206F4@sualocin.ccs.neu.edu>
References: <200112221456.fBMEunr29447@saul.cis.upenn.edu> <200112221624.fBMGOdq04891@saul.cis.upenn.edu> <20011222192305.2D9C9206F4@sualocin.ccs.neu.edu>
Reply-To: Michael.Norrish@cl.cam.ac.uk
Sender: Michael Norrish <Michael.Norrish@cl.cam.ac.uk>

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.

Michael.

Follow-Ups:

Re: Formal semantics for C

From: Matthias Felleisen <matthias@ccs.neu.edu>

References:

Re: Formal semantics for C

From: Matthias Felleisen <matthias@ccs.neu.edu>