Re: Nondeterminism / formal semantics of C
Subject: Re: Nondeterminism / formal semantics of C
From: Fergus Henderson <firstname.lastname@example.org>
Date: Sat, 29 Dec 2001 17:21:10 +1100
In-Reply-To: <200112290304.fBT34eT12252@saul.cis.upenn.edu>; from email@example.com on Fri, Dec 28, 2001 at 10:04:12PM -0500
Matthias Felleisen <firstname.lastname@example.org> 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 <email@example.com> | "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.