Re: Nondeterminism / formal semantics of C

Matthias Felleisen <matthias@ccs.neu.edu> writes:
> Excuse my ignorance, but is the Standard's notion of "conforming program" a
> decidable notion?  If so, is your semantics accompanied by an algorithm? 

The C standard's notion of "conforming program" is indeed decidable,
but unfortunately it is vacuous: every program is a conforming program.
The rationale for this is apparently to allow people who write non-portable
programs to be able to nevertheless claim that their programs are "conforming".

The C standard also has a notion of "strictly conforming" program.
This one, fortunately, is more useful.  Like all interesting run-time
program properties, it is undecidable in general, but it can be proven
for particular programs.

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.