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

RE: Nondeterminism / formal semantics of C

In defense of C, what is the meaning of the following ML
program?

  1+1;

Is it 2 or is it "uncaught exception Overflow"?  

Also, as someone else has pointed out, it is possible to
produce a "memory-safe" implementation of C (see for instance
Necula's CCured or the previous Safe-C work out of Wisconsin.)

Now to attack C:  

The language leaves many (important) things "undefined".
We cannot use a denotational semantics that maps such
program transitions to "any possible state" simply because
we cannot construct a useful mathematical model of what
those states might be.  They might be the state in which
the Universe explodes, or your credit card number gets
sent to Microsoft.  All things are possible and indeed,
many fantastic things have been achieved when programs
have stepped into this undefined territory (e.g., buffer
overruns.)

-Greg