Re: Formal semantics for C

• To: matthias@ccs.neu.edu
• Subject: Re: Formal semantics for C
• From: Michael Norrish <Michael.Norrish@cl.cam.ac.uk>
• Date: Sat, 29 Dec 2001 10:51:01 +0000
• Cc: kfl@it.edu, types@cis.upenn.edu, S.J.Thompson@ukc.ac.uk
• In-Reply-To: <20011228135034.F21FA206FC@sualocin.ccs.neu.edu>
• References: <200112221456.fBMEunr29447@saul.cis.upenn.edu> <200112221624.fBMGOdq04891@saul.cis.upenn.edu> <20011222192305.2D9C9206F4@sualocin.ccs.neu.edu> <15404.27980.393340.141579@carp.cl.cam.ac.uk> <20011228135034.F21FA206FC@sualocin.ccs.neu.edu>
• Reply-To: Michael.Norrish@cl.cam.ac.uk
• Sender: Michael Norrish <Michael.Norrish@cl.cam.ac.uk>

Matthias Felleisen 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? 
 
No.  A strictly conforming program isn't allowed to divide by zero
(among many other restrictions) because this represents undefined
behaviour. 

There's no way of deciding if a program is or isn't going to divide by
zero, so the class is undecidable.

Michael.

• Re: Formal semantics for C
• From: Matthias Felleisen <matthias@ccs.neu.edu>

• Re: Formal semantics for C
• From: Matthias Felleisen <matthias@ccs.neu.edu>
• Re: Formal semantics for C
• From: Michael Norrish <Michael.Norrish@cl.cam.ac.uk>
• Re: Formal semantics for C
• From: Matthias Felleisen <matthias@ccs.neu.edu>

• Prev: Re: Formal semantics for C
• Next: Re: Nondeterminism / formal semantics of C
• Index(es):
  • Main
  • Thread