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

Re: Formal semantics for C

> 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? there is no full abstraction and
definability result (which i take to be a minimal prerequisites for a
usable formal semantics), not even a proof of soundness or a
definition of what it means for two evolving algebras to be equal

there is an immediate objection: of course in a sense full
abstraction, definability or soundness cannot be given in this setting
because the semantics of C has never been formally specified in the
first place. this is true, but it only means that what you have
defined is a semantics (rather than a semantics of C). 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

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." 

i don't believe this. the C libraries contain some fancy operations
like longjmp or the POSIX thread creation & manipulation mechanisms.
i don't think it is at all straightforward to model them. POSIX
threads can have very complicated interactions through distributed
shared memory with non-trivial memory consistency models that may
include features like memory access reordering, memory barriers,
spurious wakeups of condition variables ... i'm not even going to start
talking about timers and networks which are also integral and heavily
used part of the C libraries ...

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

martin
Follow-Ups: