[Prev][Next][Index][Thread]
More on Formal Semantics of C
martinb writes:
> as semanticists we must try and do better. this is the context of my
> critique. it is simply bad slightly sloppy to give a semantics
> without specifying the intended notion of observation and
> equivalence. its like giving a category through its objects while
> omitting the morphisms. it is meaningless. the reason why people get
> away with this is that languages like the sequential and untimed
> core of C are totally uncontroversial (when was the last time you
> asked yourself what if-then-else did?). however, that does not mean
> that there are no hidden assumptions. but these hidden assumptions
> are shared by everybody who may use the semantics. that's why they
> do not usually cause problems. let me give you an example. the
> following clause might be part of a translation of C into assembly
> language. it deals with sequential composition.
> trans( P;Q ) = trans( P ); sleep( 1 year ); trans( Q )
The same critique might equally be made of the Definition of Standard
ML. My view is that providing a post hoc formal specification of C,
is as valuable as providing SML with a definition. It makes the
contract between implementor and user explicit, and makes possible
rigorous analysis of certain aspects of the program. Yes, timing
analyses are not possible in either language (both of which have
sequential composition with a ; operator), but I don't think the
respective semantics are "meaningless".
Further, it is not the case that the sequential and untimed parts of C
are uncontroversial. For example, if you go to
http://gcc.gnu.org/readings.html
partway down the page you will find links to four different attempts
(including mine) to make sense of the standard's language on sequence
point rules. This sort of thing is important for compiler writers,
and sadly, controversy does exist. For example, Clive Feather's model
says that
a[a[i]] = 0
is defined if a[i] == i. My semantics says that it isn't.
The newsgroup comp.std.c provides more evidence that the ISO Standard
continues to baffle people. Even standardisation committee members
disagree. A formal semantics (anybody's) would remove much ambiguity,
and surely that's worth something.
Michael.