Re: Undefined behaviour [was Re: The D Programming Language]
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.
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.
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.
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.
Andrei
--
[ See http://www.gotw.ca/resources/clcm.htm for info about ]
[ comp.lang.c++.moderated. First time posters: Do this! ]