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

Re: Formal semantics for C




There is also the work by Gurevitch (Michigan) using evolving algebras: 

  Yuri Gurevich and James K. Huggins, "The Semantics of the C Programming
  Language". First appeared in Selected papers from CSL'92 (Computer
  Science Logic), Springer Lecture Notes in Computer Science 702, 1993,
  274--308.

  http://www.eecs.umich.edu/gasm/papers/calgebra.html

The question that I have is what does it mean to have a semantics of C?  In
my mind, a semantics is a mathematical model that predicts the behavior of
a program in some programming language.

Unless you nail down the precise hardware, os specs, compiler specs, I
can't see how one can possibly specify the semantics of C. One could
specify a very small kernel of C, but as soon as you admit arrays you're
not going to produce anything that will predict the behavior in a reliable
manner. 

-- Matthias

  > Cc: "S.J.Thompson" <S.J.Thompson@ukc.ac.uk>, Michael.Norrish@cl.cam.ac.uk
  > From: Ken Friis Larsen <kfl@it.edu>
  > Date: 22 Dec 2001 15:40:50 +0000
  > User-Agent: Gnus/5.0808 (Gnus v5.8.8) Emacs/20.6
  > Content-Type: text/plain; charset=us-ascii
  > Original-Sender: Ken Larsen <Ken.Larsen@cl.cam.ac.uk>
  > X-Virus-Scanned: by AMaViS snapshot-20010714
  > 
  > [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
  > 
  > "S.J.Thompson" <S.J.Thompson@ukc.ac.uk> writes:
  > > Query about the formal semantics of C:
  > > 
  > > Are types readers aware of any work on formalizing the semantics
  > > of the C programming language?
  > 
  > Michael Norrish (Computer Lab, University of Cambridge) developed a
  > formal model for C and embedded this model into the HOL theorem
  > prover.  More information here:
  >         http://www.cl.cam.ac.uk/users/mn200/PhD/
  > 
  > 
  > Cheers,
  > 
  > --Ken Friis Larsen
  > 

Follow-Ups: