Re: Formal semantics for C

To: kfl@it.edu
Subject: Re: Formal semantics for C
From: Matthias Felleisen <matthias@ccs.neu.edu>
Date: Sat, 22 Dec 2001 14:23:05 -0500 (EST)
Cc: types@cis.upenn.edu, S.J.Thompson@ukc.ac.uk, Michael.Norrish@cl.cam.ac.uk
In-reply-to: <200112221624.fBMGOdq04891@saul.cis.upenn.edu> (message from Ken Friis Larsen on 22 Dec 2001 15:40:50 +0000)
References: <200112221456.fBMEunr29447@saul.cis.upenn.edu> <200112221624.fBMGOdq04891@saul.cis.upenn.edu>
Reply-To: matthias@ccs.neu.edu

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:

Re: Formal semantics for C

From: Michael Norrish <Michael.Norrish@cl.cam.ac.uk>