Re: Formal semantics for C

To: Fergus Henderson <fjh@cs.mu.oz.au>
Subject: Re: Formal semantics for C
From: Corky Cartwright <cork@rice.edu>
Date: Wed, 26 Dec 2001 01:21:35 -0600 (CST)
Cc: matthias@ccs.neu.edu, kfl@it.edu, types@cis.upenn.edu, S.J.Thompson@ukc.ac.uk, Michael.Norrish@cl.cam.ac.uk
In-Reply-To: <200112251446.fBPEk5Q19557@saul.cis.upenn.edu>

>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).

Of course these statements are true, but they are not pertinent to the
point that Matthias raised.  How are you going to characterize the
effects of all possible machine and implementation dependencies in any
mathematically interesting way using non-determinism?  For example,
what is the result of an unsafe operation such as updating a
out-of-bounds array element?  It is hard to identify any set of states
short of all possible program states (including aborting errors) as
the result such an operation.

All of the "semantics" that I have seen for C cheat on the issue of
unsafe operations.  Either they codify the behavior of a particular C
implementation (including a complete machine-level memory model) or
they punt when an unsafe operation is performed.

Compiler optimization researchers perform non-trivial analyses of C
programs (e.g., a pointer alias analysis) by ducking the issue of unsafe
operations: the simply assume that unsafe operations are never
executed.

-- Corky Cartwright
   Rice University

Follow-Ups:

Re: Formal semantics for C

From: Fergus Henderson <fjh@cs.mu.oz.au>