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

Re: Formal semantics for C


Thanks, that's what I thought. Indeed, I thought you'd reference the more
interesting and relevant problem that you can't decide whether an array 
index is in the proper range. I rest my case. -- Matthias

  > From: Michael Norrish <Michael.Norrish@cl.cam.ac.uk>
  > Content-Type: text/plain; charset=us-ascii
  > Date: Sat, 29 Dec 2001 10:51:01 +0000
  > Cc: kfl@it.edu, types@cis.upenn.edu, S.J.Thompson@ukc.ac.uk
  > 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.
  >
References: