[Prev][Next][Index][Thread]
Re: Formal semantics for C
Corky has made the most important points.
My conjecture is that you probably didn't mean "non-deterministic" but
indeterminate. Perhaps you're trying to say that all unsafe operations
should be bottom (denotationally speaking), since we have no
information about them. This, however, would be a bad mistake that was
made in the early history of the full abstraction problem. When you
computation is erroneous, there is information. (You may not like it,
but it is not absence of information, as bottom would make you think.)
[See the papers that Corky and I wrote on full abstraction for
sequential higher-order languages.]
In C's case the real problem is that you don't even know when to
specify that your semantics is unspecified without going through an
extreme detour. Just think about how you would specify that an array
access is out of bounds. When the array is passed to a procedure, you
typically don't even have access to its bound. If you do, what exactly
are you going to say?
-- Matthias
Follow-Ups:
References: