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

Re: Formal semantics for C

On Fri, 8 Mar 2002 martinb@dcs.qmul.ac.uk wrote:

> James K. Huggins wrote:
> > Some time ago, Yuri Gurevich and I did a formal semantics of C 
> > using the Abstract State Machine (ASM) methodology, then called
> > "evolving algebras".  You can find more information at:
> > 
> > 	http://www.eecs.umich.edu/gasm/papers/calgebra.html 
> 
> i'm a bit startled by this claim that you have done a "formal
> semantics of C". how do you know? 

This is the problem of any formal, mathematical realization of an informal
object.  Barring an official pronouncement from ISO, or ANSI, or whatever
authorities one cares to cite, any translation of the natural language
description of C into a formal model cannot be "proven" correct (as you
point out later in your message). One must simply examine the model and
one's understanding of the language and ask whether the two are
equivalent.  We have had many readers who have told us that we have gotten
it "right", with only one small problem noted later in the literature.

> there is no full abstraction and definability result (which i take to be
> a minimal prerequisites for a usable formal semantics)

It all depends on what you mean by "usable".  Our semantics for C have
been used for teaching the language in classrooms, for example, without
any such results.  

> not even a proof of soundness or a definition of what it means for two
> evolving algebras to be equal

Such items can be found elsewhere in the evolving algebra/ASM literature,
much of which can be found at the parent website
	http://www.eecs.umich.edu/gasm/

We chose to separate concerns and not treat such in our paper.  Other
papers do such proofs of equivalence for programming languages in
excrutiating detail. 

> in addition, and slightly contradicting what i have said, every C
> compiler + libraries implicitly *defines* a formal semantics, albeit a
> rather complicated one, which may or may not approximate what one may
> expect to be *the* semantics of C. you could test your semantics against
> a compiler, although i don't recommend it

I don't see the problem.  Our semantics has several "abstract" (i.e. not
completely specified) functions which capture the ambiguities in the
language, which of course must be specified in full detail for an
executable compiler + libraries.  Our semantics is completely compatible
with any such compiler.  

> this lack of a hard test whether your semantics actually works
> (in the sense that it equates exactly the translations of those
> programs that are observably equivalent in C) is probably also the
> reason why you write (on page 1)

>   "it is not difficult to extend our description of C to include
>   any desired library function or functions." 

On the contrary; this was simply an attempt to separate concerns.  One
could make the argument that the C libraries are not part of the
"programming language C" per se (notice, for example, that the library
function names do not appear in the grammar for the language).  

Also, I will beg for a bit of historical mercy in this criticism.  At the
time we began this work in 1989, the ISO standard (if it even existed) was
not available to us, in particular for the libraries.  We based our
semantics (as we state in the paper) on K&R v.2.  Ritchie himself states
that K&R did not emphasize the importance of the libraries: 
 
	At the time of publication of K&R, C was thought of mainly as the
	system programming language of Unix; although we provided examples
	of library routines intended to be readily transportable to other
	operating systems, underlying support from Unix was implicitly
	understood.
		Dennis M. Ritchie, "The Development of the C Language",
		2nd History of Programming Languages conference,
		Cambridge, MA, April 1993
		http://cm.bell-labs.com/cm/cs/who/dmr/chist.html
 
> a comprehensive formal semantics of a significant programming language
> that includes such features has (to the best of my knowledge) never
> been given and the reason is that it would be be non-trivial

ASMs/evolving algebras have been applied to dozens of full, non-trivial
programming languages.  Whether such work meets the criteria you cite is
perhaps in the eye of the beholder; I will simply suggest that you look at 
	http://www.eecs.umich.edu/gasm/proglang.html
and examine the papers therein.  (Perhaps the papers on SDL, Java, or
Prolog would be good places to start.)

--Jim Huggins (jhuggins@kettering.edu)
References: