Re: Undefined behaviour [was Re: The D Programming Language]
Jeffrey Yasskin wrote:
On Dec 8, 10:10 am, "Andrei Alexandrescu (See Website For Email)"
<SeeWebsiteForEm...@erdani.org> wrote:
It is well understood how to define languages that have no undefined
behavior. That can be proved mathematically (using formal logic). The
proof includes two parts: progress and preservation. Progress proves
that a well-typed program in any state will make a step. Preservation
proves that whatever step a program takes, it will stay well-typed.
Together, these two proofs complete the type safety proof of a language.
How did you get from "Language X is typesafe" to "Language X has no
undefined behavior"?
Proving progress and preservation defines semantics for all programs
written in a language. The term I should have used is "sound," that's
what they use in formal languages.
I don't doubt that it's possible to prove that a language has fully
defined behavior, and I suspect it's been done for Scheme and ML
(though I don't have links), but both proofs and specs tend to have
bugs, and Java's a pretty big spec, so I'd be surprised if they managed
to define everything.
It turns out proof errors are very rare to come across in peer-reviewed
serious publications. The only one I know of is on Generic Java, see
http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00849.html.
The funny part is that the unsoundness was exactly in the part of the
language that was _not_ subjected to formal proof!
C++, by admitting that certain things are undefined, at least lets
programmers defend themselves against those features.
I do not understand this sentence.
On the other
hand, C++ forgot to define some things too, and the particular brand of
Undefined Behavior(tm) it allows lets in memory stomping bugs, which
are extremely hard to debug no matter what tools you have. (That's
Undefined Behavior as defined by the standard, as opposed to just
behavior the standard left undefined. ;)
I doubt anoyone "forgot" to define something. The UB parts of C and C++
are in there for speed and expressiveness reasons.
I would claim that thread synchronization issues are just as hard to
debug as memory stomping bugs, and are just as undefined (little U this
time). Even if the language's invariants are maintained, the program's
are destroyed, and as the programmer, I care more about the program's
invariants.
Your claim is wrong. Debugging a program in which language invariants
are still in vigor cannot be as hard as debugging a program with no
invariants.
Andrei
--
[ See http://www.gotw.ca/resources/clcm.htm for info about ]
[ comp.lang.c++.moderated. First time posters: Do this! ]