[Prev][Next][Index][Thread]
Re: Nondeterminism / formal semantics of C
-
To: bcpierce@cis.upenn.edu
-
Subject: Re: Nondeterminism / formal semantics of C
-
From: Fergus Henderson <fjh@cs.mu.oz.au>
-
Date: Sat, 29 Dec 2001 17:21:10 +1100
-
Cc: types@cis.upenn.edu
-
In-Reply-To: <200112290304.fBT34eT12252@saul.cis.upenn.edu>; from bcpierce@saul.cis.upenn.edu on Fri, Dec 28, 2001 at 10:04:12PM -0500
-
References: <200112290304.fBT34eT12252@saul.cis.upenn.edu>
-
User-Agent: Mutt/1.2.5i
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.