Re: Undefined behaviour [was Re: The D Programming Language]
Andrei Alexandrescu (See Website For Email) wrote:
James Kanze wrote:
Java has no acknowledged undefined behavior. Unless you
consider that its inventors were divinely inspired, and somehow
protected from the errors which the rest of us make, whether it
be in programming or in writing a specification, you should be
sceptical of such claims.
This is wrong. Please, let us try to make statements when they are
backed up by knowledge.
Well, I have specific knowledge that the Java specification was
written by human beings. And while I cannot prove it, my
experience gives me very strong reasons to be believe that human
beings are not perfect.
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.
And what relationship does that have to not having undefined
behavior? A language can be perfectly type safe, and still have
undefined behavior.
But of course, your statement begs the question anyway. You now
have to prove that the proof is correct, and more importantly,
complete. Unless you have divine revelation for that. (Note
that the "complete" is the tricky part. If you forget to define
some behavior, you have undefined behavior. If you forget to
consider certain steps in your proof, you're proof is not
complete, and the language may have undefined behavior. This
is, for example, where the original Java specification failed
with regards to the case I raised.)
For more details, see "Types and Programming Languages" by Benjamin Pierce.
Single-threaded and reflection-less Java has been proven to be typesafe
in 1999. The proof operates on a small core of Java (called
Featherweight Java) for proof size reasons. See
http://citeseer.ist.psu.edu/igarashi99featherweight.html.
I don't know whether similar formal proofs have been made for
multithreaded programs, but
http://www.cs.umd.edu/~pugh/java/memoryModel/semantics.pdf seems to do
exactly that (using a notation that I don't know). At any rate, it is
commonly considered that Java has gone farther than most languages in
defining semantics of multithreaded programs.
Understanding and dealing with such concepts entails long, unrewarding
work. (I suck at it and would at most be able to sweat my way through a
paper, but never to produce one.) But it is self-understood that an
unwillingness to get acquainted with some theoretical concepts that have
little practical utility at best, comes together with some restraint
when it comes about peremptory statements.
I'm not sure I agree. Because I'm using the language
pragmatically, in a concrete implementation. I'm aware
(vaguely) that there are numerous techniques of such proofs, but
as you point out, "[they] operate on a small core of Java". The
problem with language features is that they interact. Proving
each individual feature doesn't buy you much. And applying the
proof to the entire language has two problems: the techniques
being used generally don't scale well, and you still have to
prove that you haven't forgotten any feature, and haven't failed
to consider any combination of features.
They're along the same lines as
claims that a non-trivial program has no errors.
Program verification is known to be intractable for even simple
programs, unlike typechecking. So the comparison does not make sense.
If simple typechecking were sufficient to ensure no undefined
behavior, you might have a point (and even then, I'm not
convinced).
At any rate, you're free to believe what you want here, because
as far as I can see, it has no practical implications.
--
James Kanze (Gabi Software) email: james.kanze@gmail.com
Conseils en informatique orient?e objet/
Beratung in objektorientierter Datenverarbeitung
9 place S?mard, 78210 St.-Cyr-l'?cole, France, +33 (0)1 30 23 00 34
[ See http://www.gotw.ca/resources/clcm.htm for info about ]
[ comp.lang.c++.moderated. First time posters: Do this! ]