[Prev][Next][Index][Thread]

Re: Formal semantics for C

On 26-Dec-2001, Matthias Felleisen <matthias@ccs.neu.edu> wrote:
> 
> My conjecture is that you probably didn't mean "non-deterministic" but
> indeterminate.

Well, I meant what I said, but maybe you understood it to mean something
different ;-).

I have in mind a specific meaning for the word in this context:
a non-deterministic semantics is one in which the denotation of
a program is a _set_ of possible behaviours. 

Maybe you have in mind some other meaning.  But I'm not sure what
you have in mind.  If you have some particular suggestions about what
terminology I should use, you'd need to explain them in more detail.

> Perhaps you're trying to say that all unsafe operations
> should be bottom (denotationally speaking), since we have no
> information about them.

"unsafe" operations may include those whose behaviour is
unspecified or implementation-defined, as well as those which
have undefined behaviour.  The former two should not be modelled as bottom.

Also, simply modelling the behaviour of individual operations with
undefined behaviour as bottom is not sufficient to capture the semantics
of C; you also need a distinguished semantic element indicating undefined
behaviour, which gets propagated up in the semantics of all program
constructs except the whole program.

And once you have such a distinguished semantic element, then you don't
*need* to model the semantics of individual operations with undefined
behaviour as bottom (the universal set); they can be denoted by any set
containing this distinguished element, and so it could be simpler to
use the singleton set containing just that element.

However, the denotation of a _whole program_ which executes any C
operation which has "undefined behaviour" should be bottom, yes.
That's what "undefined behaviour" means: any behaviour is permitted.

> This, however, would be a bad mistake [...]

The design of C is full of bad mistakes.
The question, for people who want a formal semantics for C,
is not how to fix those mistakes, but how to model them.

> In C's case the real problem is that you don't even know when to
> specify that your semantics is unspecified without going through an
> extreme detour. Just think about how you would specify that an array
> access is out of bounds. When the array is passed to a procedure, you
> typically don't even have access to its bound.

"You" (the programmer) may not, and the C implementation may not,
but in the formal semantics for C, arrays and pointers are certainly
accompanied by their bounds.

-- 
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.
Follow-Ups: References: